Require module in same directory

Question

I don't know what's the recommended approach to manage large projects and load paths, but I usually work on a single directory where I have different files which should be able to work together. What I usually do is compile, say, A.v from the command line with coqc A.v. Then, in B.v, which is in the same directory, I'd like to Require A and try some things interactively in CoqIDE or some other IDE (I often use a plugin for vscode). The problem is that I have to explicitly add the current directory to the load to make it work: Add LoadPath "/absolute/path/to/my/project". Require A.. Is there a simpler way to do it? At least I'd like to be able to do write relative paths in Add LoadPath so I don't have to change every file when I rename my directory.

Answer 1

To get started I would recommend to setup your Coq project using a _CoqProject file. Imagine your coq project where called project. Then to add files A.v and B.v you would put the following into your _CoqProject file:

-R . project
./A.v
./B.v

This way you can use the Coq makefile generator to get all you need:

coq_makefile -f _CoqProject -o Makefile

Both emacs ProofGeneral and CoqIDE should then be able to load your files using only Require Import A.. According to this question, it can be the case that CoqIDE will complain about library project.A being in file A.v and not library A. This can be fixed by starting coqide -R . project.

As suggested in the comments I would recommend to read the manual part about Coq project files and makefiles if you want to really understand how to use this machinery.