dune.2.log

...
CHECK     success/Nia.v
make report
make[1]: Entering directory '/srv/src/coq/_build/default/test-suite'
BUILDING SUMMARY FILE
logs/micromega/qexample.v.log
==========> TESTING micromega/qexample.v <==========
File "./micromega/qexample.v", line 70, characters 2-12:
Error:
Anomaly
"Uncaught exception Failure("command \"/srv/src/coq/_build/install/default/lib/coq/plugins/micromega/csdpcert\" exited 127")."
Please report at http://coq.inria.fr/bugs/.

0m0.003s 0m0.003s
0m0.748s 0m0.428s
==========> FAILURE <==========
    micromega/qexample.v...Error! (should be accepted)

logs/micromega/bertot.v.log
==========> TESTING micromega/bertot.v <==========
File "./micromega/bertot.v", line 22, characters 2-12:
Error:
Anomaly
"Uncaught exception Failure("command \"/srv/src/coq/_build/install/default/lib/coq/plugins/micromega/csdpcert\" exited 127")."
Please report at http://coq.inria.fr/bugs/.

0m0.009s 0m0.003s
0m1.532s 0m0.638s
==========> FAILURE <==========
    micromega/bertot.v...Error! (should be accepted)

logs/micromega/example.v.log
==========> TESTING micromega/example.v <==========
File "./micromega/example.v", line 19, characters 2-12:
Error:
Anomaly
"Uncaught exception Failure("command \"/srv/src/coq/_build/install/default/lib/coq/plugins/micromega/csdpcert\" exited 127")."
Please report at http://coq.inria.fr/bugs/.

0m0.004s 0m0.004s
0m0.871s 0m0.424s
==========> FAILURE <==========
    micromega/example.v...Error! (should be accepted)

logs/micromega/rexample.v.log
==========> TESTING micromega/rexample.v <==========
File "./micromega/rexample.v", line 81, characters 2-12:
Error:
Anomaly
"Uncaught exception Failure("command \"/srv/src/coq/_build/install/default/lib/coq/plugins/micromega/csdpcert\" exited 127")."
Please report at http://coq.inria.fr/bugs/.

0m0.007s 0m0.000s
0m1.250s 0m0.558s
==========> FAILURE <==========
    micromega/rexample.v...Error! (should be accepted)

FAILURES
    micromega/bertot.v...Error! (should be accepted)
    micromega/example.v...Error! (should be accepted)
    micromega/qexample.v...Error! (should be accepted)
    micromega/rexample.v...Error! (should be accepted)
make[1]: *** [Makefile:214: report] Error 1
make[1]: Leaving directory '/srv/src/coq/_build/default/test-suite'
make: *** [Makefile:133: all] Error 2

dune.log

...
TEST      output/ltac.v 
TEST      output/Match_subterm.v 
GEN output/MExtraction.out
/bin/sh: output/MExtraction.out: Permission denied
make: *** [Makefile:481: output/MExtraction.out] Error 1
make: *** Deleting file 'output/MExtraction.out'
make: *** Waiting for unfinished jobs....

fix.diff

diff --git a/test-suite/Makefile b/test-suite/Makefile
index dece21885c..ca3c46d1ce 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -478,6 +478,7 @@ approve-output: output output-coqtop
 output/MExtraction.out: ../plugins/micromega/micromega.ml
 	$(SHOW) GEN $@
 	$(HIDE) cp $< $@
+	$(HIDE) chmod +w $@
 	$(HIDE) echo >> $@
 
 $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/run.sh b/test-suite/coq-makefile/findlib-package-unpacked/run.sh
index 6d7ae15ee2..1e2250bbd8 100755
--- a/test-suite/coq-makefile/findlib-package-unpacked/run.sh
+++ b/test-suite/coq-makefile/findlib-package-unpacked/run.sh
@@ -3,6 +3,7 @@
 . ../template/init.sh
 mv src/test_plugin.mlpack src/test_plugin.mllib
 
+chmod +w src/test_aux.ml
 echo "let () = Foolib.foo ();;" >> src/test_aux.ml
 export OCAMLPATH=$OCAMLPATH:$PWD/findlib
 if which cygpath 2>/dev/null; then
diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh
index 5cab400cc4..e43ae6c1e0 100755
--- a/test-suite/coq-makefile/findlib-package/run.sh
+++ b/test-suite/coq-makefile/findlib-package/run.sh
@@ -2,6 +2,8 @@
 
 . ../template/init.sh
 
+
+chmod +w src/test_aux.ml
 echo "let () = Foolib.foo ();;" >> src/test_aux.ml
 export OCAMLPATH=$OCAMLPATH:$PWD/findlib
 if which cygpath 2>/dev/null; then