Lessness (Mar 07 2022 at 16:28): Lessness (Mar 07 2022 at 16:28):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?
Lessness (Mar 07 2022 at 16:29):That's something I have postponed too long... should learn how to do finally.
Guillaume Melquiond (Mar 07 2022 at 16:30): Lessness (Mar 07 2022 at 16:31):Thank you!
Lessness (Mar 07 2022 at 17:15):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 and CoqMakefile.conf but I saw no files A.vo and B.vo or similar.
What's the next step?
Kenji Maillard (Mar 07 2022 at 17:16):make -f CoqMakefile If I remember correctly
Guillaume Melquiond (Mar 07 2022 at 17:35):Also, do not put the full path after -R. Just use . (a single dot), since your files A.v and 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.
Karl Palmskog (Mar 07 2022 at 17:56):@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
Karl Palmskog (Mar 07 2022 at 17:57):however, it uses -Q instead of -R, but the former is essentially just a stricter form of the latter...
Lessness (Mar 07 2022 at 18:01):I installed Make for Windows from gnuwin32.sourceforge.net/packages/make.htm.
Is this the correct program?
Guillaume Melquiond (Mar 07 2022 at 18:02):How did you install Coq in the first place?
Lessness (Mar 07 2022 at 18:09):From coq.inria.fr, I believe. I have version 8.13.2 for now.
Guillaume Melquiond (Mar 07 2022 at 18:15):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.
Lessness (Mar 07 2022 at 18:31):Hmm, I don't have a cygwin environment. Ok, uninstalled current Coq and installing Coq-Platform-8.14... from Github right now.
Lessness (Mar 07 2022 at 18:49):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. :)
Notification Bot (Mar 07 2022 at 19:25):Lessness has marked this topic as resolved.
Théo Zimmermann (Mar 07 2022 at 21:46):Indeed, the Coq Platform installer doesn't install cygwin but is compatible with a cygwin-installed make. We should document that.
Last updated: Oct 04 2023 at 22:01 UTC