2025-02-28

Coq Plugin Development 1

Coq (Now is rocq) is an outstanding interactive theorem prover, and it has great community. Official website : https://rocq-prover.org/

Currently, Coq supports the development of plugins using OCaml, Ltac, and Coq-Elpi, each of which has its own advantages. I prefer to use OCaml for writing plugins, because thanks to the OCaml language, I can better integrate Coq’s proof process with other tools (accessing web databases, invoking other scripts, etc.).

Here is my coq plugin template : https://github.com/Rw1nd/CoqPlugin-Template

I use Coq 8.19.1 and OCaml 4.14.1, and plugin name is coq-xxxxx. The folder contains the following files:

.
├── Makefile
├── README.md
├── _CoqProject
├── coq-xxxxx.opam
├── dune-project
├── src
│   ├── META.coq-xxxxx
│   ├── dune
│   ├── g_xxxxx.mlg
│   ├── some.ml
│   ├── some.mli
│   └── xxxxx_plugin.mlpack
└── theories
    ├── Demo.v
    └── Loader.v

If you need to compile the plugin:

opam switch create [name] 4.14.1
eval $(opam env --switch=[name])
opam install coq.8.19.1

cd path-to-CoqPlugin-Template
make

In g_xxxxx.mlg, you can define your own commands or tactics. See the official tutorial for more details

src/*.ml is used to implement your own code. Coq’s OCaml API provides a lot of modules that is available for development with plugins. See Coq V8.19.1 OCaml API document

Coq Plugin Development with vscode

VSCode assists us in checking syntax errors, displaying type information, and matching available functions. If you wish to use VSCode for development, install the OCaml Platform plugin.

opam install vscoq-language-server.2.2.3
opam install ocamlformat-rpc.0.21.0
opam install ocaml-lsp-server.1.20.1-4.14

Before opening vscode, you need to compile the project using dune.

cd path-to-CoqPlugin-Template
make clean
dune build
code .

Open VScode and select your OCaml environment:

Select OCaml file, and you can see type information and syntax information: