[Why3-club] Coq driver

Jean-Jacques Levy jean-jacques.levy at inria.fr
Mon Mar 17 08:52:10 CET 2014


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.

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.
———

Hope this message is not new spam. Many thanks for help.

-JJ + Qia -




More information about the Why3-club mailing list