Stream: Elpi users & devs

Topic: Tactician


view this post on Zulip Elijah Malaby (Sep 09 2020 at 13:48):

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.

view this post on Zulip Enrico Tassi (Sep 09 2020 at 13:57):

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

view this post on Zulip Elijah Malaby (Sep 09 2020 at 14:12):

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

view this post on Zulip Elijah Malaby (Sep 09 2020 at 14:13):

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)

view this post on Zulip Elijah Malaby (Sep 09 2020 at 14:17):

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

view this post on Zulip Elijah Malaby (Sep 09 2020 at 14:22):

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

view this post on Zulip Enrico Tassi (Sep 09 2020 at 14:29):

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

view this post on Zulip Enrico Tassi (Sep 09 2020 at 17:29):

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.

view this post on Zulip Elijah Malaby (Sep 09 2020 at 18:50):

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!

view this post on Zulip Enrico Tassi (Sep 10 2020 at 11:48):

The problem is different.

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

view this post on Zulip Enrico Tassi (Sep 10 2020 at 11:48):

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

view this post on Zulip Enrico Tassi (Sep 10 2020 at 11:52):

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.

view this post on Zulip Enrico Tassi (Sep 10 2020 at 11:52):

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

view this post on Zulip Lasse Blaauwbroek (Sep 11 2020 at 00:36):

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.

view this post on Zulip Enrico Tassi (Sep 11 2020 at 08:23):

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.

view this post on Zulip Lasse Blaauwbroek (Sep 12 2020 at 16:45):

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.

view this post on Zulip Enrico Tassi (Sep 12 2020 at 16:50):

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.

view this post on Zulip Enrico Tassi (Sep 12 2020 at 16:56):

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

view this post on Zulip Lasse Blaauwbroek (Sep 12 2020 at 17:03):

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.

view this post on Zulip Lasse Blaauwbroek (Sep 12 2020 at 17:05):

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.

view this post on Zulip Lasse Blaauwbroek (Sep 12 2020 at 17:25):

But I might give your approach a try too.


Last updated: Feb 05 2023 at 13:02 UTC