This is a coq plugin that allows a user to do the diagrammatic reasonnings parts of categoretical proofs in a graphical manner. It can analyze the proof context to deduct the categorical diagram being working on, to display it and enable a graphical way to progress the proof.
This tool is split in two parts. The most important one, the interface itself, is a standalone program that handles displaying the graph and acting on it. It interacts with the proof assistant with an homemade protocol over its stdin/stdout. Then there is a Coq plugin, that analyze the Coq goal and exposes features and information from Coq to the interface through the protocol.
The Coq plugin is also responsible for starting the interface, and thus it must
be able to find it. If there is a COMDIAG_ENGINE environment variable, it
assumes it contains a path to the interface. Otherwise it looks for a
commutative-diagrams-engine in $PATH.
Note
Since this plugin is made of maby moving parts in different languages and ecosystem, only the nix installation method is supported for now.
Using Nix is the easiest way to quickly try the plugin if you have nix installed and flakes enabled. Simply run the following command:
nix develop "github:dwarfmaster/commutative-diagrams#unimath-user"This will drop you in a shell with the right coq version installed, and
OCAMLPATH, COQPATH and COMDIAG_ENGINE setup the right way.
The, you need to copy the
Loader.v
to UniMath/CategoryTheory/CommutativeDiagrams.v and add
CommutativeDiagrams.v to the UniMath/CategoryTheory/.package/files. You can
now build UniMath using make.
Once this is finished, you can open any file in your UniMath clone, import the plugin with:
Require Import UniMath.CategoryTheory.CommutativeDiagrams.And use the tactics as described in the usage section.
Warning
For some reason this is broken for now.
Once the installation has succeeded, you can use the following to make the tactic available in the Coq file you're developping:
From CommutativeDiagrams Require Import Loader.Warning
Right now the nix option is only available on linux due to the way I wrote the nix file.
Note
Nix is packaged in many distributions. If it is not for your distribution, see here for installation instruction.
Using Nix is the easiest way to quickly try the plugin if you have nix installed and flakes enabled. Simply run the following command:
nix develop "github:dwarfmaster/commutative-diagrams#user"This will drop you in a shell with the right coq version installed, and
OCAMLPATH, COQPATH and COMDIAG_ENGINE setup the right way. You can then
start coqide from this shell and use it to edit any file you're interested in.
If you want to use other interfaces like proof-general, you can use the direnv integrationg of Emacs/VScode to have them load the flake automatically.
Note
If you're not using nix to install this plugin, the installation is a lot more complicated. You need to make sure you have a recent enough rust version, a recent enough dune version, and the right system packages installed.
The interface is written in rust and packaged using cargo. You can install it using:
cargo install --git https://github.com/dwarfmaster/commutative-diagrams.gitThe directory it will be installed in depends of your setup. On Linux, by
default, it is installed in $HOME/.cargo/bin. Wherever it actually ends up,
the cargo install command should warn you of which directory to add to the
path to be able to run the command.
The plugin is written in OCaml and can be installed using opam.
Warning
Due to a bug in Coq under linux, installing unimath with opam will fail until coq 8.18 is out (and I have ported the plugin to it). Until then please use nix to install coq and unimath. As such I haven't been able to fully test to following procedure.
First you need to add the coq plugin repository to opam:
opam repo add coq-released https://coq.inria.fr/opam/releasedThen you need to install the necessary dependencies. You also need to make sure
the current opam switch is using an ocaml version that is at least 4.14.1.
opam install dune coq.8.17.1 coq-unimath.20230321Finally build and install the plugin:
opam pin add coq-commutative-diagrams https://github.com/dwarfmaster/commutative-diagrams.gitFinally, import opam environment in the current shell. Unless you use a mecanism to automate it, you need to do this for every shell you open.
eval $(opam env)The two main tactics are diagram run and diagram edit.
The diagram run "file" tactic tries to read commands from file and execute
them on the current goal. If it succeeds, the interface is never opened. If it
fails, or if the the file is empty, the interface is opened to graphically solve
the goal. If there where commands in the file, they are not executed but can be
replayed using the Edit>Redo button.
The diagram edit "file" always open the interface, allowing to redo part of
the proof and change other, even if it would have succeeded.