Let's suppose that I have, for example, two files - A.v and B.v. File B.v imports A.v and that means that A.v should be compiled first with B.v following next.
How to automate such process? Is there some way to write the order of compilation in some file and just call some command with the file given as parameter?
That's something I have postponed too long... should learn how to do finally.
So, I made the _CoqProject.txt file with such content:
-R "C:\Users\me\Desktop\Test" MyCode -arg "-w all" A.v B.v
Then went to directory C:\Users\me\Desktop\Test and wrote command
C:\Coq\bin\coq_makefile.exe -f _CoqProject.txt -o CoqMakefile. That resulted in two new files
CoqMakefile.conf but I saw no files A.vo and B.vo or similar.
What's the next step?
make -f CoqMakefile If I remember correctly
Also, do not put the full path after
-R. Just use
. (a single dot), since your files
B.v are next to your
_CoqProject.txt file. And I suggest to remove the
.txt extension if you are using Coqide or ProofGeneral, since they read
_CoqProject by default.
@Lessness here is a pure Coq project with the right boilerplate for building with coq_makefile, maybe useful as inspiration: https://github.com/coq-community/jmlcoq
however, it uses
-Q instead of
-R, but the former is essentially just a stricter form of the latter...
I installed Make for Windows from gnuwin32.sourceforge.net/packages/make.htm.
Is this the correct program?
How did you install Coq in the first place?
From coq.inria.fr, I believe. I have version 8.13.2 for now.
Sure. But concretely, what did you do? Did you use the installer for the "Platform"? If so, it should have installed a Cygwin environment that already contains everything you might need, including Make.
Hmm, I don't have a cygwin environment. Ok, uninstalled current Coq and installing Coq-Platform-8.14... from Github right now.
Still did something wrong, it seems. It didn't install Cygwin... but I installed Cygwin with make myself and successfully ran
make -f CoqMakefile
command in it. :)
Lessness has marked this topic as resolved.
Indeed, the Coq Platform installer doesn't install cygwin but is compatible with a cygwin-installed make. We should document that.
Last updated: Feb 08 2023 at 23:03 UTC