# Building a project with coq\_makefile, using a library specified in .coqrc

**URL:** https://discourse.rocq-prover.org/t/building-a-project-with-coq-makefile-using-a-library-specified-in-coqrc/1542
**Category:** Using Rocq
**Created:** [January 25, 2022, 3:50pm UTC](https://discourse.rocq-prover.org/t/building-a-project-with-coq-makefile-using-a-library-specified-in-coqrc/1542 "2022-01-25T15:50:56Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![slasser](https://avatars.discourse-cdn.com/v4/letter/s/ad7895/32.png) [@slasser](https://discourse.rocq-prover.org/u/slasser)
#### Post date: [January 25, 2022, 3:50pm UTC](https://discourse.rocq-prover.org/t/building-a-project-with-coq-makefile-using-a-library-specified-in-coqrc/1542/1 "2022-01-25T15:50:56Z")

</div>

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?