Stream: Coq users

Topic: ✔ Automation of .v file compiling (makefile?)


view this post on Zulip 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?

view this post on Zulip Lessness (Mar 07 2022 at 16:29):

That's something I have postponed too long... should learn how to do finally.

view this post on Zulip Guillaume Melquiond (Mar 07 2022 at 16:30):

See https://coq.inria.fr/distrib/current/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile

view this post on Zulip Lessness (Mar 07 2022 at 16:31):

Thank you!

view this post on Zulip 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?

view this post on Zulip Kenji Maillard (Mar 07 2022 at 17:16):

make -f CoqMakefile If I remember correctly

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Lessness (Mar 07 2022 at 18:01):

I installed Make for Windows from gnuwin32.sourceforge.net/packages/make.htm.
Is this the correct program?

view this post on Zulip Guillaume Melquiond (Mar 07 2022 at 18:02):

How did you install Coq in the first place?

view this post on Zulip Lessness (Mar 07 2022 at 18:09):

From coq.inria.fr, I believe. I have version 8.13.2 for now.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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. :)

view this post on Zulip Notification Bot (Mar 07 2022 at 19:25):

Lessness has marked this topic as resolved.

view this post on Zulip 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: Feb 08 2023 at 23:03 UTC