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.
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.
Last updated: Jun 10 2023 at 06:31 UTC