At a Coq call, it has been suggested, in order to favor the adoption of Ltac2 for programming tactics, that to each description of a tactic in the reference manual, the associated Ltac2 typed function and the associated Ltac2 notation be also given. There was the problem however that Ltac2 functions and notations are documented only in the Ltac2 files. To resolve this, couldn't we imagine a script that extract from Ltac2 files triples of tactic name, coqdoc link to the Ltac2 function and coqdoc link to the Ltac2 notation, together with a tag in the rst files which provokes the insertion of the appropriate Ltac2 links in the refman?
This seems like a good idea. I would be in favor of making the Ltac2 documentation more prominent. If this scripting is easy to do, then good. If not, then starting with manual links and writing the automation later would even make sense.
Let me take the opportunity to say that Ltac2 is a dramatic improvement for developing advanced and efficient proof automation. Coq would be substantially less useful without Ltac2. So thank you @Pierre-Marie Pédrot and all contributors. I also want to mention that Elpi is equally useful - for most things the two don't give each other much, for some things Ltac2 is better for some things Elpi. Thank you @Enrico Tassi and contributors. IMHO Elpi also deserves some prominent mentioning, probably not a tight integration into the ref manual, but a prominent mention.
Talking of documentation: it would also be useful to have a table which relates Ltac2 functions to corresponding OCaml functions, maybe with some notes on differences in semantics. I guess the two are close enough to make this not too complicated. I recently looked into AAC-tactics (which is OCaml) and had a really hard time to understand how to do even basic things. After a while I found what to search for in which mli files and it got better than, but the start was really tough.
we have a lot of legacy automation code, both as Ltac1 and in OCaml. Porting some/most of that to Ltac2 should be a research topic, in my opinion...
@Karl Palmskog : what I meant to say is that the "new generation" likely won't have a good reason for ever doing tactics in OCaml. This will mid term reduce the number of people which understand tactics written for OCaml. For this reason we should build some documentation bridge from Ltac2 to OCaml to ensure what exists in OCaml can be maintained in the future.
I think the number of people who understand OCaml tactics is already quite low. Documenting the connection OCaml<->Ltac2 could be useful, but at this point one priority should arguably be to document/evengelize Ltac2 in general
Agree, and in practice, maintenance of most of plugins is done by Coq developers themselves (via overlays).
if I google "Ltac2 tutorial", I find basically only this, that was last updated 4 years ago: https://github.com/tchajed/ltac2-tutorial
IMHO the doc of your favorite extension language should have a list of APIs, easy to browse/search.
Having pointers from user facing tactics to related APIs is not the right way to cut it, if only because there are hundreds of variants of tactics and hopefully a better set of APIs.
In a way, if the tactic is called "rewrite" (or something like that, like setoid_rewrite, foobar_rewrite) I, as a Ltac2/Elpi user, would like to find its entry point in the doc of the extension language by looking for rewrite. If the API is not called rewrite something, or it does not come with a comment that that mentions rewrite, or the doc of the extension language is not searchable, that is a problem of the extension language.
IMO, adding the pointers in the tactic documentation is like trying to solve an X Y problem, and it makes the doc more complex to maintain (if only for the script that would magically do the job).
Another way to put it, extension languages have a clean slate, they can craft a nicer API from scratch, organize it differently and document it properly. That is where the effort should be put, IMHO. Not in trying to reuse the doc we have for this other purpose.
Pierre Roux said:
Agree, and in practice, maintenance of most of plugins is done by Coq developers themselves (via overlays).
This is true for Coq compatibility but not for bug fixes.
@Enrico Tassi : what you say is true for Elpi, but Ltac2 was intentionally made to mimic Ltac1 (and I guess also to have a low level interface which is close to the OCaml tactic interface).
Indeed it doesn't make sense to cross reference Ltac1 and Elpi in the ref man. But what would make sense in the ref man is to mention that Elpi exists and what its strengths are.
Sure, pointers to Elpi APIs from the Coq manual would make no sense.
I'm arguing that even pointers to Ltac2 APIs make little sense IMO, since:
Then, the link, if sensible, won't hurt. But it really smells like an X Y problem here. I was not present of the call, but it smells like "the doc of Ltac2 is not easy to find/browse/..." which can hardly be fixed by adding pointers from the doc of Coq.
There was the problem however that Ltac2 functions and notations are documented only in the Ltac2 files. To resolve this, couldn't we imagine a script that extract from Ltac2 files triples of tactic name, coqdoc link to the Ltac2 function and coqdoc link to the Ltac2 notation, together with a tag in the rst files which provokes the insertion of the appropriate Ltac2 links in the refman?
This is where the smoke comes from ;-)
Well what I am saying is that we need to do something soon to ensure tactics written in OCaml can be maintained. I have recent experience with this (looking into various sorts of exponential blow up in aac-tactics - my first contact with OCaml tactics - and I didn't find it very pleasant. It took me days to find out how to do things which would be half a line in Ltac2 in OCaml. I mostly went via looking into how things are implemented in Ltac2 and see where this leads ...
But this is getting off topic and I guess we should have a separate thread for "how do we make sure our kids will understand tactics written in OCaml". Adding more OCaml to the Rosetta stone project might btw. also help. I think about providing an OCaml implementation for the reflexive real evaluation tactic I provided - what I learned around the AAC endeavour should be sufficient to do this, but I would appreciate if someone who knows what (s)he is doing would review it then.
I didn't find the OCaml tactic tutorial by @Yves Bertot that helpful btw. I think it is very helpful for writing an OCaml tactic from scratch, but not so much for understanding / extending / fixing existing OCaml tactics.
I was not present of the call, but it smells like "the doc of Ltac2 is not easy to find/browse/..." which can hardly be fixed by adding pointers from the doc of Coq.
IIRC, the original issue at the call was to unify the syntax of cbv
, cbn
, simpl
, lazy
so that all of them could support a pattern (like simpl
) and specific lists of reduction (like the others). It is not fully clear to me why the discussion stumbled at some time, but it was about extending the grammar in plugins/ltac
vs extending the Ltac2 API vs extending the Ltac2 notations (maybe someone has a clearer remembering than me; in particular there are no notes for this call which was held on Feb 12).
To find a way to be able to continue to extend the existing tactics (in tactics.ml
), I concluded that the documentation of tactics (which currently refers to the syntax defined in g_tactic.mlg
, maybe this should be changed?), should also include the corresponding Ltac2 notations and the corresponding Ltac2 typed calls.
Regarding Elpi, which is equally great, it should also be advertized more prominently. Regarding the reference manual for instance, a typical place where elpi should be mentioned is in the Scheme section, since to my knowledge, elpi provides to date the largest toolkit for deriving schemes (ahead of Equations and paramcoq). There are certainly many other places where elpi should be mentioned in the reference manual but I'm not knowledgeable enough to tell where.
In any case, the main message I want to say is that we cannot expect a newcomer to Coq to start from something else than the reference manual, so the reference manual has to give pointers to what else needs to be read.
Last updated: Oct 13 2024 at 01:02 UTC