Updated at Feb 1, 2017

In this post, I will summarize some ways of organize your Coq development. By saying pro, I mean just not being a script kid, so don’t overestimate it ;) Also, maybe not everyone thinks it is a headache, but Coq project management did bite me numerous times.

Require Import locally

Let’s start with a simple case: a bunch of .v coq scripts under directory X. There might be some inter-dependency between them. How to make the thing click?

First thing to notice is that if you want to efficiently use definitions etc. in another file, you need to link to the compiled .vo file of it. If they are in standard library, like Arith, then you can just Require Import Arith, since the standard library is already in path.

But how can I get the .vo files?

you can first compile it using coqc command yourself. For example, supposing you have source folder:

.
└── src
    ├── a.v
    └── b.v

a.v is:

Definition bar: nat := 1.

b.v is:

Require Import a.

Definition foo := bar.

Now, compile your file with following commands:

coqc -R src "" src/a.v src/b.v

What happens? First, -R maps physical address src (which is in fact expanded to $PWD/src) to empty library prefix "".

Here, the library prefix is a qualified way of referring a tree-structured group of modules (i.e. *.v files, not Module), which usually serves as a library, like Coq.Init. The prefix can also be empty, i.e. "", which means that all modules can be referred in a direct way, like the a in Require import a.. Now, since file system is also a tree structure (at least you will hope so), by sticking together two roots (two arguments of -R), the decedents will be referred in an implicit way.

For example, if logical library prefix Lib is mapped to folder X, then by Require Import Lib.Foo.bar, we link to file X/Foo/bar.v.

Actually, -R is a more flexible variant of -Q, as -R permits shortcut names [1]. For instance, combination coqc -Q src "" src/a.v src/b.v and Require Import a is fine, but combination coqc -Q src Lib src/a.v src/b.v and Require Import a would cause error (fix: Require Import Lib.a).

Another nit is that the order of filenames in coqc arguments must conform to its real dependency order, because the compiler coqc itself has no idea of dependency and will just compile in the order of appearance.

Now, if you launch coqtop in src, or edit one file with proof general, you should be able to play with it. I guess that coqtop working path is mapped to empty library prefix by default, and coqtop can spot the compiled *.vo here, so it can load successfully.

For more information, please see [2].

Add LoadPath

Add LoadPath can be viewed as another approach to the same problem above. For example, the b.v now is:

Add LoadPath "X/src".

Require Import a.

Definition foo := bar.

Then you can simply use coqc src/a.v src/b.v to compile them. What happened is that X/src is mapped to empty library prefix.

Now considering that you are developing a library A in path_to_A and a client project B in path_to_B. In A, you can either make install (using the Makefile we will introduce later), or use Add LoadPath on client side. Here are more details:

For the first choice, you essentially installed the *.vos to the default load path, which should be global thus you might not have the permission to do so. Using make userinstall can mitigate this problem, but it is somewhat annoying that every time you make your change, you have to install it in order to test it on the client side.

The second choice handles this better. By adding a custom path with Add LoadPath to search space, we essentially expose the *.vos built in the source folder. So change will immediately take effect after you make it (but you still need to reload it anyway …)

The caveat is that you need to add this ad-hoc thing to your source, which is not good. Instead, you can insert this line to your ~/.coqrc.

For me, I usually take a more general approach. Say I have a bunch of Coq projects under folder ~/Repos/coq, and I will try to make sure that every library folder is named after its library name (and they should be structured in the Makefile style introduced later as well). As a result, I mimic the structure of global library path (usually user-contrib or something) in my local dev folder.

In this way, the client code can just write something like Require Import Lib_x.Mod_a, while the library can either be installed or hot in source folder.

Makefile and _CoqProject

For a larger project, we need more build automation. You can copy & paste the below Makefile:

# Makefile originally taken from coq-club

%: Makefile.coq phony
	+make -f Makefile.coq $@

all: Makefile.coq
	+make -f Makefile.coq all

clean: Makefile.coq
	+make -f Makefile.coq clean
	rm -f Makefile.coq

