Wild shot in the dark, but would anyone have any idea why compiling coq-elpi with tactician enabled fails? For reference: I created an opam switch with coq 8.11 and coq-elpi (which compiled without issue), installed tactician, and then the coq-tactician-stdlib package (which recompiles coq's stdlib in-place so that tactician can record the tactics used in all of the proofs). Then I recompiled coq-elpi (as the coq stdlib has been recompiled underneath it) and now one of the tests fails in a way that I really do not understand: tests/test_ltac.v failed, in particular `Fail elpi intro x y.`

. I'm not even sure how tactician could be screwing with the arity checking there. I won't be able to really dig into debugging it for a little while yet, but I suspect it's well out of my depth regardless.

Can you give me a pointer to tactician and tell me how to reproduce it?

https://github.com/coq-tactician/coq-tactician is their github repo, they have a dev opam repo at git+https://github.com/coq-tactician/tmp-archive.git

The main package is coq-tactician, but it's installing coq-tactician-stdlib and running tactician recompile that triggers the issue (or installing coq-elpi after installing coq-tactician-stdlib)

For reference, I'm compiling coq-elpi 1.5.0 from coq-released.

```
opam switch create tactician 4.09.1
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add tactician git+https://github.com/coq-tactician/tmp-archive.git
opam pin coq 8.11.0
opam install coq-elpi
opam install coq-tactician coq-tactician-stdlib
tactician recompile # This will suggest recompiling coq-elpi to account for the recompiled stdlib, and that breaks
```

Ought to reproduce it...

Thanks I'll look into that tomorrow: https://github.com/LPCIC/coq-elpi/issues/183

This looks like it could be the cause: https://github.com/coq-tactician/coq-tactician/blob/master/theories/Ltac1/Record.v

Elpi extends the default proof mode, not the tactician one. I need to dig deeper in order to see if I can patch a common grammar entry or not. I guess a set default proof mode "Default" can work around the failure.

Hmm... I wonder if I could change the default proof mode only around the actual stdlib, or something along those lines. Thanks for finding that!

The problem is different.

```
Require Import Tactician.Ltac1.Record.
Example test_intro : True -> True.
Proof.
Fail whatever. (* Error: the command did not fail *)
```

Apparently `Fail`

does not work properly: here whatever does not even exist.

It could be the `pre_vernac_solve`

call in https://github.com/coq-tactician/coq-tactician/blob/71f946774da7fbf93ae79ee849698d37cabd0b44/src/g_ltac1_record.mlg#L19 that says `false`

here. I don't understand what this code is really trying to do.

I don't this it is elpi specific, it's just that elpi compiles a test suite that contains `Fail`

, while most (all?) other coq developments don't.

Do you want me to open an issue on the GH repo of tactician?

I pushed a fix for the Fail problem. If you reinstall Tactician, it should now work. Unfortunately, you can indeed not use Elpi's grammar extensions with Tactician. I'm not well-versed enough in Coq's grammar system to immediately determine if we can easily fix that.

Doing something that transparent/automatic for any tactic language seems hard to me. But if I had an API to call in order to tell tactician which are the features of my tactic invocation, I could expose that to elpi, and then one could write elpi tactics that tell tactician the features every time they are called. I think your approach is perfectly fine for the standard tactics, but for custom ones... even an opt-in model could work I guess.

An API could be interesting. However, this would not be a trivial undertaking because there are quite a few issues that need to be supported. Some random ones I can think of right now: 1) Backtracking in Coq's proof monad. 2) Tactic discharging in sections (I have this working to some degree for Ltac and Ssreflect).

Right now I am considering how to deal with Ssreflect. In principle, it already works because it is just an extension of Ltac. But the recording granularity is quite low. I might consider writing some manual code to decompose the generic arguments of Ssreflect or possibly I could parse its grammar and (semi-)automate the decomposition. If that would be possible, such an approach might also work for Elpi.

I think you should ignore elpi for now, there are not many proofs written using elpi out there.

For ssr I don't know. I've the impression it would be simpler to patch it and have it declare all its steps. See for example the entry point for intro pattern interpreter (the things after `=> x /P f /= ->`

). https://github.com/coq/coq/blob/5b62a6908202eef2c40d2f4989d8d21d0f6c3e16/plugins/ssr/ssripats.ml#L445 The AST is internal to the plugin, it is not something you can manipulate from Coq proper.

Maybe here is even simpler: https://github.com/coq/coq/blob/5b62a6908202eef2c40d2f4989d8d21d0f6c3e16/plugins/ssr/ssripats.ml#L417

Yes, Elpi is not high on my list currently (although the two of you are the only ones I know of who have installed Tactician...).

Regarding ssr: I would rather avoid getting my code all tangled up into that of ssr. I tried this approach once with Ltac, and it went quite horribly. But it seems to me that I can manipulate the AST of ssr reasonably easily through the Ltac API. The only problem is breaking through the TacGeneric/TacML barrier. I already tried this recently for the tactic discharging I mentioned above, and although not pretty, it was not a horrible experience. And I am thinking that I might partially automate this by parsing ssr's grammar.

Or alternatively, we could bite the bullet and completely integrate Tactician into the Coq codebase. But honestly, I would not advise doing this at this stage.

But I might give your approach a try too.

Last updated: Feb 05 2023 at 13:02 UTC