Add rocq-sail-stdpp.dev - #3800
Merged
Merged
Conversation
Tracks the `main` branch of rems-project/coq-sail, which is the default branch of that repository. The file is upstream's own dune-generated `rocq-sail-stdpp.opam` with exactly two lines dropped (dune's "this file is generated" header and `version: "0.20.2"`) and a `url` block appended. No constraint is relaxed: upstream's in-tree opam file carries no upper bounds, and the `< "9.3~"` / `< "1.14.0~"` caps on the released versions in this archive were added here at publish time rather than coming from upstream. Verified with `dune build -p rocq-sail-stdpp -j 8 @install` on a switch tracking Rocq master (9.4+alpha), which exits 0 with only deprecation warnings. `opam lint` passes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
Removed conflict with 'sail' version in opam file.
JasonGross
force-pushed
the
rocq-sail-stdpp-dev
branch
from
July 31, 2026 19:22
ffbee05 to
eb47d19
Compare
The extra-dev recipe tracks coq-sail's git main and is meant to be built
against the development prover, but it inherited `rocq-core {>= "9.0"}`
from upstream's dune-project via generate_opam_files.
On the opam-build:4.09.0 job that bound is satisfiable in a way it is not
on the other compilers: rocq-runtime.9.0.dev allows ocaml >= 4.09.0 while
9.2.dev/9.3.dev/dev all require >= 4.14.0, so 4.09.0 is the only job that
can select rocq-core.9.0.dev. The solver then paired it with
rocq-stdlib.dev, which fails to compile at ./Logic/EqdepFacts.v line 144.
The 4.14.2 and 5.3.0 jobs already resolve to rocq-core.dev, so this only
pins down what those jobs do anyway; 4.09.0 becomes "not installable with
the current compiler" and is skipped, as it is for other dev-only
packages. `rocq-core {= "dev"}` is the prevailing idiom for extra-dev
recipes (coq-dpdgraph, rocq-bignums, coq-hott, rocq-metarocq-utils,
rocq-lean-import, vsrocq-language-server).
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
JasonGross
added a commit
that referenced
this pull request
Jul 31, 2026
`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.
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds
rocq-sail-stdpp.dev, tracking themainbranch ofrems-project/coq-sail (
mainis thatrepository's default branch).
Provenance. The recipe is upstream's own dune-generated
rocq-sail-stdpp.opamwith exactly two lines dropped — dune's "this file is generated" header and
version: "0.20.2"— and aurlblock appended. Nothing else was edited.No constraints were relaxed. Upstream's in-tree opam file carries no upper
bounds at all; the
< "9.3~"and< "1.14.0~"caps that the released versions inthis archive have were added here at publish time rather than coming from
upstream. So
rocq-core {>= "9.0"}androcq-stdpp-bitvector {>= "1.13.0"}areupstream's own bounds, unmodified. (Worth noting for the second one: opam orders
"1.13.0" < "dev", so a< "1.14.0~"cap would have excluded thedev.2026-…versions thatrocq-stdpp-bitvectorpublishes in theiris-devrepository.)
Verification.
dune build -p rocq-sail-stdpp -j 8 @installagainst a switchtracking Rocq master (9.4+alpha) exits 0, with only deprecation warnings
(
implicit-create-rewrite-hint-dbandnon-boolean-if, insrc-stdpp/State_lemmas.vand
src-stdpp/Hoare.v).opam lintpasses under the opam 2.1.2 that.gitlab-ci.ymlpins. I did not exercise theopam installpath locally, so CIhere is the first test of that.
One thing worth a maintainer's eye:
conflicts: ["sail" {!= version}]isinherited verbatim from upstream. Since no
sail.devexists in opam-repository,on a
.devpackage this reads as "cannot be co-installed with any releasedsail". I kept it to stay faithful to upstream, and there is precedent for thepattern in
extra-dev(menhirLib.dev,menhirCST.dev,menhirGLR.dev,menhirSdk.dev,coq-hammer-tactics.dev,rocq-mathcomp-finmap.dev,rocq-mathcomp-bigenough.dev), but I am happy to drop or loosen it if you wouldrather the dev package not carry it.
🤖 Generated with Claude Code
https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
CI note. Rebased onto master. Two successive
opam-build:4.09.0failures here were both archive-side metadata problems in this package's dependency closure, not inrocq-sail-stdpp.devitself:rocq-runtime.9.3.devclaimed to support OCaml 4.09 while its own configure requires 4.14 — fixed in master by rocq-runtime.9.3: require OCaml >= 4.14.0, as upstream does #3803.rocq-core.9.0.dev(the only rocq-runtime left that allows 4.09) and then built stdlib master against a 9.0 parser, dying atLogic/EqdepFacts.v:144: Syntax error: illegal begin of vernac. Fixed by rocq-stdlib.dev: require rocq-core >= 9.2, as upstream does #3808, which givesrocq-stdlib.devtherocq-core >= 9.2bound upstream already declares.With #3808 in, no rocq-core is installable on 4.09, so this package is correctly skipped there rather than mis-built.