The Coq mailing list

[Matěj Grabovský <matej.grabovsky AT gmail.com>]

Hi.

You could instead declare Trace like

> Parameter Trace : forall A, nat -> A -> A.
> Extract Constant Trace => "trace_helper".

and define a helper function such as

> let trace_helper n ret = let _ = trace_nat n in ret

Your function would then become

> Definition f (n : nat) := Trace n n.

This will probably get hairy with more complicated expressions but
again, it's just a thought.

Best regards,
Matěj

On 23 November 2015 at 14:25, Frédéric Besson 
<frederic.besson AT inria.fr>
 wrote:
> Dear all,
>
> I would like to trace some Coq extracted code.
> Something like:
> Parameter Trace : nat -> unit.
>
> Definition f (n : nat) := let _ := Trace n in n.
>
> Extract Constant Trace => "trace_nat ».  (* Here, I will perform 
> side-effect *)
> Separate Extraction f.
>
> I have the problem that the extraction mechanism is too clever.
> It removes my call to Trace under the « false » assumption that it is 
> side-effect free.
>
> Is there a way to instruct the extraction not to do that ?
> For instance: Hey, this is an axiom : do not assume there is no 
> side-effect!"
>
> It seems that disabling optimisations is not enough i.e Unset Extraction 
> Optimize.
>
> Does anyone know about any way?
>
> Thanks,
> —
> Frédéric
>
>
>
>
>