Makefile.coq: _CoqProject Makefile
	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq

_CoqProject: ;

Makefile: ;

phony: ;

.PHONY: all clean phony

And then create a _CoqProject file like this:

-Q . Lib
A/a.v
b.v

Note that we don’t need to maintain ordering between *.vs, the coqdep called by build script will handle this for us.

Next, you call make Makefile.coq, which will generate the boilerplate Makefile.coq considering the information in _CoqProject.

Afterwards, you can simply use make to build your source.

Your source folder should looks like this now:

.
├── Makefile
├── Makefile.coq
├── _CoqProject
├── A
│   └── a.v
└── b.v

For the sake of source control, the only essential thing is _CoqProject. It is up to you whether or not to include the distributed/generated Makefile/Makefile.coq.

Also, you may find it useful to use -Q several times to map multiple libraries.

Another nice thing about _CoqProject is that ProofGeneral can automatically detect its presence and parse it to get correct dependencies in place when you go through the proofs in Emacs.

Require/Export/Import/From

First, Require X will load the X.vo into the environment, but not yet exposing names in it. Afterwards, by Import X or Export X, we can expose the names at least to current environment. The difference is that, Import will not expose these imported names to modules that depends on current environment (which might be another module), while Export will. In other languages, what Export do in extra is also called re-export.

What is awesome (but also confusing) is that we can use Require Import X. to do the same thing as Require X. Import X., and similarly for Export. People usually go this way, since there is really no fruit to only Require something without using it!

As far as From, it is usually used to Require [Import/Export] a bunch of things with same library prefix. That it to say, From A.B Require Import C1 C2 is equivalent to Require Import A.B.C1 A.B.C2.

Namespace in Coq

Usually, Sections are used to create a space for local declarations, like Variable and Context. It is some form of name hiding (but all local names turn into arguments from the external view!). And in most cases, people won’t mind much about the fact that sometimes they only need a small portion of names defined externally, while you pull them all in by Require [Import|Export].

However, there is also a less-popular way to do namespace stuff: The ML-style Module System [4]. Note that the “module” here is not the same concept we referred in previous text (And usually, when someone talks about Coq module with you, he probably means the file-based one).

Here are two books introducing it:

You can learn more about the details by reading these tutorials.

UPDATE: Module in Coq is somewhat a pain, and it looks like people are requiring to remove it and have a simple, reasonable namespace mechanism instead.

Install Coq with OPAM

Using Coq with OPAM mainly solves two problems:

  1. Multiple coq versions
  2. Local coq installation

While there are some basic instructions, I found it a bit hard to understand at the first sight so I summarize the key points as below:

  1. Install OPAM
  2. Check out the system OCaml compiler version by opam switch list, find the version number in the last line with system before it. You can use newer OCaml distribution as well. Next, we are going to create a new OPAM environment for a specific version of Coq.
  3. opam switch install coq-<coq-compiler-version-number> --alias-of <ocaml-compiler-version-number>
    • Example: opam switch install coq-8.5 --alias-of 4.04.0
    • <ocaml-compiler-version-number> is what we found in the previous step
    • <coq-compiler-version-number> is the Coq version number. Note that the name after install can be chosen arbitrarily, but using the coq-<coq-compiler-version-number> is more convenient for our purpose.
  4. opam pin add coq <coq-compiler-version-number>
    • Example: opam pin add coq 8.6
    • This will download and install the corresponding Coq in current OPAM environment. As this command will probably hint, you should run eval `opam config env`

When you want to install another version of Coq, simply repeat step 3 and step 4. To switch between them, just opam switch coq-<coq-compiler-version-number> and eval `opam config env`.

Manage Coq libraries with OPAM

First, a lot of popular Coq libraries are packaged and distributed through OPAM official channel, like ssreflect.

Second, you can use OPAM to manage your libraries in git repos as well! You might find opam pin useful.

References

  1. The Coq commands – Coq documentation
  2. Libraries – Coq documentation
  3. Compiled files – Coq documentation
  4. The Module System