Luc Chabassier (Jul 19 2022 at 09:53): Luc Chabassier (Jul 19 2022 at 09:53):Hi everyone,
As part of my PhD, I am developing a coq plugin that tries to automate the usually trivial parts of commutative diagrams reasoning for Coq. I just released the first version on the coq opam repository as coq-commutative-diagrams recently (for nix users there is also a flake). As of now it is pretty basics and only support the coq-hott category library, but I am in the middle of a refactoring that should allow supporting multiple libraries easily. You can find the code on github.
If anyone is willing to give it a try, I'd be happy to get some feedback and suggestions for improvements.
Karl Palmskog (Jul 19 2022 at 09:54):hi @Luc Chabassier the recommended way to make announcements about plugins and other Coq packages is via our Discourse forum: https://coq.discourse.group/c/announcements/8
These will then be cross-posted into the Zulip
Karl Palmskog (Jul 19 2022 at 09:57):as you probably know by now, a plugin is going to need constant updates as Coq evolves. To get this, I believe you already got advice to add the plugin/repo to Coq's CI. But another option these days is to port the plugin to use MetaCoq, which recently had its 1.0 release: https://github.com/MetaCoq/MetaCoq
Here is one example of a MetaCoq-based plugin https://github.com/vzaliva/coq-switch
Karl Palmskog (Jul 19 2022 at 10:00):also, maybe you have seen the large number of category theory libraries in this thread: https://coq.discourse.group/t/survey-of-category-theory-in-coq/371
In particular, this one seems to be popular: https://github.com/jwiegley/category-theory
Enrico Tassi (Jul 19 2022 at 14:12):You can also port it to coq-elpi :grinning_face_with_smiling_eyes: , it did grow quite substantially since the last time you used it
Karl Palmskog (Jul 19 2022 at 14:24):I agree that coq-elpi is also an option, since "almost-anything-but-maintaining-a-plugin" is preferable these days
Théo Zimmermann (Jul 19 2022 at 16:00):Anyway, this was already in Karl's message, but if you keep the plugin in OCaml, you should definitely add it to Coq's CI to get the free upgrades every time breaking changes are made in the Coq API.
Luc Chabassier (Jul 19 2022 at 21:05):I'm not sure coq-elpi is a good fit for the kind of algorithm I'm writing ^^ I'm planning a big refactor anyway, so I'll have a look at metacoq. Depending on the direction it takes I'll add it to the CI, thanks for the pointer !
Enrico Tassi (Jul 20 2022 at 08:19):Sure, I was just pushing Karl to say what I couldn't agree more with: write OCaml only if your main concern is speed. And even then, only if you are truly desperate for cpu cycles, since even a high level language like elpi is typically fast enough.
Pierre Roux (Jul 20 2022 at 08:23):Couldn't calling an OCaml library be another legitimate use case? (to retrieve some witness in a reflexive tactic for instance)
Is there a way in elpi to call some external tool?
Enrico Tassi (Jul 20 2022 at 08:29):Hum, not "streamlined for Coq" in the sense that you have APIs to run an external command and read a file but that is a bit too low level IMO to be recommended.
But if someone has a use case in mind, I'm happy to think about a better API for this use case.
Pierre Roux (Jul 20 2022 at 08:30):I was thinking about the plugin of validsdp (but smtcoq is probably in a similar situation)
Enrico Tassi (Jul 20 2022 at 08:31):You mean, you want to call OCaml code directly?
Pierre Roux (Jul 20 2022 at 08:34):That's what we are doing in validsdp: calling the OSDP OCaml library, that itself calls external solvers. But we could indeed make a standalone executable. We would then need a simple language at the interface (something to encode simple OCaml inductive types). Do we have something in elpi to parse back lisp expressions or something like that?
Karl Palmskog (Jul 20 2022 at 10:03):I agree, in plugins you can even do crazy stuff like linking in C/C++ libraries. But the maintenance price you (and your users) pay can be huge
Bas Spitters (Jul 21 2022 at 10:53):Exciting! Please make sure to announce it on hott zulip too.
Is there a particular algorithm you've implemented? It would be good to document it.
I'm curious about which proofs in the HoTT library you manage to simplify, especially since @Jason Gross, who was the main authors of that cat th library, is very keen on automation.
Julin S (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 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 don't know about Mtac2, maybe @Janno can complement this info.
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. 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, so binding Coq's internals as Elpi's APIs is easy, and hence can access almost everything and script the vernacular (programmatically open sections, modules, declare implictis, coercions...). I believe Ltac2 has a good FFI, 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 ;-)
Last updated: Jan 29 2023 at 19:02 UTC