Coq: manage LoadPath in project with subdirectories

Question

I have a Coq project with its libraries organised into subdirectories, something like:

…/MyProj/Auxiliary/Aux.v
…/MyProj/Main/Main.v  (imports Auxiliary/Aux.v)

When I compile the files, I expect to do so from working directory MyProj (via a makefile). But I also want to work on the files using Proof General/Coqtop, in which case the working directory is by default the directory in which the file lives.

But this means that the LoadPath is different between the two contexts, and so the logical path needed for the library import is different. How do I set up the coqc invocation, the LoadPath, and the import declarations so that they work in both contexts?

Each approach I have tried, something goes wrong. For instance, if I compile Aux.v by invoking

coqc -R "." "MyProj" Auxiliary/Aux.v

and import it in Main.v as

Require Import MyProj.Auxiliary.Aux.

then this works when I compile Main.v with

coqc -R "." "MyProj" Main/Main.v

but fails in Coqtop, with Error: Cannot find library MyProj.Auxiliary.Aux in loadpath. On the other hand, if before the Require Import I add

Add LoadPath ".." as MyProj.

then this works in Coqtop, but fails under coqc -R "." "MyProj" Main/Main.v, with

Error: The file […]/MyProj/Auxiliary/Aux.vo contains library

MyProj.Auxiliary.Aux and not library MyProj.MyProj.Auxiliary.Aux

I’m looking for a solution that’s robust for a library that’s shared with collaborators (and hopefully eventually with users), so in particular it can’t use absolute file paths. The best I have found for now is to add emacs local variables to set the LoadPath up when Proof General invokes Coqtop:

((coq-mode . ((coq-prog-args . ("-R" ".." "MyProj" "-emacs")))))

but this (a) seems a little hacky, and (b) only works for Proof General, not in Coqide or plain Coqtop. Is there a better solution?

Answer 1

Allow me to side-step your question by suggesting an alternative process, hinted at by Tiago.

Assuming that your project's tree looks like this:

MyProj/Auxiliary/Aux.v
MyProj/Main/Main.v

In MyProj, write a _CoqProject file listing all your Coq files

-R . ProjectName
Auxiliary/Aux.v
Main/Main.v

When you open one of these Coq files, emacs will look for the _CoqProject and do-the-right-thing (tm).

As shown by Tiago, coq_makefile will also give you a Makefile for free.

Answer 2

I know you explicitly asked for something that works across different platforms, but there's already a Proof-General-specific solution that is less hacky than the one you have. Proof General has a special variable called coq-load-path that you can set with local variables, much like you did for coq-prog-args. The advantage is that you don't have to worry about any other arguments that need to be passed to coqtop (such as -emacs in your example). Thus, your .dir-locals.el file could have a line like this:

((coq-mode . ((coq-load-path . ((".." "MyProj"))))))

Unfortunately, I am not aware of anything that works across platforms, although I'm pretty sure that something specific for CoqIDE must exist. If this is the case, maybe you could set up a script to keep these configuration files updated across different platforms?

Answer 3

If you use coq_makefile you can install the library in your system.

Without OPAM

To initialize your project:

coq_makefile -f _CoqProject -o Makefile

Share your library with other projects:

make install

With OPAM

Assuming you have OPAM installed, you can use coq-shell to help you take care of dependencies.

To setup your project:

coq_shell_url="https://raw.githubusercontent.com/gares/opam-coq-shell/master/src/opam-coq"
curl -s "${coq_shell_url}" | bash /dev/stdin init 8.4 # Install Coq and its dependencies
eval `opam config env --switch=coq-shell-8.4`         # Setup the environment
coq_makefile -f _CoqProject -o Makefile               # Generates the makefile
opam pin add coq:YOURLIBRARY .                        # Add your library to OPAM

When you update your library you should do:

opam upgrade coq:YOURLIBRARY

Here is an example of a project that uses the OPAM method:

https://bitbucket.org/cogumbreiro/aniceto-coq/src