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.
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 13 2024 at 01:02 UTC