I am getting reproducible test-suite failures when built locally, due to coq-makefile/local-late-extension/run.sh
IIUC this was introduced recently by @Jason Gross so asking for help
the log says
@@ -1 +1,2 @@
+make[2]: warning: -j1 forced in submake: resetting jobserver mode.
foo.vo
+ exit 1
Huh, does the test-suite not run in parallel mode on CI? In run.sh there's a bunch of grep -v
to filter out things that are different across different builds. Add one for "forced in submake" to fix the first change. There should already be one for exit 1
, so I have no idea why that's showing up in the log... Maybe there's some issue with stdout vs stderr or pipefail or some other reason why grep does not catch it? (I ran into a similar issue where sed
seemed incapable of removing the leading spaces...)
+ exit 1
is from the shell set -x, not part of the diff
noice
this grep -v approach is nonsense, we don't care about the log
https://github.com/coq/coq/pull/14404
Thanks! I've reviewed and left some suggestions for further simplifications
Last updated: Dec 07 2023 at 17:01 UTC