Julin Shaji (Jul 28 2022 at 10:41): Julin Shaji (Jul 28 2022 at 10:41):If one were to compare metacoq and elpi, what could be the pros and cons?
Paolo Giarrusso (Jul 28 2022 at 12:26):EDIT: IIUC, coq-elpi is much higher-level than template Coq — to generate code, you can write source-like "Coq terms" and call type inference on them, use ltac1, etc etc. The tutorials are really nice.
Karl Palmskog (Jul 28 2022 at 12:28):some would call it: "much lower level"
Paolo Giarrusso (Jul 28 2022 at 12:29):you mean elpi?
Karl Palmskog (Jul 28 2022 at 12:30):yes, compared to MetaCoq
Karl Palmskog (Jul 28 2022 at 12:31):the abstraction level in MetaCoq is mostly Coq, which to me is a high-level calculus. In contrast, Elpi seems to provide very low-level access to a range of functions in the Coq system, rather than just the calculus
Paolo Giarrusso (Jul 28 2022 at 12:31):I have not used template Coq, but colleagues have, and IIUC you need to produce elaborated terms with it. Including universes — I don't know if that changed.
Karl Palmskog (Jul 28 2022 at 12:32):do you consider universes low-level details?
Paolo Giarrusso (Jul 28 2022 at 12:32):I consider the source language of elaboration higher-level than the target language.
Karl Palmskog (Jul 28 2022 at 12:34):OK, so I guess Elpi can access some higher-level language features, but I think it still exposes the full elaboration chain?
Paolo Giarrusso (Jul 28 2022 at 12:35):I'd say think elpi exposes the elaboration chain and metacoq doesn't?
Paolo Giarrusso (Jul 28 2022 at 12:35):I think you should be able to write something closer to the "target language" also in elpi, but I haven't tried; and coq-elpi does not give you full control over the output ASTs, which could be a concern for advanced users
Paolo Giarrusso (Jul 28 2022 at 12:36):or at least, I've seen the advanced user PMP raise such a concern here
Paolo Giarrusso (Jul 28 2022 at 12:37):_my_ experience with elpi was that I could pick it up in a few hours just from examples and docs, I even skipped the tutorials — it was just that easy to use.
Paolo Giarrusso (Jul 28 2022 at 12:39):But I had already used HOAS, basics of Prolog, and even Twelf, so it might not be the universal experience...
Karl Palmskog (Jul 28 2022 at 13:42):there are essentially two primary concerns:
Both MetaCoq and Elpi are likely to have a good maintenance trajectory (OCaml has a terrible one), but with Elpi you will have to know both Coq and some of its internals like elaboration and Lambda-Prolog. So absent other specialized knowledge and requirements, writing regular Coq [in MetaCoq] to do an extension probably has an edge.
Karl Palmskog (Jul 28 2022 at 13:45):it would be nice if we had some comparison points, so one could get an idea of: if I want to do X, then Y is better suited
Karl Palmskog (Jul 28 2022 at 13:46):but in general, I will just try to say to anyone who wants to extend Coq and listens: please use either MetaCoq or Coq-Elpi, so we have a chance of seeing your code not bitrot immediately and thus possibly be functional in a year or two
Yannick Forster (Jul 28 2022 at 15:58):I'd be very excited to start a project where we find a nontrivial but easy enough plugin to write in Elpi, MetaCoq, Ltac2 and maybe Mtac2, and use that to give a "unified" hello-world style tutorial (whatever that means exactly) to all 4 options, plus maybe some insights regarding pros and cons. The huge excitement is balanced by a severe lack of time, but whoever else is excited: Please get in touch!
Enrico Tassi (Jul 28 2022 at 16:06):About high leve / low level: my take is that de Bruijn indexes are lower level than HOAS and writing fully elaborated terms can be substantially more work than manipulating terms with holes and call the elaborator when you like, to infer holes and universe constraints for example. In that sense Elpi is more high level than ocaml or metacoq which essentially manipulate the same terms.
Paolo Giarrusso (Jul 28 2022 at 18:28):@Yannick Forster does MetaCoq let you call elaboration, universe inference or Ltac today?
Paolo Giarrusso (Jul 28 2022 at 18:33):with Elpi you will have to know both Coq and some of its internals like elaboration and Lambda-Prolog.
That sounds... backwards again. If we use an analogy to compilation, you're basically claiming that assembly is higher level than OCaml because generating a binary with OCaml requires using OCaml internals like "call the compiler to translate OCaml to assembly" — where the compiler plays the role of elaboration.
Paolo Giarrusso (Jul 28 2022 at 18:34):Elpi lets you generate source Coq terms (which I'm comparing with OCaml), which elaboration translates to kernel terms (which I'm comparing to assembly), while Template-Coq lets you write kernel terms directly.
Paolo Giarrusso (Jul 28 2022 at 18:35):@Yannick Forster am I missing something on the Template-Coq side?
Yannick Forster (Jul 28 2022 at 18:36):I can give more detailed info tomorrow. Quickly: Elaboration no, universe inference for inductives yes but in terms no, ltac yes but not documented
Enrico Tassi (Jul 28 2022 at 20:36):Paolo Giarrusso said:
But I had already used HOAS, basics of Prolog, and even Twelf, so it might not be the universal experience...
That is cheating, Twelf "transliterates" to Elpi ;-) Good for you!
Enrico Tassi (Jul 28 2022 at 20:56):@Karl Palmskog one was to see it: how much of the pain is taken care of by the language, via its runtime or APIs or other language features. Eg, memory handling is easy if your language has a GC, of if you can kind of implement it via smart pointers (a la C++/rust).
The runtime of of Elpi takes care of the "Logic Monad" you have in OCaml (a bit like Ltac2): you don't pass around the evar map (the state of evars and universes) nor the continuations/alternatives if you need to backtrack. So, if you are not allergic to monads (like me) these 3 languages are equivalent w.r.t. this. This point is moot, for now, in TemplateCoq, since evars are not yet a thing, IIRC. I'm not sure about Mtac2, maybe @Janno can complement this info, I believe it handles evars transparently, but I don't know about backtracking.
The runtime of of Elpi takes care of binders (shifting/substitution) so you don't see a De Bruijn index/level, never. I believe Mtac2 is super close to that (same ideas from HOAS transposed to functional programming). I believe in Ltac2 the AST has variables as numbers, but you can play with quotations/antiquotations to avoid most of the times the pain. I don't know if this trick applies to TemplateCoq, but I don't think so. In OCaml we have no support for that (we had the quotation/antiquotation trick a long ago) but we could use an API in the style of bindlib to hide indexes and impose a coding style very close to the one of Elpi/Mtac2 w.r.t. crossing binders. They do so in lambdapi (dedukti) and the code looks nice to me.
Elpi and Ltac2 have support for quotations/antiquotations to write code (data) using Coq's syntax/parser. I believe Mtac2 also lets you use Coq's syntax (since the object language and meta language are kind of mixed). TemplateCoq has a quotation/antiquotation mechanism, but I don't think you can mix/nest the two languages, please correct me if I'm wrong.
Elpi has a quite sophisticated FFI for OCaml, so binding Coq's internals as Elpi's APIs is easy, and hence one can access almost everything and script the vernacular (programmatically open sections, modules, declare implictis, coercions...). I believe Ltac2 has a good FFI (and fast by design), but I don't see many Coq internals exposed, dunno why. I've no clue how hard it is to bind a primitive in Mtac2 or TemplateCoq. I know the latter has a writer monad to add inductives/definitions to the environment, but I don't think it has many more effects than these.
And given this message is biased ;-) I must mention that Elpi has => (implication) which is the best thing after sliced bread, but you really need a logic programming language for that and explaining it without that background is too hard, so you will have to believe me ;-)
Enrico Tassi (Jul 28 2022 at 21:24):An aspect I forgot to talk about is FFI for other languages. Elpi has a minimalistic one for ltac1. Ltac2 has a more complete one for ltac1 I believe. TemplateCoq can apparently call ltac1. I've no clue about Mtac2. Ltac1 can call anything which can implement a tactic, I believe.
Karl Palmskog (Jul 28 2022 at 21:36):I think my point was kind of simple and naive: MetaCoq is by definition programming Coq in Coq, so there is no additional language to learn, just a Coq API of sorts. But it's always helpful with more details, and I hope some of this eventually makes it to some MetaCoq/Elpi/Ltac2/Mtac2 comparison documentation/code
Karl Palmskog (Jul 28 2022 at 21:41):the key annoyance for me personally with any Prolog (which may bias me against Elpi) is the execution model: in the ideal, all your predicates are actually really predicates, and evaluation takes care of itself predictably. In practice, you will have to know tons of details about the runtime for side-effecting stuff that gets your work done
Paolo Giarrusso (Jul 28 2022 at 21:59):Both are interesting points. But if your metaprogram lives in a logic monad with side effects, how well can you avoid the latter problem?
Paolo Giarrusso (Jul 28 2022 at 22:02):I imagine that logic monads might be optional in some applications — but probably only if you never rely on elaboration, since the latter can itself backtrack?
Paolo Giarrusso (Jul 28 2022 at 22:03):it certainly is the case that you trade off learning curves: HOAS vs de Bruijn, and logic programming vs logic monads vs lacking backtracking.
Paolo Giarrusso (Jul 28 2022 at 22:07):so I guess the "assembly" comparison only applies to actually constructing terms in TemplateCoq :sweat_smile:
Paolo Giarrusso (Jul 28 2022 at 22:20):@Karl Palmskog and to disable backtracking, std.do! is a nice idiom https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html#pitfalls . but here I cheated by following examples
Enrico Tassi (Jul 29 2022 at 04:54):I totally get your POV Karl, having to learn a new language may be scary. My pitch there is that you have already been doing it for DSLs in most PL and you did not regret it. Eg you did learn regular expressions because matching text with for loops is too painful and becomes much simpler with regexps. To me Elpi is a DSL for term manipulation, not a general purpose language. I'm stretching it a bit, but not too much I hope. I promise, I won't write a web server in Elpi ;-)
Yannick Forster (Jul 29 2022 at 07:09):Yannick Forster said:
I can give more detailed info tomorrow. Quickly: Elaboration no, universe inference for inductives yes but in terms no, ltac yes but not documented
If mind is the representation of an inductive type tmMkInductive true mind defines this inductive type and runs universe inference on it.
And I wrote up my (admittedly slightly hacky, but working) way of solving goals using Ltac here: https://github.com/MetaCoq/metacoq/wiki/Calling-Ltac-from-the-TemplateMonad/ It only works for solving goals, but probably for defining a tactic which is not solving one can work with shelve and unshelve - I never tried this though
Théo Zimmermann (Jul 29 2022 at 08:15):I'd like to emphasize that we have a section in the refman called "Writing Coq libraries and plugins" and that for now, it contains a link to the plugin tutorial (in OCaml), but does not even mention using Coq-Elpi, Template/MetaCoq or whatever. This might be worth adding if we want people to use these languages instead of the OCaml API.
Michael Soegtrop (Aug 08 2022 at 08:12):@Yannick Forster : if you start such a "Rosetta stone" project, I could contribute the Ltac2 part - and maybe the Ltac part (a bit rusted). I guess we should start with a list of people who would like to contribute the solution in various languages.
I am not sure how synced the developments should be. One could make the implementations pretty close, so that one can compare them easily, but this would not emphasize the advantages and disadvantages of various languages. So maybe one should have (for some languages) two solutions - one which follows as much as possible the same implementation path, and one which uses the respective language in the best way.
Yannick Forster (Aug 08 2022 at 09:08):The biggest open question for me here is what the non trivial but also not too tricky example is. Where individual solutions can shine in their strengths, but also reasonably expose their weaknesses. Maybe we should set up a discussion or brainstorming session about that around a CUDW or similar workshop
Michael Soegtrop (Aug 08 2022 at 09:14):@Yannick Forster : We could also put together an interest group and set up a dedicated online meeting.
Théo Zimmermann (Aug 08 2022 at 09:16):Feel free to use the wiki (in particular a page that would be linked from here) to coordinate.
Yannick Forster (Aug 08 2022 at 09:18):That's a great idea @Michael Soegtrop :)
Michael Soegtrop (Aug 08 2022 at 09:28):Would "Topic Working Group: Tactic language Rosetta stone" be an appropriate title for the Wiki page?
@Yannick Forster : Would you handle the MetaCoq and Mtac2 part? If not, whom should we ask?
@Enrico Tassi : would you handle the Elpi part? If not, whom whould we ask?
Assuming I am doing Ltac2 and Ltac, I think only OCaml is missing. Whom could we ask there? @Yves Bertot : since you did the existing plugin tutorial, would you take the OCaml part?
Yannick Forster (Aug 08 2022 at 09:28):Maybe "mega-programming rosetta stone"?
Yannick Forster (Aug 08 2022 at 09:28):I know no mtac2 at all, but we can try to ping @Janno
Yannick Forster (Aug 08 2022 at 09:29):But sure, very happy to for now take on the MetaCoq part
Yannick Forster (Aug 08 2022 at 09:29):Also ping to @Louise Dubois de Prisque because we talked about similar ideas in the past
Janno (Aug 08 2022 at 09:39):Sure, I can do the Mtac2 part!
Louise Dubois de Prisque (Aug 08 2022 at 09:46):I would be really interested in this project, as I have experienced metaprogramming in Elpi, Ltac and MetaCoq
Théo Zimmermann (Aug 08 2022 at 11:21):Maybe "mega-programming rosetta stone"?
I guess you meant meta-programming :wink:
Michael Soegtrop (Aug 08 2022 at 13:23):I created the Wiki page.
@Yannick Forster @Janno @Louise Dubois de Prisque : please put in your names in the languages you want to contribute - I wouldn't hurt to have more than one contributor for each language.
Michael Soegtrop (Aug 08 2022 at 13:25):@Théo Zimmermann : would it make sense to have a link on the working groups page in the main links shown on each page on the right?
Théo Zimmermann (Aug 08 2022 at 13:26):@Michael Soegtrop Definitely! Feel free to add such a link.
Théo Zimmermann (Aug 08 2022 at 13:27):BTW, there are chances that this project will quickly outgrow a single Zulip topic, so it could make sense to create a dedicated Zulip stream as well.
Michael Soegtrop (Aug 08 2022 at 13:52):Time will tell ...
Michael Soegtrop (Aug 08 2022 at 13:55):I created the link in the "index side bar"
Enrico Tassi (Aug 08 2022 at 14:04):I can cover ocaml as well
Enrico Tassi (Aug 08 2022 at 14:06):For Elpi, also @Kazuhiko Sakaguchi , @Cyril Cohen , @Pierre Roux, @Gordon Stewart (@Gordon Stewart ) and @Enzo Crance are good choices. While I'm happy to do it myself, I'm even more interested in seeing how other would do it ;-)
Enrico Tassi (Aug 08 2022 at 15:12):Yannick Forster said:
The biggest open question for me here is what the non trivial but also not too tricky example is. Where individual solutions can shine in their strengths, but also reasonably expose their weaknesses.
I think it will be hard to find one example, if only because commands and tactics are somewhat different beasts (e.g. in a tactic you don't need to synthesize an inductive declaration or open a module, for example).
If we focus on tactics, then a very common example is reification: since you can't do it in Coq itself, so you have to work at the meta level.
If we look at commands, something I've seen implemented in many languages/systems is the parametricity translation. It already exists in template-coq, coq-elpi, ocaml (and Lean) for example. It is not too intricate if one fixes, once and forall, that he wants the, say, binary one (the n-ary case is a trivial extension, but the one kind which makes things just less readable). This is also a case were one cannot do it in Coq itself, so a meta language is truly needed.
Enrico Tassi (Aug 08 2022 at 15:21):If I had to introduce a third category (but as of today it would be too biased toward Elpi), is vernacular scripting. Something like mlock would be perfect, but I'm afraid this is not possible (yet) in most of the languages.
Michael Soegtrop (Aug 08 2022 at 16:25):When would be a good time for a meeting to discuss the example(s)?
I would btw. appreciate an extensible plugin, something like ring, which also shows how to add user defined structures.
Louise Dubois de Prisque (Aug 09 2022 at 08:18):From my experience, a difficult part while programming Coq plugins (I my PhD I am mostly interested in tactics), is to make different tactics interact together. Once we are in the "reified world", if we are familiar with the meta-programming language the implementation is often not too hard, but if we need to get information from the local context, assert new hypothesis and then go back to reified Coq terms, or mix it with some Ltac, this can become tricky very quickly because of side effects. Maybe that I am not familiar enough with all the evaluation mechanisms at stake but I think that most meta-programming languages were thought and designed in a way that supposes that the user uses the reification mechanism only once, codes everything in the language and then goes back to the unquoted world. I don't know if this aspect could be interesting for this project but I think this can show some weaknesses or at least difficulties with meta-programming tools.
Enzo Crance (Aug 09 2022 at 08:28):I second this. When writing tactics, I usually do everything at the meta level, querying the Coq environment to get information (in read-only mode it's usually OK), and then perform one single call to a refine API that applies the big proof. I wonder how this would work if I had to combine several different tactics into one using the meta-language. If Ltac is good at anything, it probably is for this precise task, but I have no idea how to make it work nicely in other meta-languages.
Enrico Tassi (Aug 09 2022 at 14:42):A huge problem when using ltac1 is that very little in the APIs or in the language helps to pass data around. In some way this makes "tactics" not the right building block to organize your code, since they can't pass data around easily. In ltac1 one can pass Coq terms, and that is all. It is not uncommon to add a dummy context entry to "remember" you already did something. Another way to say that is that ltac1 forces to store the state of your tactic in the goal.
This is why, IMO, combining ltac1 tactics is hard. While if you stay within the same (non ltac1) language, then you have much more freedom and you can combine "functions" (or "predicates") as you like, and craft and carry your own state.
Michael Soegtrop (Aug 09 2022 at 14:55):@Enrico Tassi : In my experience all this is dramatically improved in Ltac2.
IMHO Ltac1 is obsolete - I am not sure one should even include it in the Meta Programming Rosetta Stone project - I would discourage people to use it for anything except manual step by step proof scripts.
Paolo Giarrusso (Aug 09 2022 at 18:37):A Rosetta stone to help move away from Ltac1 might still help
Paolo Giarrusso (Aug 09 2022 at 18:37):Even if it might be a very different project
Michael Soegtrop (Aug 10 2022 at 07:47):@Paolo Giarrusso : indeed this is the only reason to include it.
Kenji Maillard (Aug 16 2022 at 14:13):I'm a bit late to the discussion but I would also be interested in joining in. I've been thinking about using MetaCoq for boilerplate generation for over 2 years (mostly inspired by syntactic gadgets I liked when using F*) but just made it public now (the code is still in an early stage but that might inspire someone).
Michael Soegtrop (Aug 16 2022 at 15:18):I guess right now some people are on vacation, so we should probably have a first meeting sometime early September.
Michael Soegtrop (Aug 16 2022 at 15:20):@Kenji Maillard : a nice example - instructive and not too complicated.
Yannick Forster (May 22 2023 at 15:56):Does it make sense to kick-start a Meta-programming Rosetta Stone Project at this year's CUDW happening in 4 weeks? @Michael Soegtrop do you plan to come?
Michael Soegtrop (May 22 2023 at 17:46):@Yannick Forster : I am quite busy and don't plan to come, but I am available online and can contribute Ltac, Ltac2 and Elpi for some given cases. It would definitely be a good thing to get started with.
Kazuhiko Sakaguchi (May 23 2023 at 19:08):That's convenient for me. I can contribute on the Elpi side.
Enzo Crance (May 24 2023 at 07:46):I would also be interested in contributing on the Elpi part if it helps.
Michael Soegtrop (May 24 2023 at 11:47):OK, it is settled then. I would suggest that we do many small snippets, but also a few more complex larger examples.
Enrico Tassi (May 24 2023 at 12:29):That seems a very nice topic for the CUDW, maybe we can do a brainstorming session with Michael attending remotely to get a good list of problems, and then we spend the rest of the time to find nice solutions to these.
Enrico Tassi (May 24 2023 at 12:31):I'm more than happy to contribute to the Elpi bandwagon, but I'd be even more proud if others do, thanks @Enzo Crance @Kazuhiko Sakaguchi ;-)
I prefer to be around to fix the bugs / api / doc which gets in the way.
Enzo Crance (May 24 2023 at 13:16):Just to be precise, I will not be there physically either, but can make myself available for various meetings or coding sessions on the topic. :smile:
Yannick Forster (Jun 24 2023 at 15:47):@Michael Soegtrop would you be interested and available say on Monday afternoon to jump on a zoom call with the people attending in Sophia? If not we can keep you in the loop closely, but probably for a brainstorming session it would be interesting to have you
Patrick Nicodemus (Jun 24 2023 at 19:52):I admit that this is off topic but I am a mathematician and I have struggled finding ideas for how I can use tactics and automation to eliminate mundane and verbose proof scripts. It seems that much of the discussion around automation has been around PL and manipulating syntax trees of object languages. I would love it if the meetup could discuss ways to automate routine proofs in algebra or analysis, for example suggest ideas for a plugin to help math-comp developers. It is unfortunately very difficult for me to look at reasoning about separation logic or imperative programming and come away with good transferable ideas for mathematics.
Karl Palmskog (Jun 24 2023 at 19:56):I think an underrated problem is also nontrivial combination of advanced tactics. There is for example Itauto that is able to do the Nelson-Oppen combination of lia and congruence in propositional reasoning, but [the Nelson-Oppen stuff is] not ready for large-scale use yet according to author.
Paolo Giarrusso (Jun 24 2023 at 20:01):Patrick: yeah, "elegant" mathematical proofs strive to avoid most syntactic reasoning. But that question seems somewhat separate from "what metaprogramming tooling to use" — assuming metaprogramming is needed at all!
Paolo Giarrusso (Jun 24 2023 at 20:02):Tho most automation must manipulate Coq syntax trees at least a bit. Even proof by reflection (like used by lia) must convert the goal to some object language.
Michael Soegtrop (Jun 26 2023 at 07:12):@Yannick Forster : sure I am available today and most of the week for calls. Today I have another meeting 1..2 PM Paris time, but otherwise I am available.
Michael Soegtrop (Jun 26 2023 at 07:15):@Patrick Nicodemus : I am mostly doing analysis and linear algebra in Coq and most of the automation I do is in this direction. I would say there are good examples for tactics in this area (lra, field, coq-interval).
Kazuhiko Sakaguchi (Jun 26 2023 at 08:31):Hello. I gave up attending the CUDW in person for some reason, but I should be available for video calls. Sorry about that.
Enrico Tassi (Jun 26 2023 at 09:00):What about a call at 4PM? I'll find a room here for the ones interested
Enrico Tassi (Jun 26 2023 at 10:53):I booked a video room in the Kahn building, I guess I will communicate the coordinated in the CUDW stream
Last updated: Dec 07 2023 at 06:38 UTC