Fabian Kunze (Nov 19 2020 at 10:39): 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.
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: Apr 19 2024 at 21:01 UTC