Build:
- 0
2026-06-23 16:45.33: New job: build coq-core.8.18.0 (da442f99dfb1) 2026-06-23 16:45.33: Waiting for resource in pool day11-builds 2026-06-23 16:54.47: Got resource from pool day11-builds 2026-06-23 16:54.47: [profile full] build coq-core.8.18.0 2026-06-23 16:54.47: build coq-core.8.18.0 (da442f99dfb1) === DEPENDENCIES (11 transitive) === base-threads.base b7164ff76afe base-unix.base 839dc585f12d conf-gmp.5 61e3c79e0ddf conf-pkg-config.5 4b60827fc174 dune.3.23.1 433683e90514 ocaml.5.3.0 f3f5cb82ec5e ocaml-base-compiler.5.3.0 3282792848d7 ocaml-compiler.5.3.0 ec781058d2f3 ocaml-config.3 0df636be409d ocamlfind.1.9.8 814b8d0197a7 zarith.1.14 bed60daa9e32 === STDOUT === Processing: [default: loading data] [coq-core.8.18.0: dl] [coq-core.8.18.0: extract] -> retrieved coq-core.8.18.0 (https://opam.ocaml.org/cache) [coq-core: ./configure no] + /home/opam/.opam/default/.opam-switch/build/coq-core.8.18.0/./configure "-prefix" "/home/opam/.opam/default" "-mandir" "/home/opam/.opam/default/man" "-libdir" "/home/opam/.opam/default/lib/coq" "-native-compiler" "no" (CWD=/home/opam/.opam/default/.opam-switch/build/coq-core.8.18.0) - You have OCaml 5.3.0. Good! - You have OCamlfind 1.9.8. Good! - You have native-code compilation. Good! - You have the Zarith library 1.14 installed. Good! - - Architecture : Linux - Sys.os_type : Unix - OCaml version : 5.3.0 - OCaml binaries in : /home/opam/.opam/default/bin/ - OCaml library in : /home/opam/.opam/default/lib/ocaml - Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s & - Coq web site : http://coq.inria.fr/ - Bytecode VM enabled : true - Native Compiler enabled : no - - Paths where installation is expected by Coq Makefile: - - Coq is expected in /home/opam/.opam/default - - the Coq library is expected in /home/opam/.opam/default/lib/coq - - the Coqide configuration files is expected in /home/opam/.opam/default/etc/xdg/coq - - the Coqide data files is expected in /home/opam/.opam/default/share/coq - - the Coq man pages is expected in /home/opam/.opam/default/man - - documentation prefix path for all Coq packages is expected in /home/opam/.opam/default/share/doc - - If anything is wrong above, please restart './configure'. - - *Warning* To compile the system for a new architecture - don't forget to do a 'make clean' before './configure'. [coq-core: dune build] + /home/opam/.opam/default/bin/dune "build" "-p" "coq-core" "-j" "39" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/coq-core.8.18.0) - (cd _build/default && /usr/bin/bash -e -u -o pipefail -c dev/tools/make_git_revision.sh) > _build/default/revision - skipping make_git_revision: git dir not found - (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I kernel/.kernel.objs/byte -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 boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -no-alias-deps -o kernel/.kernel.objs/byte/float64.cmi -c -intf kernel/float64.mli) - File "kernel/float64.mli", line 60, characters 3-15: - 60 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64.mli", line 66, characters 3-15: - 66 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64.mli", line 80, characters 3-15: - 80 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64.mli", line 83, characters 3-15: - 83 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64.mli", line 89, characters 3-15: - 89 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64.mli", line 92, characters 3-15: - 92 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64.mli", line 101, characters 3-15: - 101 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64.mli", line 109, characters 3-15: - 109 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I kernel/.kernel.objs/byte -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 boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -no-alias-deps -o kernel/.kernel.objs/byte/float64_common.cmi -c -intf kernel/float64_common.mli) - File "kernel/float64_common.mli", line 60, characters 3-15: - 60 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64_common.mli", line 66, characters 3-15: - 66 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64_common.mli", line 70, characters 3-15: - 70 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64_common.mli", line 73, characters 3-15: - 73 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64_common.mli", line 79, characters 3-15: - 79 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64_common.mli", line 82, characters 3-15: - 82 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64_common.mli", line 91, characters 3-15: - 91 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/float64_common.mli", line 99, characters 3-15: - 99 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I kernel/.kernel.objs/byte -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 boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -cmi-file kernel/.kernel.objs/byte/uGraph.cmi -no-alias-deps -o kernel/.kernel.objs/byte/uGraph.cmo -c -impl kernel/uGraph.ml) - File "kernel/uGraph.ml", line 22, characters 10-17: - 22 | end) [@@inlined] (* without inline, +1% ish on HoTT, compcert. See jenkins 594 vs 596 *) - ^^^^^^^ - Warning 53 [misplaced-attribute]: the "inlined" attribute cannot appear in this context - (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I kernel/.kernel.objs/byte -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 boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -no-alias-deps -o kernel/.kernel.objs/byte/nativevalues.cmi -c -intf kernel/nativevalues.mli) - File "kernel/nativevalues.mli", line 104, characters 3-15: - 104 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 107, characters 3-15: - 107 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 110, characters 3-15: - 110 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 113, characters 3-15: - 113 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 124, characters 3-15: - 124 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 148, characters 3-15: - 148 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 192, characters 3-15: - 192 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 195, characters 3-15: - 195 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 198, characters 3-15: - 198 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 201, characters 3-15: - 201 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 204, characters 3-15: - 204 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 207, characters 3-15: - 207 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 210, characters 3-15: - 210 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 213, characters 3-15: - 213 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 216, characters 3-15: - 216 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 219, characters 3-15: - 219 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 222, characters 3-15: - 222 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 225, characters 3-15: - 225 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 228, characters 3-15: - 228 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 231, characters 3-15: - 231 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 234, characters 3-15: - 234 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 237, characters 3-15: - 237 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 240, characters 3-15: - 240 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 243, characters 3-15: - 243 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 246, characters 3-15: - 246 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 249, characters 3-15: - 249 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 252, characters 3-15: - 252 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 255, characters 3-15: - 255 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 258, characters 3-15: - 258 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 261, characters 3-15: - 261 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 264, characters 3-15: - 264 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 267, characters 3-15: - 267 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 270, characters 3-15: - 270 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 273, characters 3-15: - 273 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 282, characters 3-15: - 282 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 306, characters 3-15: - 306 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 309, characters 3-15: - 309 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 312, characters 3-15: - 312 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 315, characters 3-15: - 315 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 318, characters 3-15: - 318 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 321, characters 3-15: - 321 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 324, characters 3-15: - 324 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 327, characters 3-15: - 327 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 330, characters 3-15: - 330 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 333, characters 3-15: - 333 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 336, characters 3-15: - 336 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 339, characters 3-15: - 339 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 342, characters 3-15: - 342 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 345, characters 3-15: - 345 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 348, characters 3-15: - 348 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 351, characters 3-15: - 351 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 354, characters 3-15: - 354 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 357, characters 3-15: - 357 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 360, characters 3-15: - 360 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 375, characters 3-15: - 375 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 378, characters 3-15: - 378 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 381, characters 3-15: - 381 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 384, characters 3-15: - 384 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 387, characters 3-15: - 387 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 390, characters 3-15: - 390 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.inline" attribute cannot appear in this context - (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I pretyping/.pretyping.objs/byte -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 boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -cmi-file pretyping/.pretyping.objs/byte/inductiveops.cmi -no-alias-deps -o pretyping/.pretyping.objs/byte/inductiveops.cmo -c -impl pretyping/inductiveops.ml) - File "pretyping/inductiveops.ml", line 133, characters 3-19: - 133 | [@@ocaml.deprecated "Alias for Inductiveops.nconstructors"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 142, characters 3-19: - 142 | [@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 151, characters 3-19: - 151 | [@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 160, characters 3-19: - 160 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 169, characters 3-19: - 169 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 178, characters 3-19: - 178 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 187, characters 3-19: - 187 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 196, characters 3-19: - 196 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 205, characters 3-19: - 205 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 214, characters 3-19: - 214 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 223, characters 3-19: - 223 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 232, characters 3-19: - 232 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 241, characters 3-19: - 241 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 250, characters 3-19: - 250 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 257, characters 3-19: - 257 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -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 boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -cmi-file kernel/.kernel.objs/byte/uGraph.cmi -no-alias-deps -o kernel/.kernel.objs/native/uGraph.cmx -c -impl kernel/uGraph.ml) - File "kernel/uGraph.ml", line 22, characters 10-17: - 22 | end) [@@inlined] (* without inline, +1% ish on HoTT, compcert. See jenkins 594 vs 596 *) - ^^^^^^^ - Warning 53 [misplaced-attribute]: the "inlined" attribute cannot appear in this context - (cd _build/default/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -fPIC -pthread -D_FILE_OFFSET_BITS=64 -O2 -fno-strict-aliasing -fwrapv -fPIC -pthread -Wall -Wno-unused -g -O2 -msse2 -mfpmath=sse -g -I /home/opam/.opam/default/lib/ocaml -o coq_interp.o -c coq_interp.c) - coq_interp.c: In function 'coq_interprete': - coq_interp.c:816:11: warning: assignment discards 'volatile' qualifier from pointer target type [-Wdiscarded-qualifiers] - 816 | p = &Field(accu, 0); - | ^ - (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I tactics/.tactics.objs/byte -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 boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -no-alias-deps -o tactics/.tactics.objs/byte/hints.cmi -c -intf tactics/hints.mli) - File "tactics/hints.mli", line 200, characters 2-18: - 200 | [@ocaml.deprecated "Declare a hint constant instead"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -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 boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -cmi-file pretyping/.pretyping.objs/byte/inductiveops.cmi -no-alias-deps -o pretyping/.pretyping.objs/native/inductiveops.cmx -c -impl pretyping/inductiveops.ml) - File "pretyping/inductiveops.ml", line 133, characters 3-19: - 133 | [@@ocaml.deprecated "Alias for Inductiveops.nconstructors"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 142, characters 3-19: - 142 | [@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 151, characters 3-19: - 151 | [@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 160, characters 3-19: - 160 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 169, characters 3-19: - 169 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 178, characters 3-19: - 178 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 187, characters 3-19: - 187 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 196, characters 3-19: - 196 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 205, characters 3-19: - 205 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 214, characters 3-19: - 214 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 223, characters 3-19: - 223 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 232, characters 3-19: - 232 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 241, characters 3-19: - 241 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 250, characters 3-19: - 250 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context - - File "pretyping/inductiveops.ml", line 257, characters 3-19: - 257 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] - ^^^^^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the "ocaml.deprecated" attribute cannot appear in this context -> compiled coq-core.8.18.0 -> installed coq-core.8.18.0 [WARNING] Opam package conf-pkg-config.5 depends on the following system package that can no longer be found: pkg-config === STDERR === 2026-06-23 16:59.54: OK: build coq-core.8.18.0 (runc: 173.7s, disk: 39KB) 2026-06-23 16:59.54: Job succeeded