Stream: Elpi users & devs

Topic: !tactic_mode


view this post on Zulip 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.]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gordon Stewart (Jul 14 2022 at 15:56):

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

view this post on Zulip Gordon Stewart (Jul 14 2022 at 16:47):

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?

view this post on Zulip 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

view this post on Zulip Gordon Stewart (Jul 14 2022 at 19:37):

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

view this post on Zulip Enrico Tassi (Jul 16 2022 at 08:50):

Fixed in 1.15.1


Last updated: Feb 05 2023 at 13:02 UTC