Follow-up meta task and notes

[tlringer]

Following up from the presentation at CUDW, some TODOs:

1. Type annotations in OCaml and Ltac2 (done)
2. Aligning code side by side to show similarities
3. Implementing other examples besides autoinduct in the other metalanguages
4. Release and crowdsource more solutions? Could be like POPLmark Challenge for metalanguages IMO

Talia's Notes:

1. By far the biggest barrier to plugin development is setup; it would be very nice to have a plugin generator for initial setup.
2. In OCaml, it's very nice to have access to maps and folds over the subterm structure. It would be nice to have map/fold over terms exposed in other metalanguages if it isn't already (though I do wonder what the expressiveness of this is relative to [match!] and so on).
3. I find it easier to organize automation behind interfaces in OCaml so that I can reuse utility functions; has thought gone into this for other metalanguages? In particular, I like being able to put utility functions behind nice .mli files and then just reuse them; I also like having lots of higher-order functions. Examples: 1 2 3 4
4. I wish I could write OCaml inline right in a Coq file. This is a definite plus of all of the other metalanguages.
5. I like being able to swap out different notions of equality and so on trivially in OCaml, and it'd be cool to be able to do that more easily in other metalanguages.
6. Ltac is so limited; fixed numbers of arguments are sad.
7. The OCaml plugin API changes a lot, so one major barrier to plugin development is that the burden of change is difficult (even for things like how to set up plugins, which confused me for this particular development). This is a plus of other metalanguages. (One thing we can track here in this repository is how much we need to change these over time.)
8. Metacoq turned my computer into a furnace when I installed it, as a heads up.
9. I was personally really impressed with the Ltac2 version and how similar it feels to the OCaml one.

Not (yet) covered by the autoinduct example, but relevant to writing automation:

1. Caching for efficiency
2. Fancier equalities and unification
3. Nicely organizing automation in libraries
4. Burden of change (discussed but not yet encountered)

[tlringer]

Feel free to add your own notes here and we can use this to figure out next steps

[SkySkimmer]

Type annotations in OCaml and Ltac2

done for ltac2 autoinduct

[SkySkimmer]

The OCaml plugin API changes a lot, so one major barrier to plugin development is that the burden of change is difficult

The recommended solution is to get the plugin into Coq's CI. It is fine to open a PR with a non-master-compatible plugin to ask for help porting it. The main requirements are responsiveness when changes come from upstream and testing your changes with Coq master before merging them in the tested branch.

NB: the branch tested by Coq doesn't have to be your development branch, it can be a for-CI branch then you can backport upstream changes at your leisure. You can also give merge permissions to Coq devs and tell them they're only allowed to merge to that branch, then you don't have to be responsive.

[tlringer]

@SkySkimmer how far does that stretch back? Like if I have a plugin on 8.9.1, can I still get help porting that? Or does it have to be on a relatively recent Coq still before I can open a PR

[SkySkimmer]

It should be fine, if we start getting spammed with not very useful plugins we could be stricter but restrictions would be more about how useful the plugin is than its starting version.

Also when asking for porting help please be clear about what versions you want to support (eg just master, current release + master, etc), just master will be easiest of course but supporting more versions can be done, eg quickchick using preprocessing https://github.com/QuickChick/QuickChick/blob/6cf6918a5add0e10512f4529719f8fd8a4b605fa/plugin/depDriver.ml.cppo#L248-L252 etc, rewriter using duplicated files https://github.com/mit-plv/rewriter/tree/master/src/Rewriter/Util/plugins

[tlringer]

Thanks, that is amazing, will take advantage of that soon.

Just added type annotations to the OCaml.

[tlringer]

Thanks, that is amazing, will take advantage of that soon.

Just added type annotations to the OCaml.

[gares]

4. Could be like POPLmark Challenge for metalanguages IMO

I love this idea, but I think we need to separate the goals:

• some exercises must be easy, a sort of playground for explaining your language/approach
• some exercises more challenging, allowing for "scientific" comparison. E.g. a proper benchmarking (I'm thinking at Michael's simplifier)

I guess accumulating here more and more exercises is anyway a good start.

[SkySkimmer]

By far the biggest barrier to plugin development is setup; it would be very nice to have a plugin generator for initial setup.

I guess it could be based on https://github.com/coq-community/coq-plugin-template ?