Pierre-Marie Pédrot (May 28 2021 at 13:01): Pierre-Marie Pédrot (May 28 2021 at 13:01):I am getting reproducible test-suite failures when built locally, due to coq-makefile/local-late-extension/run.sh
Pierre-Marie Pédrot (May 28 2021 at 13:02):IIUC this was introduced recently by @Jason Gross so asking for help
Pierre-Marie Pédrot (May 28 2021 at 13:02):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...)
Gaëtan Gilbert (May 28 2021 at 13:08):+ exit 1 is from the shell set -x, not part of the diff
Pierre-Marie Pédrot (May 28 2021 at 13:11):noice
Gaëtan Gilbert (May 28 2021 at 13:16):this grep -v approach is nonsense, we don't care about the log
Gaëtan Gilbert (May 28 2021 at 13:21):https://github.com/coq/coq/pull/14404
Jason Gross (May 28 2021 at 13:53):Thanks! I've reviewed and left some suggestions for further simplifications
Last updated: Apr 19 2024 at 17:02 UTC