Elpi is ~7-8 years old at this point, right? It seems like it is fairly mature and "production-ready."
Would it be a good idea to add Elpi in the coq documentation in the "Creating New Tactics" section alongside Ltac and Ltac2?
P.S. Just want to say that I know nothing about logic programming and have been rapidly adjusting over the past few days. It is equal parts frustrating and rewarding. Very cool language. :D
I am not sure - Mtac2 is e.g. also not included in the documentation. The Coq documentation includes only things which are part of Coq itself (live in the Coq git repo). But it would not hurt to have a list of "other tactic languages" with links in the manual.
Indeed I wanted to submit a PR, but the @Michael Soegtrop you had the idea of a working group to identify the pros/cons of each language, and I told myself that the output of that working group would be the perfect contents for that section of the refman.
The point being that just listing alternatives is already covered by awesome Coq.
I hope I have a bit more time for projects like the "tactic languages Rosetta stone" in the near future - in the past half year keeping Coq Platform CI alive pretty much consumed all my extra time.
Enrico Tassi said:
Indeed I wanted to submit a PR, but the Michael Soegtrop you had the idea of a working group to identify the pros/cons of each language, and I told myself that the output of that working group would be the perfect contents for that section of the refman.
The point being that just listing alternatives is already covered by awesome Coq.
Unfortunately, Awesome Coq does not have the ambition to list all possible alternatives, just the alternatives that are popular/impactful/unique enough, which may be a single one.
In fact, we'd be violating the "awesome list" guidelines/rules if we started to list everything in some area.
Michael Soegtrop said:
I am not sure - Mtac2 is e.g. also not included in the documentation. The Coq documentation includes only things which are part of Coq itself (live in the Coq git repo). But it would not hurt to have a list of "other tactic languages" with links in the manual.
First of all, that's not true: Mtac2 is listed here (as an external link), so Coq-elpi should as well: https://coq.inria.fr/refman/proofs/creating-tactics/index.html.
Second, I think if we want users to start considering the Coq Platform the "enhanced / new stdlib", we should improve documentation consolidation on a central official website.
@Théo Zimmermann : sure - as I said Elpi should be mentioned in the Coq reference manual, but I don't think the documentation of Elpi belongs into the reference manual. I interpreted the request of @Patrick Nicodemus this way ("alongside Ltac and Ltac2").
But for sure it would make sense to have a consolidated directory of documentation and examples for all packages in Coq Platform.
Théo Zimmermann said:
First of all, that's not true: Mtac2 is listed here (as an external link), so Coq-elpi should as well: https://coq.inria.fr/refman/proofs/creating-tactics/index.html.
Ah, I did not see that. Here it is: https://github.com/coq/coq/pull/17409
Last updated: Oct 13 2024 at 01:02 UTC