Build:
- 0
2026-06-16 11:52.14: New job: build coq-core.8.19.2 (8206933664ce) 2026-06-16 11:52.14: Waiting for resource in pool day11-builds 2026-06-16 12:16.33: Got resource from pool day11-builds 2026-06-16 12:16.33: [profile full] build coq-core.8.19.2 2026-06-16 12:16.34: build coq-core.8.19.2 (8206933664ce) === DEPENDENCIES (11 transitive) === base-threads.base b7164ff76afe base-unix.base 839dc585f12d conf-gmp.5 61e3c79e0ddf conf-linux-libc-dev.0 096e638ca371 conf-pkg-config.5 64c6b37d622b dune.3.23.1 9174d78a1f0e ocaml.5.2.1 b36a3a003df3 ocaml-base-compiler.5.2.1 91ea68ae8779 ocaml-config.3 291db63d419b ocamlfind.1.9.6 36f1f9a3ee82 zarith.1.14 058558459586 === 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.2.1. Good! - You have OCamlfind 1.9.6. 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.2.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 && /home/opam/.opam/default/bin/ocamlopt.opt -I topbin/.coqc_bin.eobjs/byte -I topbin/.coqc_bin.eobjs/native -I /home/opam/.opam/default/lib/findlib -I /home/opam/.opam/default/lib/ocaml/dynlink -cmi-file topbin/.coqc_bin.eobjs/byte/findlib_initl.cmi -no-alias-deps -opaque -o topbin/.coqc_bin.eobjs/native/findlib_initl.cmx -c -impl topbin/.coqc_bin.eobjs/findlib_initl.ml-gen) - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Findlib, and its interface was not compiled with -opaque - (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -I topbin/.coqworker_bin.eobjs/byte -I topbin/.coqworker_bin.eobjs/native -I /home/opam/.opam/default/lib/findlib -I /home/opam/.opam/default/lib/ocaml/dynlink -cmi-file topbin/.coqworker_bin.eobjs/byte/findlib_initl.cmi -no-alias-deps -opaque -o topbin/.coqworker_bin.eobjs/native/findlib_initl.cmx -c -impl topbin/.coqworker_bin.eobjs/findlib_initl.ml-gen) - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Findlib, and its interface was not compiled with -opaque - (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -I topbin/.coqtop_bin.eobjs/byte -I topbin/.coqtop_bin.eobjs/native -I /home/opam/.opam/default/lib/findlib -I /home/opam/.opam/default/lib/ocaml/dynlink -cmi-file topbin/.coqtop_bin.eobjs/byte/findlib_initl.cmi -no-alias-deps -opaque -o topbin/.coqtop_bin.eobjs/native/findlib_initl.cmx -c -impl topbin/.coqtop_bin.eobjs/findlib_initl.ml-gen) - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Findlib, and its interface was not compiled with -opaque - (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -I plugins/micromega/.csdpcert.eobjs/byte -I plugins/micromega/.csdpcert.eobjs/native -I /home/opam/.opam/default/lib/findlib -I /home/opam/.opam/default/lib/ocaml/dynlink -cmi-file plugins/micromega/.csdpcert.eobjs/byte/findlib_initl.cmi -no-alias-deps -opaque -o plugins/micromega/.csdpcert.eobjs/native/findlib_initl.cmx -c -impl plugins/micromega/.csdpcert.eobjs/findlib_initl.ml-gen) - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Findlib, and its interface was not compiled with -opaque - (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 && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I tools/coqdep/lib/.coqdeplib.objs/byte -I tools/coqdep/lib/.coqdeplib.objs/native -I /home/opam/.opam/default/lib/findlib -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 lib/.lib.objs/byte -I lib/.lib.objs/native -I perf/.coqperf.objs/byte -I perf/.coqperf.objs/native -cmi-file tools/coqdep/lib/.coqdeplib.objs/byte/coqdeplib__Fl.cmi -no-alias-deps -open Coqdeplib -o tools/coqdep/lib/.coqdeplib.objs/native/coqdeplib__Fl.cmx -c -impl tools/coqdep/lib/fl.ml) - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Findlib, and its interface was not compiled with -opaque - - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Fl_metascanner, and its interface was not compiled with -opaque - - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Fl_package_base, and its interface was not compiled with -opaque - (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 - (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/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -pthread -D_FILE_OFFSET_BITS=64 -O2 -fno-strict-aliasing -fwrapv -pthread -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 vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -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 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 gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.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 -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I perf/.coqperf.objs/byte -I perf/.coqperf.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -cmi-file vernac/.vernac.objs/byte/mltop.cmi -no-alias-deps -o vernac/.vernac.objs/native/mltop.cmx -c -impl vernac/mltop.ml) - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Findlib, and its interface was not compiled with -opaque - - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Fl_dynload, and its interface was not compiled with -opaque - - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Fl_package_base, and its interface was not compiled with -opaque - (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -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 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 gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.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 -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I perf/.coqperf.objs/byte -I perf/.coqperf.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -cmi-file sysinit/.sysinit.objs/byte/coqinit.cmi -no-alias-deps -o sysinit/.sysinit.objs/native/coqinit.cmx -c -impl sysinit/coqinit.ml) - File "_none_", line 1: - Warning 58 [no-cmx-file]: no cmx file was found in path for module Findlib, and its interface was not compiled with -opaque [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-16 12:19.40: OK: build coq-core.8.19.2 (runc: 153.2s, disk: 37KB) 2026-06-16 12:19.40: Job succeeded