[Why3-club] Coq driver

Guillaume Melquiond guillaume.melquiond at inria.fr
Mon Mar 17 09:29:27 CET 2014


On 17/03/2014 08:52, Jean-Jacques Levy wrote:
> Dear Why3 fans,
>
> it looks we have problem with Coq driver in new Why3 0.83:
>
> 1- /usr/local/share/why3/drivers/coq.drv exists, but Why3ide seems call
>     /usr/local/share/why3/drivers/coq_8_4.drv
>     That can be fixed with a link between these 2 filenames.

My guess is that your .why3.conf contains an obsolete entry. Make sure 
to rerun why3config --detect-provers after upgrading Why3.

> 2- we have a type declaration missing the Coq file.
> The following why3 type:
> ———
>   type btree =
>   | Empty
>   | Root (list (pair btree int)) btree
>   | Node (list (pair btree int)) btree
> ———
> gives in Coq
> ———
> (* Why3 assumption *)
> Inductive btree :=
>    | Empty : btree
>    | Root : (list (@pair btree btree_WhyType Z _)) -> btree -> btree
>    | Node : (list (@pair btree btree_WhyType Z _)) -> btree -> btree.
> Axiom btree_WhyType : WhyType btree.
> Existing Instance btree_WhyType.
> ———
> which when run gives:
> ———
> Toplevel input, characters 67-80:
> Error: The reference btree_WhyType was not found in the current environment.

Ouch, so many bugs in a single testcase. This will require some heavy 
changes to the Coq printer to fix them. Do not hold your breath.

In the meantime, avoid nesting custom inductive types. For instance, the 
following definition is properly translated to Coq:

   use import list.List

   type btree =
   | Empty
   | Root (list (btree, int)) btree
   | Node (list (btree, int)) btree

Best regards,

Guillaume



More information about the Why3-club mailing list