2026-06-24 16:20.00: New job: build coq-waterproof.3.0.0+8.20 (08508f23342a)
2026-06-24 16:20.00: Waiting for resource in pool day11-builds
2026-06-24 17:14.32: Got resource from pool day11-builds
2026-06-24 17:14.32: [profile full] build coq-waterproof.3.0.0+8.20
2026-06-24 17:14.32: build coq-waterproof.3.0.0+8.20 (08508f23342a)
=== DEPENDENCIES (16 transitive) ===
  base-threads.base                                  c9e7bdbf5823
  base-unix.base                                     7d1428be9ddb
  conf-gmp.5                                         be11edf77089
  conf-linux-libc-dev.0                              2d4ad9bc3a8f
  conf-pkg-config.5                                  d5de2c6a88f9
  coq.8.20.1                                         635aebac49ab
  coq-core.8.20.1                                    6b2c9fd7972e
  coq-stdlib.8.20.1                                  d9560a7ae934
  coqide-server.8.20.1                               4e223a0e963b
  dune.3.23.1                                        dc7ac21ea3be
  ocaml.5.4.1                                        71fed6f83b21
  ocaml-base-compiler.5.4.1                          4b8cbe74bda9
  ocaml-compiler.5.4.1                               df07189447bd
  ocaml-config.3                                     e4a06a221f09
  ocamlfind.1.9.8                                    567e34ecf540
  zarith.1.14                                        442c15edac63
