Stream: Elpi users & devs

Topic: Elpi applications besides HB


view this post on Zulip 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 )

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 03 2022 at 12:29):

no opam package yet though :cry:

view this post on Zulip Michael Soegtrop (May 03 2022 at 12:31):

You can find a working one here: https://github.com/ecranceMERCE/trakt/issues/3.

view this post on Zulip Michael Soegtrop (May 03 2022 at 12:32):

(I have this in my local patch repo).

view this post on Zulip Enrico Tassi (May 04 2022 at 07:51):

coq-mathcomp-algebra-tactics

view this post on Zulip 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

view this post on Zulip 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: Feb 05 2023 at 14:02 UTC