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
you can first compile it using
coqc command yourself. For example, supposing you have source folder:
. └── src ├── a.v └── b.v
Definition bar: nat := 1.
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
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
-R is a more flexible variant of
-R permits shortcut names . 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
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 .
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
path_to_A and a client project
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
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.
For a larger project, we need more build automation. You can copy & paste the below
# 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
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
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
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 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
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
Sections are used to create a space for local declarations, like
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
However, there is also a less-popular way to do namespace stuff: The ML-style Module System . 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 with
systembefore 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>
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
installcan be chosen arbitrarily, but using the
coq-<coq-compiler-version-number>is more convenient for our purpose.
opam pin add coq <coq-compiler-version-number>
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.