2026-09-28 15:45.59: New job: build coq-core.8.18.0 (a05166d2f522)
2026-09-28 15:45.59: Waiting for resource in pool day11-builds
2026-09-28 15:47.14: Got resource from pool day11-builds
2026-09-28 15:47.14: [profile oxcaml-odoc-master] build coq-core.8.18.0
2026-09-28 15:47.14: build coq-core.8.18.0 (a05166d2f522)
=== DEPENDENCIES (12 transitive) ===
  base-threads.base                                  ddcab511c589
  base-unix.base                                     742554e1dbc2
  conf-autoconf.1                                    43fe4a407b7a
  conf-gmp.5                                         00570d20295f
  conf-which.1                                       5fccb3a41099
  dune.3.22.2+ox                                     057b1ed5957b
  ocaml.5.4.0                                        74a2c67841c6
  ocaml-config.3                                     d58db97ddfef
  ocaml-variants.5.4.0+ox                            4babdc19da91
  ocamlfind.1.9.8+ox                                 47b14ae6bc12
  oxcaml-compiler.5.4.0-ox7                          42053eeff39a
  zarith.1.12+ox3                                    7530a50bde9e
=== 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.4.0+ox. Good!
- You have OCamlfind 1.9.8. Good!
- You have native-code compilation. Good!
- You have the Zarith library 1.12 installed. Good!
- 
-   Architecture                : Linux
-   Sys.os_type                 : Unix
-   OCaml version               : 5.4.0+ox
-   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 -bin-annot-cms -I clib/.clib.objs/byte -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -cmi-file clib/.clib.objs/byte/int.cmi -no-alias-deps -o clib/.clib.objs/byte/int.cmo -c -impl clib/int.ml)
- File "clib/int.ml", line 1:
- Error: The implementation clib/int.ml
-        does not match the interface clib/.clib.objs/byte/int.cmi:  ...
-        In module List:
-        Values do not match:
-          val mem : 'a @ local -> 'a list @ local -> bool
-        is not included in
-          val mem : int -> int list -> bool
-        The type int @ local -> int list @ local -> bool
-        is not compatible with the type int -> int list -> bool
-        File "clib/int.mli", line 25, characters 2-35: Expected declaration
-        File "clib/int.ml", line 61, characters 6-9: Actual declaration
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -bin-annot-cms -I lib/.lib.objs/byte -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 -cmi-file lib/.lib.objs/byte/control.cmi -no-alias-deps -o lib/.lib.objs/byte/control.cmo -c -impl lib/control.ml)
- File "lib/control.ml", line 39, characters 14-24:
- 39 |     let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-                    ^^^^^^^^^^
- Alert unsafe_multidomain: Stdlib.Sys.signal
- Use [Sys.Safe.signal].
- 
- File "lib/control.ml", line 48, characters 6-20:
- 48 |       Sys.set_signal Sys.sigalrm psh
-            ^^^^^^^^^^^^^^
- Alert unsafe_multidomain: Stdlib.Sys.set_signal
- Use [Sys.Safe.set_signal].
- 
- File "lib/control.ml", line 116, characters 22-32:
- 116 |     let old_handler = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-                             ^^^^^^^^^^
- Alert unsafe_multidomain: Stdlib.Sys.signal
- Use [Sys.Safe.signal].
- 
- File "lib/control.ml", line 119, characters 6-20:
- 119 |       Sys.set_signal Sys.sigalrm old_handler;
-             ^^^^^^^^^^^^^^
- Alert unsafe_multidomain: Stdlib.Sys.set_signal
- Use [Sys.Safe.set_signal].
- 
- File "lib/control.ml", line 125, characters 6-20:
- 125 |       Sys.set_signal Sys.sigalrm old_handler;
-             ^^^^^^^^^^^^^^
- Alert unsafe_multidomain: Stdlib.Sys.set_signal
- Use [Sys.Safe.set_signal].
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I clib/.clib.objs/byte -I clib/.clib.objs/native -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -cmi-file clib/.clib.objs/byte/int.cmi -no-alias-deps -o clib/.clib.objs/native/int.cmx -c -impl clib/int.ml)
- File "clib/int.ml", line 1:
- Error: The implementation clib/int.ml
-        does not match the interface clib/.clib.objs/byte/int.cmi:  ...
-        In module List:
-        Values do not match:
-          val mem : 'a @ local -> 'a list @ local -> bool
-        is not included in
-          val mem : int -> int list -> bool
-        The type int @ local -> int list @ local -> bool
-        is not compatible with the type int -> int list -> bool
-        File "clib/int.mli", line 25, characters 2-35: Expected declaration
-        File "clib/int.ml", line 61, characters 6-9: Actual declaration
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -bin-annot-cms -I lib/.lib.objs/byte -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 -cmi-file lib/.lib.objs/byte/envars.cmi -no-alias-deps -o lib/.lib.objs/byte/envars.cmo -c -impl lib/envars.ml)
- File "lib/envars.ml", line 111, characters 4-15:
- 111 |     Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> ""))
-           ^^^^^^^^^^^
- Alert unsafe_multidomain: Unix.putenv
- Mutating the environment makes reading the environment unsafe.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -bin-annot-cms -I lib/.lib.objs/byte -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 -cmi-file lib/.lib.objs/byte/cErrors.cmi -no-alias-deps -o lib/.lib.objs/byte/cErrors.cmo -c -impl lib/cErrors.ml)
- File "lib/cErrors.ml", line 26, characters 2-27:
- 26 |   Printexc.register_printer pr
-        ^^^^^^^^^^^^^^^^^^^^^^^^^
- Alert unsafe_multidomain: Stdlib.Printexc.register_printer
- Use [Printexc.Safe.register_printer].
- 
- File "lib/cErrors.ml", line 39, characters 8-33:
- 39 | let _ = Printexc.register_printer (function
-              ^^^^^^^^^^^^^^^^^^^^^^^^^
- Alert unsafe_multidomain: Stdlib.Printexc.register_printer
- Use [Printexc.Safe.register_printer].
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -bin-annot-cms -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 -bin-annot-cms -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 -bin-annot-cms -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 -bin-annot-cms -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/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 -bin-annot-cms -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/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -bin-annot-cms -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/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -bin-annot-cms -I plugins/ltac/.ltac_plugin.objs/byte -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 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 -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -cmi-file plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tactic_debug.cmi -no-alias-deps -open Ltac_plugin -o plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tactic_debug.cmo -c -impl plugins/ltac/tactic_debug.ml)
- File "plugins/ltac/tactic_debug.ml", line 477, characters 4-18:
- 477 |     Sys.set_signal Sys.sigusr1 (Sys.Signal_handle
-           ^^^^^^^^^^^^^^
- Alert unsafe_multidomain: Stdlib.Sys.set_signal
- Use [Sys.Safe.set_signal].
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -bin-annot-cms -I plugins/micromega/.micromega_plugin.objs/byte -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 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 plugins/ltac/.ltac_plugin.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -cmi-file plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__NumCompat.cmi -no-alias-deps -open Micromega_plugin -o plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__NumCompat.cmo -c -impl plugins/micromega/numCompat.ml)
- File "plugins/micromega/numCompat.ml", lines 106-169, characters 38-3:
- 106 | ......................................struct
- 107 |   module Z = Z
- 108 | 
- 109 |   let pow_check_exp x y =
- 110 |     let z_res =
- ...
- 166 |       (* CErrors.user_err (Pp.str "[micromega] overflow in exponentiation") *)
- 167 |     in
- 168 |     pow_check_exp (Z.of_int x) y
- 169 | end
- Error: Signature mismatch:
-        ...
-        ...
-        In module Notations:
-        Values do not match:
-          val ( =/ ) : Q.t @ local -> Q.t @ local -> bool
-        is not included in
-          val ( =/ ) : t -> t -> bool
-        The type Q.t @ local -> Q.t @ local -> bool
-        is not compatible with the type t -> t -> bool
-        File "plugins/micromega/numCompat.ml", line 71, characters 4-31:
-          Expected declaration
-        File "plugins/micromega/numCompat.ml", line 129, characters 8-14:
-          Actual declaration
[ERROR] The compilation of coq-core.8.18.0 failed at "dune build -p coq-core -j 39 @install".
build failed... 

=== STDERR ===

2026-09-28 15:50.24: FAILED: build coq-core.8.18.0
2026-09-28 15:50.24: Job failed: build failed: coq-core.8.18.0