Manage your Coq projects like a pro
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 *.vo
s 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 *.vo
s 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 *.v
s, 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, Section
s 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:
- Ilya Sergey, Programs and Proofs, Section 2.6 Sections and Modules
- Adam Chlipala, Certified Programming with Dependent Types, Section 16.3 Modules
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:
- Multiple coq versions
- 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:
- Install OPAM
- Check out the system OCaml compiler version by
opam switch list
, find the version number in the last line withsystem
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. 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 afterinstall
can be chosen arbitrarily, but using thecoq-<coq-compiler-version-number>
is more convenient for our purpose.
- Example:
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`
- Example:
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.