Learning to write Coq plugins - what is the purpose of .mlg files?

Developing plugins
1

Dear Coq Discourse folks,

After recently learning Coq to a level where I feel confident using all of Coqs user features and being able to load and use external plugins, I have come to the conclusion that for some of the personal projects I have in mind it would be a big help if I where to be able to develop some custom tooling of my own. Thus I have taken it upon myself to learn how to write plugins for Coq.

Whilst there are plenty of high quality tutorials on learning Coq from the end-user perspective I’m really struggling to find resources to help me get into writing plugins as they are significantly more sparse. They invariably also assume a degree of familiarity with the internals of Coq that i don’t have knowledge of nor can find adequate resources elsewhere to bridge that gap. Notably the Coq manual itself only touches on plugins with a section of how to depreciate parts of them, which in my opinion is somewhat putting the cart before the horse!

Despite this I have at the least found two resources (in the form of git repos) that I feel I ought to be able to pick at and tweak with to muddle through and bootstrap some sort of understanding on the whole process that will allow me learn from more advanced projects’ sources afterwards. They are as follows:

I can mostly get started by looking into these, but there is one problem, and that is in understanding how .mlg files work, or even what .mlg stands for:

I don’t really understand .mlg files - not can I find any introductions to them in the Coq manual or by searching the internet in general. From the looks of it it seems that it is some shim/wrapper around Ocaml code to get it working together with the Coq kernel.

Does anyone have any good introductory resources for someone to learn to write / how .mlg files work? Ideally I would really want to see a reference to the Grammar of the language that they are written in (even if its just a link to where the parser lives for .mlg files in the coq source code). Thus-far I have only pre-written examples to go on and I am struggling to reverse engineer what is actually happening in these files!

1 Like
2

There is some info in coq/dev/doc/parsing.md at master · coq/coq · GitHub

1 Like
3

There is some kind of misconception. You do not need .mlg files to interact with the Coq kernel, as absolutely none of the the features of the mlg language is related to the kernel. Its only purpose is to make it a bit easier to interact with the Coq parser, that is, to add a new constructs to the surface language.

You can very well write plugins without ever writing a single line of .mlg file. In fact, none of the plugins I wrote uses .mlg files. That being said, I do not recommend this mlg-free approach, unless you have very specific requirements like backward compatibility, as it is quite verbose and low-level.

Just run coqpp on the .mlg file and see what the resulting .ml file looks like.

2 Likes
4

Note that writing plugins should be a last resort today. Before learning how to write them, you probably want to learn how not having to write one. As highlighted in the reference manual Creating new tactics — Coq 8.19.0 documentation nowadays there are quite a few metalanguages that are very effective to do in a much simpler way things that were historically done with plugins. You can look at the Rosetta stone projects for some examples comparing them GitHub - coq-community/metaprogramming-rosetta-stone: A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster] I personally have a good experience with elpi that provides very good starting tutorials. Ltac2 is known to be good too.

5

I understand the need for better documentation. We are trying to work on it GitHub - Zimmi48/platform-docs: A project of short tutorials and how-to guides for Coq features and Coq Platform packages. and we welcome contributions, but it will take some times before we have something comprehensive

1 Like
6

That’s really helpful to know - thank you very much!