The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Hi

I know I should use an error monad instead of the option monad I'm
currently in. It was just faster to register the reson of the error
that way (I'm not throwing any exception) as it did not modify my
proofs. But I still think a call to a parameter should not be
optimized away, since it can be really important for things like
dumping an AST as said earlier or sometimes debugging (since yes, even
coq code can have bugs!!).

Cheers.
Alexandre

Le dimanche 8 mai 2011, AUGER Cedric  a écrit :
> Le Sat, 7 May 2011 01:47:47 +0200,
> Alexandre Pilkiewicz  a écrit :
>
>> Dear list
>>
>> I'm trying report some errors in my code by adding things like
>>
>> Parameter error_badly_masked: unit -> unit.
>> Extract Constant error_badly_masked => "Errors.error_badly_masked".
>>
>>
>> Definition .....
>>    let tt := error_badly_masked tt in
>>    ....
>>
>> But the extraction removes this call
>>
>> Is it possible to forbid the extraction to remove call to parameters?
>>
>> Thanks in advance
>>
>> Alexandre
>
> I suggest you to deactivate optimizations of the extractor:
>
> Unset Extraction Optimize.
>
> If you use "tt" in the rest of the code, that should do the trick,
> else, you have to destructure it, to force the dependence to your
> function call:
>
>  Definition .....
>     let tt := error_badly_masked tt in
>     let () := tt in
>     ....
>
> But do you really need to perform some "Extraction constant ..."?
> As P. Letouzey wrote in this list, it is an "unsafe" feature, you
> really need some extra care if you want your code to be really correct.
>
> As I guess you "error_badly_masked" is an exception raiser, you may
> consider using an error monad. I am currently writting a short tutorial
> on extraction that I hope to post on the cocorico wiki. I guess I am
> not good at it, but it may be shorter for you (when it will be done)
> than having a look at the Compcert Project (since it is a big project).
>
> Here is a link if you want to take a look at this project on how to
> manage errors.
> http://compcert.inria.fr/doc/html/Errors.html
>