dune.2.log

...
CHECK     success/Nia.v
make report
make[1]: Entering directory '/srv/src/coq/_build/default/test-suite'
BUILDING SUMMARY FILE
logs/bugs/closed/bug_5127.v.log
==========> TESTING bugs/closed/bug_5127.v <==========
File "./bugs/closed/bug_5127.v", line 13, characters 0-22:
Warning: To avoid stack overflow, large numbers in nat are interpreted as
applications of Nat.of_uint. [abstract-large-number,numbers]
0m0.007s 0m0.001s
0m24.715s 0m0.704s
==========> FAILURE <==========
    bugs/closed/bug_5127.v...Error! (bug seems to be opened, please check)

logs/coq-makefile/findlib-package.log
run.sh: line 5: src/test_aux.ml: Permission denied
==========> FAILURE <==========
    coq-makefile/findlib-package/run.sh...Error!

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.006s 0m0.000s
0m0.836s 0m0.401s
==========> 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.003s 0m0.005s
0m0.886s 0m0.557s
==========> 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.007s 0m0.000s
0m0.849s 0m0.440s
==========> 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.002s 0m0.005s
0m1.209s 0m0.509s
==========> FAILURE <==========
    micromega/rexample.v...Error! (should be accepted)

FAILURES
    bugs/closed/bug_5127.v...Error! (bug seems to be opened, please check)
    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)
    coq-makefile/findlib-package/run.sh...Error!
make[1]: *** [Makefile:214: report] Error 1
make[1]: Leaving directory '/srv/src/coq/_build/default/test-suite'
make: *** [Makefile:133: all] Error 2