3

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.

  • 1
    Perhaps [Manage your Coq projects like a pro](https://blog.zhenzhang.me/2016/09/19/coq-dev.html) blog post can help. It might be a bit outdated, since Coq's build system was upgraded last year. You might want to read the corresponding reference manual chapter and copy Makefile from it. – Anton Trunov Mar 18 '18 at 17:25
  • I don't understand your question, because for me (under linux), I do exactly what you would like to do and never have to use the `Add LoadPath` command. – Yves Mar 19 '18 at 07:30
  • See also this [question](https://stackoverflow.com/questions/16202666/coqide-cant-load-modules-from-same-folder), though I am not fully satisfied with the proposed answers. – eponier Mar 19 '18 at 11:03

1 Answers1

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.

Community
  • 1
  • 1
Heiko Becker
  • 556
  • 3
  • 16