Coq Project Setup

Tutorial for setting up your own Coq Project

2024-01-02 1573 words 8 minutes

Contents

Why

Proof assistants like Coq and Lean4 are becoming more and more popular. However, there is a lack of tutorials on how to set up a Coq project. As useful a tool as they are to mathematicians in the 21st century, they are almost useless if not configured to include other's libraries. This tutorial aims to fill this gap.

Installation Guide

The first step in setting up a Coq Project is to install Coq. For the users who merely want to try out Coq, please refer to this guide or simply use your favourite package management system like homebrew or paru.

The more advanced users may need to use libraries that's not included in the above mentioned distributions of Coq. The Coq homepage mentioned multiple ways to install Coq with extendability. I will follow the method using opam, the package manager for OCaml. OCaml is the language used to write Coq, therefore Coq related libraries should remain "native" to OCaml. Using opam has the advantage of keeping the toolchain in the ecosystem of OCaml.

Opam Preparation

You could visit the homepage of opam to install it. To verify opam is correctly installed, run the following command.

opam --version

2.1.5

By default, opam will install a global OCaml compiler. OCaml code and packages will conform to that version by default. We will create an "environment" with a version of OCaml specifically for Coq. The "environment" where our OCaml compiler lives is called a switch in OCaml. To create the switch run the following code.

