Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add some minor results about single-step behavior of nth_error #17998

Merged
merged 2 commits into from
Sep 2, 2023

Add some minor results about single-step behavior of nth_error

a285183
Select commit
Failed to load commit list.
Merged

Add some minor results about single-step behavior of nth_error #17998

Add some minor results about single-step behavior of nth_error
a285183
Select commit
Failed to load commit list.
coqbot-app / GitLab CI job plugin:ci-metacoq (pull request) failed Sep 2, 2023 in 0s

Test has reached timeout on GitLab CI

This job has failed. If you need to, you can restart it directly in the GitHub interface using the "Re-run" button.

We show below the last 40 lines of the trace from GitLab (the complete trace is available here).

Details

findlib: [WARNING] Interface pCUICNormal.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface pCUICProgram.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface pCUICPrimitive.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface pCUICEqualityDec.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface pCUICTyping.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface pCUICPosition.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface ssrbool.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface pCUICErrors.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface pCUICSafeReduce.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface induction.cmi occurs in several directories: /builds/coq/coq/_build_ci/metacoq/test-suite/plugin-demo/../../template-coq/./gen-src, /builds/coq/coq/_install_ci/lib/coq-core/tactics
findlib: [WARNING] Interface pCUICAst.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
findlib: [WARNING] Interface pCUICWfEnv.cmi occurs in several directories: ../../safechecker-plugin/src, ../../erasure-plugin/src
src/demo_plugin.cmxs (real: 0.06, user: 0.03, sys: 0.02, mem: 19400 ko)
COQC theories/Loader.v
theories/Loader.vo (real: 0.12, user: 0.07, sys: 0.05, mem: 83784 ko)
COQC test/test.v
Notation plus := Nat.add
Expands to: Notation Coq.Init.Peano.plus
(1 + 2)
x: Point -> nat
y: Point -> nat
Build_Point: nat -> nat -> Point
_y: Lens Point Point nat nat
_x: Lens Point Point nat nat
test/test.vo (real: 0.51, user: 0.27, sys: 0.22, mem: 361312 ko)
make[4]: Leaving directory '/builds/coq/coq/_build_ci/metacoq/test-suite/plugin-demo'
make[3]: Leaving directory '/builds/coq/coq/_build_ci/metacoq/test-suite/plugin-demo'
coq_makefile -f _CoqProject -o Makefile.coq
Warning: ../utils/theories (used in -R or -Q) is not a subdirectory of the current directory

make -f Makefile.coq TIMED=pretty-timed
make[3]: Entering directory '/builds/coq/coq/_build_ci/metacoq/test-suite'
COQDEP VFILES
COQC bug1.v
bug1.vo (real: 2.28, user: 1.50, sys: 0.69, mem: 782228 ko)
COQC bug2.v
bug2.vo (real: 1.88, user: 1.42, sys: 0.42, mem: 782132 ko)
COQC bug369.v
ERROR: Job failed: execution took longer than 1h0m0s seconds
View more details on coqbot-app