Coq: manage LoadPath in a project using subdirectories

Question

I have a Coq project with its libraries organized in subdirectories, for example:

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

When I compile the files, I expect to do this from the MyProj working directory (via the make file). But I also want to work with files using Proof General / Coqtop, in which case the default working directory is the directory where the file is located.

But this means that LoadPath is different between the two contexts, and therefore the logical path required to import the library is different. How to set up coqc, LoadPath and import declarations to work in both contexts?

Every approach I tried is something wrong. For example, if I compile Aux.v by calling

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

and import it into Main.v as

 Require Import MyProj.Auxiliary.Aux. 

then this works when I compile Main.v with

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

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

 Add LoadPath ".." as MyProj. 

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

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

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

We are looking for a solution that is reliable for a library that is shared by the co-authors (and, I hope, ultimately with users), therefore, in particular, it cannot use absolute file paths. The best I have found now is to add local emacs variables to set LoadPath when Proof General calls Coqtop:

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

but this one (a) seems a bit hacky, and (b) works only for proof, not Coqide or plain Coqtop. Is there a better solution?

Answer 1

I know that you explicitly requested something that works on different platforms, but there is already a solution specifically designed for testing, which is less dangerous than the one you have. The proof has a special variable called coq-load-path , which you can set using local variables, just like coq-prog-args . The advantage is that you do not have to worry about any other arguments that need to be passed to coqtop (e.g. -emacs in your example). So your .dir-locals.el could have a line like this:

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

Unfortunately, I do not know anything that works on different platforms, although I'm sure something specific for CoqIDE should exist. If so, maybe you can configure the script so that these configuration files are updated on different platforms?

Answer 2

Let me shift your question by suggesting the alternative process that Tiago has hinted at.

Assuming your project 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 _CoqProject and do-the-right-thing (tm).

As shown by Thiago, coq_makefile also provide you with a Makefile for free.

Answer 3

If you use coq_makefile , you can install the library on 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 set up a 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:

 opam upgrade coq:YOURLIBRARY 

Here is an example project using the OPAM method:

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