:if based debug facility mentioned in tutorial does not work as expected

[MSoegtropIMC]

Going through the tutorial elpi_lang.v I found that the :if base debugging facility does note work.

Elpi Query lp:{{ mypred 3 }}.
Elpi Debug "DEBUG_MYPRED".
Elpi Query lp:{{ mypred 3 }}.
Elpi Debug.
Elpi Query lp:{{ mypred 3 }}.

results in

ok
ok
ok

which is not what I would expect from the description.

This is with

coq-elpi                 1.5.1                             Elpi extension language for Coq
elpi                     1.11.2                            ELPI - Embeddable λProlog Interpreter

both in VSCoq and CoqIDE.

[gares]

Thanks for reporting.

I believe this change in behavior was introduces with elpi 1.11, which supports separate "compilation". Since then Elpi snippets are compiled once and for all, while before they were compiled every time they were executed. This means the :if thing only works if you use Elpi Debug before Elpi Proogram or Elpi Accumulate, since the snippets are compiled at that point in time, while before elpi 1.11 one could flip the flag anywhere.

I hope to be able to move this "conditional compilation" thing out of the tutorial (or at least outside the debugging section) when LPCIC/elpi#68 will be solved (providing a decent debugging facility).

[MSoegtropIMC]

Thanks for the details! Conditional compilation might still be interesting for debugging since one also might do different things besides tracing. But for that it is perfectly fine to do the definitions at the top of the file.