Skip to content

rocq-stdlib.dev: require rocq-core >= 9.2, as upstream does - #3808

Merged
JasonGross merged 1 commit into
rocq-prover:masterfrom
JasonGross:rocq-stdlib-dev-core-bound
Jul 31, 2026
Merged

rocq-stdlib.dev: require rocq-core >= 9.2, as upstream does#3808
JasonGross merged 1 commit into
rocq-prover:masterfrom
JasonGross:rocq-stdlib-dev-core-bound

Conversation

@JasonGross

Copy link
Copy Markdown
Member

rocq-stdlib.dev tracks coq/stdlib#master, whose own in-tree
rocq-stdlib.opam declares "rocq-core" {>= "9.2"}. The recipe here still
said {>= "9.0" | = "dev"}, which admits rocq-core.9.0.dev.

That is not hypothetical. rocq-runtime.9.0.dev is the only rocq-runtime that
still allows OCaml 4.09, so on the opam-build:4.09.0 job the solver picks

  • install rocq-runtime 9.0.dev [required by rocq-core]
  • install rocq-core 9.0.dev [required by rocq-sail-stdpp]
  • install rocq-stdlib dev [required by rocq-stdpp]

and the build then dies compiling master's stdlib against a 9.0 parser:

ROCQ compile ./Logic/EqdepFacts.v
File "./Logic/EqdepFacts.v", line 144, characters 0-12:
Error: Syntax error: illegal begin of vernac

With this bound, no rocq-core is installable on 4.09 (9.1.dev and later all
require OCaml >= 4.14), so packages in this closure are correctly reported as
"not compatible with the current compiler" and skipped rather than mis-built.
That is currently failing opam-build:4.09.0 on #3800.

I kept the | = "dev" disjunct that was already there rather than writing bare
{>= "9.2"} as upstream does; opam orders dev above numeric versions, so the
two are equivalent, but the explicit form matches the surrounding recipes.

The stricter alternative would be "rocq-core" {= version}, which is what
rocq-core.dev, coq-core.dev and coq-stdlib.dev use for their own core
dependencies. I did not do that here because rocq-stdlib.dev is the only
stdlib available to rocq-core.9.3.dev (released has only rocq-stdlib.9.2.0),
so pinning it to rocq-core.dev would make that combination unsatisfiable.
Happy to switch if you would rather have the tighter constraint.

opam lint passes under the opam 2.1.2 that .gitlab-ci.yml pins.
🤖 Generated with Claude Code

https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b

`rocq-stdlib.dev` tracks coq/stdlib#master, whose own in-tree
`rocq-stdlib.opam` declares `"rocq-core" {>= "9.2"}`.  The recipe here still
said `{>= "9.0" | = "dev"}`, which admits `rocq-core.9.0.dev`.

That is not hypothetical.  `rocq-runtime.9.0.dev` is the only rocq-runtime that
still allows OCaml 4.09, so on the `opam-build:4.09.0` job the solver picks

  - install rocq-runtime 9.0.dev [required by rocq-core]
  - install rocq-core    9.0.dev [required by rocq-sail-stdpp]
  - install rocq-stdlib  dev     [required by rocq-stdpp]

and the build then dies compiling master's stdlib against a 9.0 parser:

  ROCQ compile ./Logic/EqdepFacts.v
  File "./Logic/EqdepFacts.v", line 144, characters 0-12:
  Error: Syntax error: illegal begin of vernac

With this bound, no rocq-core is installable on 4.09 (9.1.dev and later all
require OCaml >= 4.14), so packages in this closure are correctly reported as
"not compatible with the current compiler" and skipped rather than mis-built.
That is currently failing opam-build:4.09.0 on rocq-prover#3800.

I kept the `| = "dev"` disjunct that was already there rather than writing bare
`{>= "9.2"}` as upstream does; opam orders `dev` above numeric versions, so the
two are equivalent, but the explicit form matches the surrounding recipes.

The stricter alternative would be `"rocq-core" {= version}`, which is what
rocq-core.dev, coq-core.dev and coq-stdlib.dev use for their own core
dependencies.  I did not do that here because `rocq-stdlib.dev` is the only
stdlib available to `rocq-core.9.3.dev` (released has only rocq-stdlib.9.2.0),
so pinning it to `rocq-core.dev` would make that combination unsatisfiable.
Happy to switch if you would rather have the tighter constraint.

`opam lint` passes under the opam 2.1.2 that .gitlab-ci.yml pins.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
@JasonGross
JasonGross merged commit c3720b6 into rocq-prover:master Jul 31, 2026
3 checks passed
@JasonGross
JasonGross deleted the rocq-stdlib-dev-core-bound branch July 31, 2026 20:59
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