Skip to content

rocq-runtime.9.3: require OCaml >= 4.14.0, as upstream does - #3803

Merged
JasonGross merged 1 commit into
rocq-prover:masterfrom
JasonGross:rocq-runtime-93-ocaml
Jul 31, 2026
Merged

rocq-runtime.9.3: require OCaml >= 4.14.0, as upstream does#3803
JasonGross merged 1 commit into
rocq-prover:masterfrom
JasonGross:rocq-runtime-93-ocaml

Conversation

@JasonGross

Copy link
Copy Markdown
Member

rocq-runtime.9.3.dev and rocq-runtime.9.3+rc1 both declare
"ocaml" {>= "4.09.0"}. Rocq 9.3 disagrees with that: its own in-tree
rocq-runtime.opam says >= "4.14.0", and tools/configure/configure.ml
exits with "You need OCaml 4.14.0 or later."

The 9.1, 9.2 and dev recipes here already say 4.14.0; only the two 9.3 ones
were missed. The value they carry is the one the 9.0 recipes use, which suggests
they were copied from that template.

Why this matters beyond tidiness. scripts/opam-coq-install-remove first
asks whether a package is installable on the job's compiler and only builds if
it is. On opam-build:4.09.0 a package depending on rocq-core {>= "9.0"}
therefore splits two ways, as visible in
job 7677268:

  • rocq-elpi.dev fails that check and is correctly tolerated as "not compatible
    with the current compiler"
    ;
  • rocq-micromega-plugin.dev passes it — possible only because
    rocq-runtime.9.3.dev claims 4.09 support — so CI proceeds to a real install
    that then dies:
[ERROR] The compilation of rocq-runtime.9.3.dev failed at
"./configure -release -prefix ... -native-compiler no".

That is what is currently failing opam-build:4.09.0 on unrelated pull requests
(#3789, #3800), neither of which touches anything related.

Scope. Metadata only, two lines. opam lint --warn=-21 passes on both files
under the opam 2.1.2 that .gitlab-ci.yml pins. Note that this makes the
4.09.0 job skip rather than pass the affected packages: with 9.3 correctly
excluded, rocq-core {>= "9.0"} can still be satisfied by rocq-core.9.0.dev
(whose 4.09 support is genuine), so what each package does next on that job is
for CI here to answer.

🤖 Generated with Claude Code

https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b

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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
@JasonGross
JasonGross merged commit c9731cf into rocq-prover:master Jul 31, 2026
3 checks passed
@JasonGross
JasonGross deleted the rocq-runtime-93-ocaml branch July 31, 2026 19:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant