From 0749611bd14033140479952407d24a11b2b8e2fe Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Jul 2026 20:44:22 +0000 Subject: [PATCH] rocq-runtime.9.3: require OCaml >= 4.14.0, as upstream does Both 9.3 recipes declared `"ocaml" {>= "4.09.0"}`, which contradicts Rocq 9.3 itself: its in-tree rocq-runtime.opam says `>= "4.14.0"` and tools/configure/configure.ml dies with "You need OCaml 4.14.0 or later." The 9.1, 9.2 and dev recipes all already say 4.14.0; only these two were missed, and the value they carry matches the 9.0 recipes, which suggests they were copied from that template. The consequence is a hard CI failure rather than a skipped package. scripts/opam-coq-install-remove first asks whether a package is installable on the job's compiler, and only builds if it is. On the 4.09.0 job, a package depending on `rocq-core {>= "9.0"}` therefore splits two ways: rocq-elpi.dev fails that check and is correctly tolerated as "not compatible with the current compiler", while rocq-micromega-plugin.dev passes it -- solely because rocq-runtime.9.3.dev claims to support 4.09 -- so CI proceeds to a real build that then dies: [ERROR] The compilation of rocq-runtime.9.3.dev failed at "./configure -release -prefix ... -native-compiler no". That is currently failing opam-build:4.09.0 on unrelated pull requests. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- core-dev/packages/rocq-runtime/rocq-runtime.9.3+rc1/opam | 2 +- core-dev/packages/rocq-runtime/rocq-runtime.9.3.dev/opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/core-dev/packages/rocq-runtime/rocq-runtime.9.3+rc1/opam b/core-dev/packages/rocq-runtime/rocq-runtime.9.3+rc1/opam index 967a3f471..b056024db 100644 --- a/core-dev/packages/rocq-runtime/rocq-runtime.9.3+rc1/opam +++ b/core-dev/packages/rocq-runtime/rocq-runtime.9.3+rc1/opam @@ -26,7 +26,7 @@ doc: "https://rocq-prover.org/docs" bug-reports: "https://github.com/rocq-prover/rocq/issues" depends: [ "dune" {>= "3.21"} - "ocaml" {>= "4.09.0"} + "ocaml" {>= "4.14.0"} "ocamlfind" {>= "1.8.1"} "zarith" {>= "1.11"} "conf-linux-libc-dev" {os = "linux"} diff --git a/core-dev/packages/rocq-runtime/rocq-runtime.9.3.dev/opam b/core-dev/packages/rocq-runtime/rocq-runtime.9.3.dev/opam index fe62bca4d..c0a2b1a7e 100644 --- a/core-dev/packages/rocq-runtime/rocq-runtime.9.3.dev/opam +++ b/core-dev/packages/rocq-runtime/rocq-runtime.9.3.dev/opam @@ -26,7 +26,7 @@ doc: "https://rocq-prover.org/docs" bug-reports: "https://github.com/rocq-prover/rocq/issues" depends: [ "dune" {>= "3.21"} - "ocaml" {>= "4.09.0"} + "ocaml" {>= "4.14.0"} "ocamlfind" {>= "1.8.1"} "zarith" {>= "1.11"} "conf-linux-libc-dev" {os = "linux"}