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.]

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.

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?

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

Thanks! I just opened an issue here: https://github.com/LPCIC/coq-elpi/issues/372.

Fixed in 1.15.1

Enrico Tassi has marked this topic as resolved.

Last updated: May 24 2024 at 22:02 UTC