Skip to content

Change rocq-prover version from 9.0.0 to meta.1#29190

Merged
mseri merged 1 commit intoocaml:masterfrom
proux01:rocq-prover-meta
Jan 7, 2026
Merged

Change rocq-prover version from 9.0.0 to meta.1#29190
mseri merged 1 commit intoocaml:masterfrom
proux01:rocq-prover-meta

Conversation

@proux01
Copy link
Contributor

@proux01 proux01 commented Jan 6, 2026

Since #28179 the rocq-prover package is a pure metapackage not depending on rocq-core version, this makes the old 9.0.0 version number (no longer updated) confusing, c.f., https://rocq-prover.zulipchat.com/#narrow/channel/237977-Rocq-users/topic/diff.20version.20Rocq.20Core.2C.20and.20Rocq.20Prover/with/561649780
A version number clearly conveying the metapackage status should help.
We have 9.0.0 < meta.1 in the version ordering which should avoid too much trouble.

Since ocaml#28179 the
rocq-prover package is a pure metapackage not depending on rocq-core
version, this makes the old 9.0.0 version number (no longer updated)
confusing, c.f.,
https://rocq-prover.zulipchat.com/#narrow/channel/237977-Rocq-users/topic/diff.20version.20Rocq.20Core.2C.20and.20Rocq.20Prover/with/561649780
A version number clearly conveying the metapackage status should help.
We have 9.0.0 < meta.1 in the version ordering which should avoid too
much trouble.
@proux01
Copy link
Contributor Author

proux01 commented Jan 6, 2026

The linting error is expected since this is a metapackage (no source, only dependencies, by definition).

@mseri mseri merged commit f8556fe into ocaml:master Jan 7, 2026
3 of 4 checks passed
@proux01
Copy link
Contributor Author

proux01 commented Jan 7, 2026

Thanks

@proux01 proux01 deleted the rocq-prover-meta branch January 7, 2026 15:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

Comments