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.
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
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
Both are interesting points. But if your metaprogram lives in a logic monad with side effects, how well can you avoid the latter problem?
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?
it certainly is the case that you trade off learning curves: HOAS vs de Bruijn, and logic programming vs logic monads vs lacking backtracking.
so I guess the "assembly" comparison only applies to actually constructing terms in TemplateCoq :sweat_smile:
@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
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 dis 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 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
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
unshelve - I never tried this though
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.
@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.
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
@Yannick Forster : We could also put together an interest group and set up a dedicated online meeting.
Feel free to use the wiki (in particular a page that would be linked from here) to coordinate.
That's a great idea @Michael Soegtrop :)
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?
Maybe "mega-programming rosetta stone"?
I know no mtac2 at all, but we can try to ping @Janno
But sure, very happy to for now take on the MetaCoq part
Also ping to @Louise Dubois de Prisque because we talked about similar ideas in the past
Sure, I can do the Mtac2 part!
I would be really interested in this project, as I have experienced metaprogramming in Elpi, Ltac and MetaCoq
Maybe "mega-programming rosetta stone"?
I guess you meant meta-programming :wink:
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.
@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?
@Michael Soegtrop Definitely! Feel free to add such a link.
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.
Time will tell ...
I created the link in the "index side bar"
I can cover ocaml as well
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 ;-)
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.
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.
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.
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.
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.
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.
@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.
A Rosetta stone to help move away from Ltac1 might still help
Even if it might be a very different project
@Paolo Giarrusso : indeed this is the only reason to include it.
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).
I guess right now some people are on vacation, so we should probably have a first meeting sometime early September.
@Kenji Maillard : a nice example - instructive and not too complicated.
Last updated: Jan 29 2023 at 18:03 UTC