[Why3-club] Coq driver

Jean-Jacques Levy jean-jacques.levy at inria.fr
Tue Mar 18 02:49:28 CET 2014


Guillaume,

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. 

THANKS! -JJ-

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
>>    /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