I've the impression it does one file at a time (no parallelism). Am I wrong?
Am I supposed to pass -j N in some way?
I wouldn't be surprised by this. Note that until the test-suite is Dunerized, I tend to prefer running
make -C test-suite (it was made compatible with a Dune-based build and allows for incremental retries).
Yes, you need to pass
NJOBS=8 for example
it will be fixed when we finish https://github.com/coq/coq/pull/13364
imo test-suite/dune is more confusing than useful
Last updated: Dec 01 2023 at 07:01 UTC