Stream: Coq users

Topic: Order of compilation in Makefile.coq


view this post on Zulip Fabian Kunze (Nov 19 2020 at 10:39):

Does anyone know if I can influence the order of compilation using coq_makefile and _CoqProject (of files not depending of each other of course)?
I have a .v file that is very slow, and would like to 'prioritise' it and its dependencies so that with a parallel make -j, I do not end in a situation where SLOW.v is compiled near the end and the only file left, thus not making use of parallelism.

I once thought that the order of files in the _CoqProject was of any significance for this, but I can't reproduce anything like this anymore.

view this post on Zulip Enrico Tassi (Nov 19 2020 at 11:29):

This has little to do with Coq, it's really a question about make. The short answer is no, but apparently some internals can be exploited https://lists.gnu.org/archive/html/bug-make/2009-12/msg00023.html


Last updated: Oct 05 2023 at 02:01 UTC