[Why3-club] Coq driver
jean-jacques.levy at inria.fr
Tue Mar 18 02:49:28 CET 2014
1- you were right. In fact I did ‘detect-provers’ after posting my message.. and now it’s fine. Sorry for that new spam :-) !!!
2- I do not get the point [you meant that you cannot use a type previously defined in a new one ??!!]. But now it works.
Le 17 mars 2014 à 16:29, Guillaume Melquiond <guillaume.melquiond at inria.fr> a écrit :
> 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
>> 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,
More information about the Why3-club