Rodolphe Lepigre (Feb 26 2024 at 12:46): Rodolphe Lepigre (Feb 26 2024 at 12:46):@Janno and I are now having issues with NES, as we do have elpi commands that rely on it. The issue we see is that, since NES is kind of synterp-only, and our command also need an interp phase, we basically end up running a copy of NES's synterp phase at interp. This seems to work mostly fine, but the new_int primitive from elpi does not know about the synterp/interp distinction.
How would you approach this @Enrico Tassi?
Enrico Tassi (Feb 26 2024 at 13:10):There are interp APIs to peek/re-run the synterp phase at interp time:
https://github.com/LPCIC/coq-elpi/blob/0066a3aa0a86375de7601cd67571eff58a28f392/coq-builtin.elpi#L1783
https://github.com/LPCIC/coq-elpi/blob/0066a3aa0a86375de7601cd67571eff58a28f392/elpi/coq-lib.elpi#L609
And APIs to pass (a subset of) synterp actions from synterp to interp:
synterp:acess the log of actions
See NES.Print for an example on how to pass data from synterp to interp.
For new_int, I suggest you call coq.replay-synterp-action {coq.next-synterp-action}. Maybe you can add an assert to check the next synterp action is the one you expect.
Last updated: Oct 13 2024 at 01:02 UTC