Build:
- 0
2026-06-24 12:11.37: New job: build coq-core.8.19.2 (b1f40b559eda) 2026-06-24 12:11.37: Waiting for resource in pool day11-builds 2026-06-24 13:36.18: Got resource from pool day11-builds 2026-06-24 13:36.18: [profile full] build coq-core.8.19.2 2026-06-24 13:36.18: build coq-core.8.19.2 (b1f40b559eda) === DEPENDENCIES (12 transitive) === base-threads.base c9e7bdbf5823 base-unix.base 7d1428be9ddb conf-gmp.5 be11edf77089 conf-linux-libc-dev.0 2d4ad9bc3a8f conf-pkg-config.5 d5de2c6a88f9 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-core.8.19.2: dl] [coq-core.8.19.2: extract] -> retrieved coq-core.8.19.2 (https://opam.ocaml.org/cache) [coq-core: ./configure no] + /home/opam/.opam/default/.opam-switch/build/coq-core.8.19.2/./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.19.2) - You have OCaml 5.4.1. 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.4.1 - 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" "--promote-install-files=false" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/coq-core.8.19.2) - (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 -I perf/.coqperf.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 -I perf/.coqperf.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 -I perf/.coqperf.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 23, characters 10-17: - 23 | 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 -I perf/.coqperf.objs/byte -no-alias-deps -o kernel/.kernel.objs/byte/nativevalues.cmi -c -intf kernel/nativevalues.mli) - File "kernel/nativevalues.mli", line 103, characters 3-15: - 103 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 106, characters 3-15: - 106 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 109, characters 3-15: - 109 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 112, characters 3-15: - 112 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 123, characters 3-15: - 123 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 147, characters 3-15: - 147 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 191, characters 3-15: - 191 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 194, characters 3-15: - 194 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 197, characters 3-15: - 197 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 200, characters 3-15: - 200 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 203, characters 3-15: - 203 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 206, characters 3-15: - 206 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 209, characters 3-15: - 209 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 212, characters 3-15: - 212 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 215, characters 3-15: - 215 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 218, characters 3-15: - 218 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 221, characters 3-15: - 221 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 224, characters 3-15: - 224 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 227, characters 3-15: - 227 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 230, characters 3-15: - 230 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 233, characters 3-15: - 233 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 236, characters 3-15: - 236 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 239, characters 3-15: - 239 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 242, characters 3-15: - 242 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 245, characters 3-15: - 245 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 248, characters 3-15: - 248 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 251, characters 3-15: - 251 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 254, characters 3-15: - 254 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 257, characters 3-15: - 257 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 260, characters 3-15: - 260 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 263, characters 3-15: - 263 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 266, characters 3-15: - 266 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 269, characters 3-15: - 269 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 272, characters 3-15: - 272 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 281, characters 3-15: - 281 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 305, characters 3-15: - 305 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 308, characters 3-15: - 308 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 311, characters 3-15: - 311 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 314, characters 3-15: - 314 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 317, characters 3-15: - 317 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 320, characters 3-15: - 320 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 323, characters 3-15: - 323 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 326, characters 3-15: - 326 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 329, characters 3-15: - 329 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 332, characters 3-15: - 332 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 335, characters 3-15: - 335 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 338, characters 3-15: - 338 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 341, characters 3-15: - 341 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 344, characters 3-15: - 344 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 347, characters 3-15: - 347 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 350, characters 3-15: - 350 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 353, characters 3-15: - 353 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 356, characters 3-15: - 356 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 359, characters 3-15: - 359 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 374, characters 3-15: - 374 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 377, characters 3-15: - 377 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 380, characters 3-15: - 380 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 383, characters 3-15: - 383 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 386, characters 3-15: - 386 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context - - File "kernel/nativevalues.mli", line 389, characters 3-15: - 389 | [@@ocaml.inline always] - ^^^^^^^^^^^^ - Warning 53 [misplaced-attribute]: the ocaml.inline 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:827:11: warning: assignment discards 'volatile' qualifier from pointer target type [-Wdiscarded-qualifiers] - 827 | p = &Field(accu, 0); - | ^ - (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 -I perf/.coqperf.objs/byte -I perf/.coqperf.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 23, characters 10-17: - 23 | 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 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 perf/.coqperf.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 [coq-core: dune install] + /home/opam/.opam/default/bin/dune "install" "-p" "coq-core" "--create-install-files" "coq-core" (CWD=/home/opam/.opam/default/.opam-switch/build/coq-core.8.19.2) -> compiled coq-core.8.19.2 -> installed coq-core.8.19.2 [WARNING] Opam package conf-pkg-config.5 depends on the following system package that can no longer be found: pkg-config === STDERR === 2026-06-24 13:39.14: OK: build coq-core.8.19.2 (runc: 140.2s, disk: 30KB) 2026-06-24 13:39.14: Job succeeded