Enzo Crance (May 17 2023 at 14:57): Enzo Crance (May 17 2023 at 14:57):Hello. I noticed that printing a variable, then calling a predicate doing things with that variable, then re-printing the variable prints two different names (i.e., X7 before calling the middle predicate, and X9 after). I have a predicate linking variables to integers in the constraint store, and querying it before and after gives twice the same integer, so I guess it is still the same variable, it is just the printer that gives two different names. The bad thing about this behaviour is that it obfuscates the debugging messages, as I can no longer track what is done to each variable. Is there a reason for this?
I did not succeed in minimising the "bug" (it's not a real bug as it is still the same variable internally, just what is printed is a mess)...
Enrico Tassi (May 17 2023 at 19:50):It is not documented, but in vscoq you have this elpi-lang extension, with an "Elpi Tracer" panel. In there you should be able to see a trace, and I guess one sees X7 = X9 at some point. Sometimes this is inevitable, eg if I write X = Y one of the two has to become the other...
Enzo Crance (Jun 01 2023 at 07:36):Is there any documentation about this tracer plugin? I have it in my IDE but cannot find how to actually see a trace.
Enrico Tassi (Jun 01 2023 at 12:32):I should really write some doc, but I'm busy now. Next week I'll be in Nantes, I could show you and then we can write a short howto. How does that sound?
Enrico Tassi (Jun 01 2023 at 12:33):Super short: if you are in Coq, write Elpi Trace Browser. before running your elpi command. If you are in plain elpi, the trace panel should have a button to run your program and load the trace (you should also see the command line options to get the trace, save it to a file and load in the UI).
Last updated: Oct 13 2024 at 01:02 UTC