Gordon Stewart (Jul 14 2022 at 14:33): Gordon Stewart (Jul 14 2022 at 14:33):I have a coq-elpi command that registers a number of constants (using coq.env.add-const).
Some of those constants are proofs, and some of the proofs are built by a separate coq-elpi tactic.
This gives me a
API coq.env.add-const cannot be used in tactics
error.
Is this expected?
Or should I instead expect that the state of tactic_mode is reverted at the end of a coq-elpi tactic?
[Apologies if this question is already answered or discussed elsewhere. Feel free to redirect me in that case.]
Enrico Tassi (Jul 14 2022 at 15:30):Can you better explain what the call stack is? I do have commands which calls coq.ltac.collect-goals on a term, coq.ltac1.call .... and finally add-const. And I don't get the error.
Gordon Stewart (Jul 14 2022 at 15:45):Sure.
I have an elpi command like
Elpi Command the_command.
Elpi Accumulate Db the_database.
Elpi Accumulate lp:{{
main ... :- std.do! [
...
mk-lem Name ...
].
}}.
Elpi Typecheck.
Elpi Export the_command.
mk-lem is defined roughly as:
pred mk-lem i:string, i:term, i:list constructor.
mk-lem Name ... :- std.do! [
...
Lem = {{ <coq-type-of-lemma> }},
std.assert-ok! (coq.elaborate-skeleton Lem _ ELem) "...",
std.assert-ok! (coq.typecheck {{ lp:Bo : lp:ELem }} _) "...",
coq.ltac.collect-goals Bo [SealedGoal] [],
coq.ltac.open (coq.ltac.call "ltac1-that-calls-elpi" Args) SealedGoal [],
coq.env.add-const Name Bo ELem @transparent! C,
...
].
ltac1-that-calls-elpi is ltac1 that calls some ltac2 that eventually calls an elpi tactic of the form:
Elpi Tactic elpi_tac.
Elpi Accumulate lp:{{
...
solve (goal _Ctx _ {{ @ClassImTryingToSolve _ _ _ _ lp:M lp:EL _ }} _ _) _ :- std.do! [
elpi-solver M L,
std.assert-ok! (coq.elaborate-skeleton L _ EL) "...",
].
solve _ _ :- coq.ltac.fail _ "...".
}}.
Elpi Typecheck.
Here's a self-contained example:
Elpi Command the_command.
Elpi Accumulate lp:{{
pred mk-lem i:string.
mk-lem Name :- std.do! [
Lem = {{ (1 + 1 = 2)%nat }},
std.assert-ok! (coq.elaborate-skeleton Lem _ ELem) "failed",
std.assert-ok! (coq.typecheck {{ lp:Bo : lp:ELem }} _) "failed",
coq.ltac.collect-goals Bo [SealedGoal] [],
coq.ltac.open (coq.ltac.call "ltac1_that_calls_elpi" []) SealedGoal [],
% !tactic_mode should equal false here
coq.env.add-const Name Bo ELem @transparent! C_,
].
main [str Name] :- std.do! [
mk-lem Name
].
}}.
Elpi Typecheck.
Elpi Export the_command.
Elpi Tactic elpi_tac.
Elpi Accumulate lp:{{
solve (goal _Ctx _ {{ (1 + 1 = lp:EX)%nat }} _ _) _ :- std.do! [
X = {{ 2%nat }},
std.assert-ok! (coq.elaborate-skeleton X _ EX) "failed",
].
solve _ _ :- coq.ltac.fail _ "failed".
}}.
Elpi Typecheck.
From elpi Require Import elpi.
Ltac ltac1_that_calls_elpi :=
elpi elpi_tac;
reflexivity.
the_command xx.
Running the_command xx gives me
API coq.env.add-const cannot be used in tactics
Not in proof mode.
I haven't looked deeply yet, but I wonder whether the code that sets tactic_mode := true fails to restore the state of tactic_mode when you leave the elpi tactic?
Enrico Tassi (Jul 14 2022 at 19:18):Oh, I see. I was silly, that "ref" should be in the state, eg of the API: https://github.com/LPCIC/coq-elpi/blob/94563ba58b27728893c3df75367b46b2310443be/src/coq_elpi_HOAS.ml#L92
By doing so each elpi runtime would have his ref.
Please, just open an issue. I'll fix it ASAP
Gordon Stewart (Jul 14 2022 at 19:37):Thanks! I just opened an issue here: https://github.com/LPCIC/coq-elpi/issues/372.
Enrico Tassi (Jul 16 2022 at 08:50):Fixed in 1.15.1
Notification Bot (Jul 16 2022 at 20:36):Enrico Tassi has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC