Stream: Coq devs & plugin devs

Topic: test-suite failure with local-late-extensions


view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (May 28 2021 at 13:02):

IIUC this was introduced recently by @Jason Gross so asking for help

view this post on Zulip 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

view this post on Zulip Jason Gross (May 28 2021 at 13:06):

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...)

view this post on Zulip Gaëtan Gilbert (May 28 2021 at 13:08):

+ exit 1 is from the shell set -x, not part of the diff

view this post on Zulip Pierre-Marie Pédrot (May 28 2021 at 13:11):

noice

view this post on Zulip Gaëtan Gilbert (May 28 2021 at 13:16):

this grep -v approach is nonsense, we don't care about the log

view this post on Zulip Gaëtan Gilbert (May 28 2021 at 13:21):

https://github.com/coq/coq/pull/14404

view this post on Zulip Jason Gross (May 28 2021 at 13:53):

Thanks! I've reviewed and left some suggestions for further simplifications


Last updated: Oct 21 2021 at 20:02 UTC