Karl Palmskog (May 03 2022 at 08:30): Karl Palmskog (May 03 2022 at 08:30):What are the most high-profile applications of Elpi besides HB? Are they packaged in opam?
(Prompted by discussion in mathcomp channel about use of Elpi for Stdpp instances, cc: @Paolo Giarrusso )
Michael Soegtrop (May 03 2022 at 09:23):I like Trakt (https://coq.discourse.group/t/trakt-1-0-released/1558) - a generic form of zify based on Elpi.
Karl Palmskog (May 03 2022 at 12:29):no opam package yet though :cry:
Michael Soegtrop (May 03 2022 at 12:31):You can find a working one here: https://github.com/ecranceMERCE/trakt/issues/3.
Michael Soegtrop (May 03 2022 at 12:32):(I have this in my local patch repo).
Enrico Tassi (May 04 2022 at 07:51):coq-mathcomp-algebra-tactics
Enrico Tassi (May 04 2022 at 07:52):There is some use of elpi in Dx https://gitlab.univ-lille.fr/2xs/dx/-/tree/main
Enrico Tassi (May 04 2022 at 08:41):There is also derive (which comes with coq-elpi, and which we are still improving). It has a paper attached.
In any case I like to link users in the main README of coq-elpi, so if you find more, I'm all ears
Last updated: Oct 13 2024 at 01:02 UTC