Remove deprecated files in Arith and Numbers/Natural #18164
Merged
coqbot-app / GitLab CI job library:ci-fiat_crypto (pull request)
completed
Nov 27, 2023 in 0s
Test has failed on GitLab CI
This job is allowed to fail.
This job ran on the Docker image registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2023-08-28-93124ee272, depended on the build job build:edge+flambda with OCaml 4.14.1+flambda.
We show below an excerpt from the trace from GitLab starting around the last detected "Error" (the complete trace is available here).
Details
File "/builds/coq/coq/_build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Arrays.v", line 282, characters 34-52:
Error: The reference Min.min_idempotent was not found in the current
environment.
Command exited with non-zero status 1
/builds/coq/coq/_build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Arrays.vo (real: 0.93, user: 0.67, sys: 0.25, mem: 500512 ko)
make[4]: *** [Makefile.coq:847: /builds/coq/coq/_build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Arrays.vo] Error 1
make[4]: *** [/builds/coq/coq/_build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Arrays.vo] Deleting file '/builds/coq/coq/_build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Arrays.glob'
make[3]: *** [Makefile.coq:417: all] Error 2
make[2]: *** [Makefile:15: all] Error 2
make[1]: *** No rule to make target 'rupicola', needed by '.Makefile.coq.d'. Stop.
make[1]: Leaving directory '/builds/coq/coq/_build_ci/fiat_crypto'
Aggregating timing log...
Time | Peak Mem | File Name
--------------------------------------------------------------------------------------------------------------
0m34.23s | 522816 ko | Total Time / Peak Mem
--------------------------------------------------------------------------------------------------------------
0m06.20s | 522816 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Examples/CapitalizeThird/Properties.vo
0m05.68s | 516680 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Loops.vo
0m04.27s | 503540 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Core.vo
0m01.83s | 501524 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/InlineTables.vo
0m01.74s | 497972 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Compiler.vo
0m00.99s | 505344 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/ExprCompiler.vo
0m00.85s | 496160 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/NoExprReflection.vo
0m00.77s | 496636 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Examples/Net/IPChecksum/Spec.vo
0m00.75s | 492952 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Examples/Swap/Properties.vo
0m00.72s | 501048 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/ExprReflection.vo
0m00.67s | 500512 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Arrays.vo
0m00.65s | 478720 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Examples/KVStore/kv.vo
0m00.65s | 502860 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/SepLocals.vo
0m00.65s | 494144 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/SepReflection.vo
0m00.63s | 496948 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Alloc.vo
0m00.60s | 461032 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Examples/CRC32/Table.vo
0m00.58s | 493224 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Conditionals.vo
0m00.57s | 465988 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/ToCString.vo
0m00.56s | 414244 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Notations.vo
0m00.55s | 400764 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Tactics.vo
0m00.54s | 445424 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Monads.vo
0m00.49s | 414084 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Lib/Invariants.vo
0m00.48s | 375008 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Examples/Swap/Swap.vo