Build:
- 0
2026-10-01 23:21.00: New job: build rocq-runtime.9.2.0 (318466afdedf) 2026-10-01 23:21.00: Waiting for resource in pool day11-builds 2026-10-01 23:24.23: Got resource from pool day11-builds 2026-10-01 23:24.23: [profile oxcaml-odoc-master] build rocq-runtime.9.2.0 2026-10-01 23:24.27: build rocq-runtime.9.2.0 (318466afdedf) === DEPENDENCIES (13 transitive) === base-threads.base ddcab511c589 base-unix.base 742554e1dbc2 conf-autoconf.1 43fe4a407b7a conf-gmp.5 00570d20295f conf-linux-libc-dev.0 6a88f9847ca1 conf-which.1 5fccb3a41099 dune.3.22.2+ox a2ef013eeea9 ocaml.5.2.0 cda6777ccfe3 ocaml-config.3 d77b853eaa33 ocaml-variants.5.2.0+ox a9808a9375cd ocamlfind.1.9.8+ox f23a347b8f5f oxcaml-compiler.5.2.0minus39 9c94ae342626 zarith.1.12+ox3 f6ec0c6300f3 === STDOUT === Processing: [default: loading data] [rocq-runtime.9.2.0: dl] [rocq-runtime.9.2.0: extract] -> retrieved rocq-runtime.9.2.0 (https://opam.ocaml.org/cache) [rocq-runtime: ./configure no] + /home/opam/.opam/default/.opam-switch/build/rocq-runtime.9.2.0/./configure "-release" "-prefix" "/home/opam/.opam/default" "-libdir" "/home/opam/.opam/default/lib/coq" "-native-compiler" "no" (CWD=/home/opam/.opam/default/.opam-switch/build/rocq-runtime.9.2.0) - You have OCaml 5.2.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.2.0+ox - OCaml binaries in : /home/opam/.opam/default/bin/ - OCaml library in : /home/opam/.opam/default/lib/ocaml - Web browser : xdg-open "%s" - Rocq web site : http://rocq-prover.org/ - Bytecode VM enabled : true - Native Compiler enabled : no - - Paths where installation is expected by Rocq Makefile: - - Prefix is expected in /home/opam/.opam/default - - the Rocq library is expected in /home/opam/.opam/default/lib/coq - - the Rocqide configuration files is expected in /home/opam/.opam/default/etc/xdg/coq - - the Rocqide data files is expected in /home/opam/.opam/default/share/coq - - documentation prefix path for all Rocq 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'. [rocq-runtime: dune build] + /home/opam/.opam/default/bin/dune "build" "-p" "rocq-runtime" "-j" "39" "--promote-install-files=false" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/rocq-runtime.9.2.0) - (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 94, characters 6-9: Actual declaration - (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 94, 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 -I perf/.coqperf.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 111, characters 22-32: - 111 | 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 114, characters 6-20: - 114 | Sys.set_signal Sys.sigalrm old_handler; - ^^^^^^^^^^^^^^ - Alert unsafe_multidomain: Stdlib.Sys.set_signal - Use [Sys.Safe.set_signal]. - - File "lib/control.ml", line 120, characters 6-20: - 120 | 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/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -bin-annot-cms -I topbin/.rocqshim.objs/byte -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 clib/.clib.objs/byte -I config/.config.objs/byte -cmi-file topbin/.rocqshim.objs/byte/rocqshim.cmi -no-alias-deps -o topbin/.rocqshim.objs/byte/rocqshim.cmo -c -impl topbin/rocqshim.ml) - File "topbin/rocqshim.ml", line 96, characters 26-37: - 96 | | None -> Unix.putenv n v - ^^^^^^^^^^^ - Alert unsafe_multidomain: Unix.putenv - Mutating the environment makes reading the environment unsafe. - (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 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 -I perf/.coqperf.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 22, characters 2-27: - 22 | Printexc.register_printer pr - ^^^^^^^^^^^^^^^^^^^^^^^^^ - Alert unsafe_multidomain: Stdlib.Printexc.register_printer - Use [Printexc.Safe.register_printer]. - - File "lib/cErrors.ml", line 35, characters 8-33: - 35 | 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 plugins/micromega/.micromega_core_plugin.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 /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -cmi-file plugins/micromega/.micromega_core_plugin.objs/byte/micromega_core_plugin__NumCompat.cmi -no-alias-deps -open Micromega_core_plugin -o plugins/micromega/.micromega_core_plugin.objs/byte/micromega_core_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 - (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 -I perf/.coqperf.objs/byte -cmi-file kernel/.kernel.objs/byte/vmbytegen.cmi -no-alias-deps -o kernel/.kernel.objs/byte/vmbytegen.cmo -c -impl kernel/vmbytegen.ml) - File "kernel/vmbytegen.ml", line 891, characters 9-26: - 891 | let () = Callback.register "rocq_subst_instance" rocq_subst_instance - ^^^^^^^^^^^^^^^^^ - Alert unsafe_multidomain: Stdlib.Callback.register - Use [Callback.Safe.register]. - (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 perf/.coqperf.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]. [ERROR] The compilation of rocq-runtime.9.2.0 failed at "dune build -p rocq-runtime -j 39 --promote-install-files=false @install". build failed... === STDERR === 2026-10-01 23:26.34: FAILED: build rocq-runtime.9.2.0 2026-10-01 23:26.34: Job failed: build failed: rocq-runtime.9.2.0