The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Ok, my short tutorial is published on cocorico.

Le Sun, 8 May 2011 13:30:15 +0200,
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 a écrit :

> Le Sat, 7 May 2011 01:47:47 +0200,
> Alexandre Pilkiewicz 
> <alexandre.pilkiewicz AT polytechnique.org>
>  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
>