Elijah Malaby (Sep 09 2020 at 13:48): 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.
Enrico Tassi (Sep 09 2020 at 13:57):Can you give me a pointer to tactician and tell me how to reproduce it?
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
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)
Elijah Malaby (Sep 09 2020 at 14:17):For reference, I'm compiling coq-elpi 1.5.0 from coq-released.
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...
Enrico Tassi (Sep 09 2020 at 14:29):Thanks I'll look into that tomorrow: https://github.com/LPCIC/coq-elpi/issues/183
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.
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!
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 *)
Apparently Fail does not work properly: here whatever does not even exist.
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.
Enrico Tassi (Sep 10 2020 at 11:52):Do you want me to open an issue on the GH repo of tactician?
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.
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.
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.
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.
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
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.
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.
Lasse Blaauwbroek (Sep 12 2020 at 17:25):But I might give your approach a try too.
Last updated: Oct 13 2024 at 01:02 UTC