=== STDOUT ===
Processing: [default: loading data]
[coq-waterproof.3.0.0+8.20: dl]
[coq-waterproof.3.0.0+8.20: extract]
-> retrieved coq-waterproof.3.0.0+8.20  (https://opam.ocaml.org/cache)
[coq-waterproof: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "coq-waterproof" "-j" "39" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/coq-waterproof.3.0.0+8.20)
- (cd _build/default/theories && /home/opam/.opam/default/bin/coqdep -boot -I /home/opam/.opam/default/lib/coq-core/boot -I /home/opam/.opam/default/lib/coq-core/clib -I /home/opam/.opam/default/lib/coq-core/config -I /home/opam/.opam/default/lib/coq-core/engine -I /home/opam/.opam/default/lib/coq-core/gramlib -I /home/opam/.opam/default/lib/coq-core/interp -I /home/opam/.opam/default/lib/coq-core/kernel -I /home/opam/.opam/default/lib/coq-core/lib -I /home/opam/.opam/default/lib/coq-core/library -I /home/opam/.opam/default/lib/coq-core/parsing -I /home/opam/.opam/default/lib/coq-core/perf -I /home/opam/.opam/default/lib/coq-core/plugins/ltac -I /home/opam/.opam/default/lib/coq-core/plugins/ltac2 -I /home/opam/.opam/default/lib/coq-core/pretyping -I /home/opam/.opam/default/lib/coq-core/printing -I /home/opam/.opam/default/lib/coq-core/proofs -I /home/opam/.opam/default/lib/coq-core/tactics -I /home/opam/.opam/default/lib/coq-core/vernac -I /home/opam/.opam/default/lib/coq-core/vm -I /home/opam/.opam/default/lib/findlib -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/zarith -I ../src -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/btauto -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/cc -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/derive -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/extraction -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/firstorder -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/funind -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ltac -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ltac2 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ltac2_ltac1 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/micromega -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/micromega_core -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/nsatz -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/number_string_notation -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ring -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/rtauto -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ssreflect -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ssrmatching -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tauto -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tutorial/p0 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tutorial/p1 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tutorial/p2 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tutorial/p3 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/zify -R /home/opam/.opam/default/lib/coq/theories Coq -Q /home/opam/.opam/default/lib/coq/user-contrib/Ltac2 Ltac2 -R . Waterproof -dyndep opt -vos Util/TypeCorrector.v Util/MessagesToUser.v Util/Init.v Util/Hypothesis.v Util/Goals.v Util/Evars.v Util/Constr.v Util/BySince.v Util/Binders.v Util/Assertions.v Tactics/Unfold.v Tactics/ToShow.v Tactics/Take.v Tactics/Specialize.v Tactics/Obtain.v Tactics/ItSuffices.v Tactics/ItHolds.v Tactics/Induction.v Tactics/Help.v Tactics/Either.v Tactics/Define.v Tactics/Contradiction.v Tactics/Conclusion.v Tactics/Claims.v Tactics/Choose.v Tactics/BothStatements.v Tactics/BothDirections.v Tactics/Because.v Tactics/Assume.v Notations/Sets.v Notations/RealsWithSubsets.v Notations/Reals.v Notations/Integers.v Notations/IndexedSets.v Notations/Functions.v Notations/Common.v Libs/Sets/Operations.v Libs/Sets/IndexedOperations.v Libs/Reals/RealInequalities.v Libs/Reals/Rational.v Libs/Reals/Intervals.v Libs/Reals/Integer.v Libs/Reals/ArchimedN.v Libs/Logic/Quantification.v Libs/Logic/InformativeEpsilon.v Libs/Logic/ConstructiveLogic.v Libs/Integers/Square.v Libs/Integers/Even.v Libs/Integers/Divisibility.v Libs/Analysis/SupAndInf.v Libs/Analysis/SubsequencesMetric.v Libs/Analysis/Subsequences.v Libs/Analysis/StrongInductionIndexSequence.v Libs/Analysis/Series.v Libs/Analysis/SequentialAccumulationPoints.v Libs/Analysis/SequencesMetric.v Libs/Analysis/Sequences.v Libs/Analysis/OpenAndClosed.v Libs/Analysis/MetricSpaces.v Libs/Analysis/LimsupLiminfBolzano.v Libs/Analysis/ContinuityDomainR.v Libs/Analysis/ContinuityDomainNat.v Libs/Sets.v Libs/Reals.v Libs/Negation.v Libs/Logic.v Libs/Integers.v Libs/Functions.v Libs/Analysis.v Chains/Manipulation.v Chains/Inequalities.v Automation/Hints.v Waterprove.v Waterproof.v Version.v Tactics.v Notations.v Chains.v Automation.v) > _build/default/theories/.Waterproof.theory.d
- Warning: in file Waterproof.v, declared ML module waterproof has not been found!
-          [declared-module-not-found,filesystem,default]
- (cd _build/default && /home/opam/.opam/default/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /home/opam/.opam/default/lib/coq-core/boot -I /home/opam/.opam/default/lib/coq-core/clib -I /home/opam/.opam/default/lib/coq-core/config -I /home/opam/.opam/default/lib/coq-core/engine -I /home/opam/.opam/default/lib/coq-core/gramlib -I /home/opam/.opam/default/lib/coq-core/interp -I /home/opam/.opam/default/lib/coq-core/kernel -I /home/opam/.opam/default/lib/coq-core/lib -I /home/opam/.opam/default/lib/coq-core/library -I /home/opam/.opam/default/lib/coq-core/parsing -I /home/opam/.opam/default/lib/coq-core/perf -I /home/opam/.opam/default/lib/coq-core/plugins/ltac -I /home/opam/.opam/default/lib/coq-core/plugins/ltac2 -I /home/opam/.opam/default/lib/coq-core/pretyping -I /home/opam/.opam/default/lib/coq-core/printing -I /home/opam/.opam/default/lib/coq-core/proofs -I /home/opam/.opam/default/lib/coq-core/tactics -I /home/opam/.opam/default/lib/coq-core/vernac -I /home/opam/.opam/default/lib/coq-core/vm -I /home/opam/.opam/default/lib/findlib -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/zarith -I src -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/btauto -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/cc -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/derive -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/extraction -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/firstorder -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/funind -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ltac -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ltac2 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ltac2_ltac1 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/micromega -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/micromega_core -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/nsatz -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/number_string_notation -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ring -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/rtauto -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ssreflect -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/ssrmatching -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tauto -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tutorial/p0 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tutorial/p1 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tutorial/p2 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/tutorial/p3 -I /home/opam/.opam/default/lib/coq/../coq-core/plugins/zify -R /home/opam/.opam/default/lib/coq/theories Coq -Q /home/opam/.opam/default/lib/coq/user-contrib/Ltac2 Ltac2 -R theories Waterproof theories/Waterproof.v)
- File "./theories/Waterproof.v", line 20, characters 0-53:
- Error: Can't find file waterproof.cmxs on loadpath.
- 
[ERROR] The compilation of coq-waterproof.3.0.0+8.20 failed at "dune build -p coq-waterproof -j 39 @install".
build failed... 

=== STDERR ===

2026-06-24 17:14.59: FAILED: build coq-waterproof.3.0.0+8.20
2026-06-24 17:14.59: Job failed: build failed: coq-waterproof.3.0.0+8.20