Stream: Ltac2

Topic: Ltac2 Commands?

view this post on Zulip Gregory Malecha (Feb 14 2024 at 14:38):

Has anyone considered using Ltac2 to implement vernacular commands? The current effects built into the Ltac2 language may make this sort of thing difficult, but we have found a lot of value in writing vernaculars at BedRock Systems and it seems like the low-level infrastructure that Ltac2 provides could lower the cost of this.

view this post on Zulip Michael Soegtrop (Feb 14 2024 at 14:52):

Elpi might be more suitable for this - there is even a tutorial

view this post on Zulip Gregory Malecha (Feb 14 2024 at 16:14):

I agree that Elpi is pretty good at this. And you can also do some of this stuff in MetaCoq with the template monad. But it also feels fairly fragmented. Cross-talk between these languages is pretty difficult. The ML-core of Ltac2 seems like it provides a nice core that could be used beyond tactics and would allow sharing logic easily between tactics and commands.

view this post on Zulip Andres Erbsen (Feb 14 2024 at 16:34):

I would also be interested in this. Jason and I have pushed transparent_abstract and so on the the limit already and having access to a wider API without pulling in yet another language would be great.

view this post on Zulip Michael Soegtrop (Feb 14 2024 at 17:07):

Indeed cross calling capability between Elpi and Ltac2 would be very nice. Some things are natural to do in a relational language, other things are natural to do in a functional language.

view this post on Zulip Enrico Tassi (Feb 14 2024 at 21:19):

In case the Ltac2 guys want to add vernac scripting facilities, I'm happy to share code for making the Coq inductive type declaration API usable. There is substantial work in Elpi make it possible to declare an inductive type "easily", the Coq APIs are just crazy there. Of course Elpi exposes an HOAS representation of the inductive, that may not fit well Ltac2, but there is some middle ground where the data is still in low level format (like Ltac2 terms) but in a reasonably organized package (like the parameters, the indexes, the sort, the constructors, the implicits...). I have baked my own code, but I would be happier to share that with Ltac2 or any other meta language, and benefit from any improvements.

Last updated: Oct 12 2024 at 13:01 UTC