Patrick Nicodemus (Mar 19 2023 at 20:26): Patrick Nicodemus (Mar 19 2023 at 20:26):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
Michael Soegtrop (Mar 20 2023 at 08:23):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.
Enrico Tassi (Mar 20 2023 at 08:45):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.
Michael Soegtrop (Mar 20 2023 at 08:53):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.
Karl Palmskog (Mar 20 2023 at 08:54):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.
Théo Zimmermann (Mar 20 2023 at 08:55):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.
Michael Soegtrop (Mar 20 2023 at 09:37):@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").
Michael Soegtrop (Mar 20 2023 at 09:37):But for sure it would make sense to have a consolidated directory of documentation and examples for all packages in Coq Platform.
Enrico Tassi (Mar 20 2023 at 10:26):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