I have two Coq projects with the following structure:
A/
_CoqProject
Foo.v
B/
_CoqProject
Bar.v
My .coqrc file contains the following command:
Add LoadPath “path/to/A” as A.
After building project A, I can use Proof General to open Bar.v and import definitions from project A (e.g., Require Import A.Foo), which is what I expect because of the contents of .coqrc.
However, when I use coq_makefile to create a Makefile for project B and try to build the project, I get the following output:
*** Warning: in file Bar.v, library A.Foo is required and has not been found in the loadpath!
COQC Bar.v
File “./Bar.v”, line 1, characters 15-20:
Error: Cannot find a physical path bound to logical path matching suffix A.
I can build project B successfully by running coq_makefile as follows:
coq_makefile -Q path/to/A A -f _CoqProject -o Makefile
However, I’d rather provide project A’s loadpath via .coqrc. Is there a way to use coq_makefile such that, when I build the project, coqc reads from the .coqrc file?