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.

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

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

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

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

I agree that coq-elpi is also an option, since "almost-anything-but-maintaining-a-plugin" is preferable these days

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.

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 !

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.

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

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.

Last updated: Oct 13 2024 at 01:02 UTC