opam switch create my-coq 4.10.2

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><> 🐫 Switch invariant: ["ocaml-base-compiler" {= "4.10.2"} | "ocaml-system" {= "4.10.2"}] Constructing initial basis…

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫 ∗ installed base-bigarray.base ∗ installed base-threads.base ∗ installed base-unix.base ⬇ retrieved ocaml-base-compiler.4.10.2 (https://opam.ocaml.org/cache) ∗ installed ocaml-base-compiler.4.10.2 ∗ installed ocaml-config.1 ∗ installed ocaml.4.10.2 Done.

After the creation of the switch, we could change to that switch via

opam switch my-coq
eval $(opam env)

Roots

As a side note, you could also create a new root in OCaml. A root is a higher level of "environment" than switch. It contains several switches. Packages installed in a root is sharable amongst switches under that same root. We will not use them here.

Install Coq

Now that opam is all installed and configured, we could go ahead and install Coq. If you just want to install Coq you could run the following code

# don't run this just yet
opam add coq $VERSION_NUMBER

However, as this guide points out, Coq is highly sensitive to version number, we would also like to fix the Coq version. We could achieve this using pin keyword like this

# version 8.18.0 is most upto date version as of 2024/01/01
opam pin add coq 8.18.0

Verification

Assuming you have following the guide til now, we could verify that you have installed Coq correctly, run the following command.

coqc -v

The Coq Proof Assistant, version 8.18.0 compiled with OCaml 4.10.2

Packages

As alluded to before, Coq is not a standalone software. It is a proof assistant. Therefore, it is highly likely that you will need to use some libraries to help you with your proofs. The most common way to install packages is to use opam. To do so, you will first need to add the coq-released repo to opam.

opam repo add coq-released https://coq.inria.fr/opam/released

Now that you have added the repository, you could install packages from it. Let's browse the repository first.

opam search coq

archsat – A first-order theorem prover with formal proof output coq 8.18.0 pinned to version 8.18.0 coq-aac-tactics – Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators coq-abp – A verification of the alternating bit protocol expressed in CBS coq-actuary – Formalization of actuarial mathematics in Coq coq-addition-chains – Exponentiation algorithms following addition chains in Coq coq-additions – Addition Chains coq-ails – Proof of AILS algorithm coq-alea – Coq library for reasoning on randomized algorithms coq-algebra – Basics notions of algebra

We could see that there are a lot of packages available. Let's take a closer look at one of them

opam show coq-graph-theory

<><> coq-graph-theory: information on all versions ><><><><><><><><><><><><> 🐫 name coq-graph-theory all-versions 0.7 0.9 0.9.1 0.9.2 0.9.3

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><> 🐫 version 0.9.3 repository coq-released url.src "https://github.com/coq-community/graph-theory/archive/v0.9.3.tar.gz" url.checksum "sha512=1cc5fef0c862d8a52ebf63dad547a996b57b61d2e13ec06245ba37fee1deaccd9cf9b90ad965c6c93a06d7c197810cdabb78bf2f85f803e1f8133bf93e51dc73" homepage "https://github.com/coq-community/graph-theory" bug-reports "https://github.com/coq-community/graph-theory/issues" dev-repo "git+https://github.com/coq-community/graph-theory.git" authors "Christian Doczkal" "Damien Pous" maintainer "christian.doczkal@mpi-sp.org" license "CECILL-B" tags "category:Computer Science/Graph Theory" "keyword:graph theory" "keyword:minors" "keyword:treewidth" "keyword:algebra" "logpath:GraphTheory.core" "date:2023-08-21" depends "dune" {>= "2.8"} "coq" {>= "8.16" & < "8.19"} "coq-mathcomp-ssreflect" {>= "2.0"} "coq-mathcomp-algebra" "coq-mathcomp-finmap" "coq-hierarchy-builder" {>= "1.4.0"} synopsis General graph theory definitions and results in Coq and MathComp description Formalized general graph theory definitions and results using Coq and the Mathematical Components library, including various standard results from the literature (e.g., Menger's Theorem and Hall's Marriage Theorem).

The package looks like being under active development. Let's install it.

opam instal coq-graph-theory

To end things in this section, we will show you three ways to find logical name that is needed to tell Coq how to load a package. A Logical Name is essentially a path to the Coq file on your machine of which your current program needs to load. To get the logical name, you could either

opam show --list-files coq-graph-theory | head -n1

Users/yushengzhao.opam/my-coq/doc/coq-graph-theory

opam switch my-coq
eval $(opam env)
ls $(coqtop -where)/user-contrib

GraphTheory (this is the one) HB Ltac2 elpi mathcomp

Afterwards

After the installation, you will want to examine what packages are installed relating to Coq. This can be achieved with

opam list "coq-*" --installed

You may also want to explore other repositories that contains user developed Coq libraries, you may find them here. For example, you could run

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

to install extra-dev packages. They include more topics than released packages ableit being less stable.

Project Creation

Now that Coq has been installed, let's talk about how to initialize a Coq project. There are three ways to generate a project skeleton. Firstly, you could use dune, OCaml's build system, to generate the skeleton for a Coq project. However, as this guide points out, this is still experimental. Furthermore, I have found the dune-project file a bit cryptic, we will not cover it here. But interested reader should read the previous referred guide and dune's documentation. The second method is to use coq_makefile. It's a tool included with Coq which relies on makefile to generate a project skeleton. Although it's widely used within the community, I have found it to be restrictive in the templates it supports and others found the dependency on makefile system too complicated. Interested reader should find this guide helpful.

We will focus on the third method, the use of template created by the coq-community.

Install Mustache

Mustache is a tool that allows you to generate text from a template. It is used by the coq-community to generate the project skeleton. To install it, run

sudo gem install mustache

Write meta.yml file

The coq-community template uses a meta.yml file to generate the project skeleton. The file is written in YAML format. The following is an example of meta.yml file.

---
fullname: Huffman
shortname: huffman
organization: coq-community
community: true
action: true
coqdoc: true
coqdoc_index: 'docs/latest/coqdoc/toc.html'

synopsis: Coq proof of the correctness of the Huffman coding algorithm

description: |-
  This projects contains a Coq proof of the correctness of the Huffman coding algorithm,
  as described in David A. Huffman's paper A Method for the Construction of Minimum-Redundancy
  Codes, Proc. IRE, pp. 1098-1101, September 1952.  

publications:
- pub_url: https://hal.archives-ouvertes.fr/hal-02149909
  pub_title: Formalising Huffman's algorithm
- pub_url: http://compression.ru/download/articles/huff/huffman_1952_minimum-redundancy-codes.pdf
  pub_title: A Method for the Construction of Minimum-Redundancy Codes
  pub_doi: 10.1109/JRPROC.1952.273898

authors:
- name: Laurent Théry
  initial: true
- name: Karl Palmskog
  orcid: 0000-0003-0228-1240

maintainers:
- name: Karl Palmskog
  nickname: palmskog

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: GNU Lesser General Public License v2.1 or later
  identifier: LGPL-2.1-or-later

supported_coq_versions:
  text: 8.12 or later
  opam: '{(>= "8.12" & < "8.20~") | (= "dev")}'

tested_coq_opam_versions:
- version: 'dev'
- version: '8.19'
- version: '8.18'
- version: '8.17'
- version: '8.16'
- version: '8.15'
- version: '8.14'
- version: '8.13'
- version: '8.12'

ci_cron_schedule: '10 1 * * 0'

namespace: Huffman

keywords:
- name: data compression
- name: code
- name: huffman tree

categories:
- name: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
- name: Miscellaneous/Extracted Programs/Combinatorics

documentation: |-
  ## Documentation

  For more information about the project, see the [technical report][techreport]
  describing the formalization. See also the [coqdoc presentation][coqdoc] of the
  Coq source files from the latest release.

  ### Running extracted code

  To extract code and obtain the program, run
  ```shell
  make run_huffman.ml
  ```

  Next, open an OCaml toplevel (e.g., `ocaml`) and do
  ```ocaml
  #use "run_huffman.ml";;
  ```

  To get the code that gives the frequency string:
  ```ocaml
  let code = huffman "abbcccddddeeeee";;
  ```

  To code a string:
  ```ocaml
  let c = encode code "abcde";;
  ```

  To decode a string:
  ```ocaml
  decode code c;;
  ```

  [techreport]: https://hal.archives-ouvertes.fr/hal-02149909
  [coqdoc]: https://coq-community.org/huffman/docs/latest/coqdoc/toc.html  
---

The detailed explaination of each field can be found in this file.

To see more examples, please refer to The meta.yml file section of the coq-community template's README.

Generate Project

Now that we have the meta.yml file, we could generate the project skeleton using the following command.

cd <your-project>
TMP=$(mktemp -d); git clone https://github.com/coq-community/templates.git $TMP
$TMP/generate.sh # nix users can do instead: nix-shell -p mustache-go --run $TMP/generate.sh
git add <the_generated_files>