Remove compat coq-core libraries (not executables) by SkySkimmer · Pull Request #21955 · rocq-prover/rocq

SkySkimmer · 2026-04-24T11:54:59Z

Overlays:

SkySkimmer · 2026-04-28T11:12:31Z

dune coq mode needs coq-core.kernel so let's keep that one until we drop coq-core as a whole.

SkySkimmer · 2026-04-29T16:11:36Z

@JasonGross can you figure out how to port fiat-parsers? The compat infrastructure is confusing me. (without compat you just need to replace coq-core -> rocq-runtime in META.coq-fiat-parsers)
also rewriter (needs to modify the META and also Makefile.local-late)

SkySkimmer · 2026-04-30T10:52:42Z

elpi_hb failure is spurious (parallel merge with elpi 3.7)

SkySkimmer · 2026-05-05T12:55:44Z

ping @JasonGross

JasonGross · 2026-05-05T18:49:56Z

Sorry, will aim to take a look at this shortly.

Make META.coq-fiat-parsers version-controlled, with a v93 variant that uses rocq-runtime instead of coq-core, since rocq/pull/21955 removes the coq-core compat libraries. Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Use rocq-runtime instead of coq-core in META.coq-fiat-parsers.v93, since rocq/pull/21955 removes the coq-core compat libraries. Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

The deprecated coq-core.* library aliases are removed; switch the v93 META and the Makefile.local-late ltac2 -package kludge to rocq-runtime. Older versions still pin coq-core.

Adapt to rocq-prover/rocq#21955

* Add v93 files ```bash ( export v=2; export nv=$(( v+1 )); for i in $(git ls-files "*\.v9${v}"); do cp "$i" "${i/v9${v}/v9${nv}}"; git add "${i/v9${v}/v9${nv}}"; done ) ``` Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]> * Make META.coq-fiat-parsers version-controlled Add a META.coq-fiat-parsers.v<XX> variant for every supported Coq version (each currently identical to the prior unversioned file), wire META into ML_COMPATIBILITY_FILES so the per-version variant is copied to META.coq-fiat-parsers at build time, and gitignore the unversioned file so it is no longer overwritten in-tree. Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]> * Adapt to rocq-prover/rocq#21955 Use rocq-runtime instead of coq-core in META.coq-fiat-parsers.v93, since rocq/pull/21955 removes the coq-core compat libraries. Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]> --------- Co-authored-by: Claude Opus 4.7 (1M context) <[email protected]>

SkySkimmer · 2026-05-21T13:37:15Z

@coqbot run full ci

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

Not sure if safechecker actually needs ltac or if rocq-runtime.vernac would be enough but doesn't need to be figured out in this PR.

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

SkySkimmer · 2026-05-28T11:38:26Z

@coqbot run full ci

ppedrot · 2026-05-28T20:13:19Z

@coqbot merge now

coqbot-app · 2026-05-28T20:13:22Z

@ppedrot: You can't merge the PR because it hasn't been approved yet.

ppedrot · 2026-05-28T20:13:50Z

@coqbot merge now

coqbot-app · 2026-05-28T20:13:58Z

@ppedrot: Please take care of the following overlays:

21955-SkySkimmer-rm-core.sh

rocq-prover/rocq#21955 (in the dev builds of Rocq 9.3) removed the coq-core.* findlib compatibility aliases, so the static `requires = "coq-core.plugins.ltac"` lines in META.coq-rewriter now fail on rocq dev with: findlib error: coq-core.plugins.ltac not found ... required by `coq-rewriter.rewriter_build' The real findlib package has been rocq-runtime.plugins.ltac since Rocq 9.0, but Coq 8.x only has coq-core.plugins.ltac, so the META file is now generated from META.coq-rewriter.in by substituting @ROCQ_RUNTIME_PACKAGE@ with coq-core on 8.x and rocq-runtime on 9.x, following the same sed-template pattern as _CoqProject.in. The generation rule lives in the top-level Makefile (not Makefile.local-late) because the META file is referenced from _CoqProject and hence must exist before coq_makefile runs; Makefile.coq now depends on it, and the .d files depend on it so it is regenerated before coqdep needs it (and re-made when the Coq version changes, since it depends on the .coq-version file). Also use $(ROCQ_RUNTIME_PACKAGE) for the FINDLIBPKGS ltac2 kludge, and query the rocq-runtime packages in describe-system-config.sh. This unbreaks the docker-master / dev CI builds of rewriter and of fiat-crypto (via its rewriter submodule). https://claude.ai/code/session_01PjCbMk9zjAZWvZHuznFXqh

…206) The diagnostic script only queried coq-core.* findlib packages. Since Rocq 9.0 the plugins live under rocq-runtime.* (coq-core.* were compat aliases, removed in rocq-prover/rocq#21955), so on Rocq 9.x the coq-core queries now report "not found" while the real rocq-runtime packages go unreported. Query both so the system-config log is useful for diagnosing findlib resolution failures (such as the coq-core.plugins.ltac-not-found error) on both Coq 8.x and Rocq 9.x. https://claude.ai/code/session_01PjCbMk9zjAZWvZHuznFXqh Co-authored-by: Claude <[email protected]>

Pulls in mit-plv/rewriter's adaptation to the removal of the deprecated coq-core.* findlib library aliases (rocq-prover/rocq#21955), merged as mit-plv/rewriter#203. Without this, the dev (rocq dev / 9.3) docker CI builds fail while compiling the rewriter submodule with: *** Error: In file src/Rewriter/Util/plugins/RewriterBuild.v findlib error: coq-core.plugins.ltac not found ... required by `coq-rewriter.rewriter_build' because the rewriter META still required coq-core.plugins.* which no longer exists on rocq 9.3. The bumped rewriter generates the META per Coq version (coq-core.* on 8.x/9.0-9.2, rocq-runtime.* on 9.3). https://claude.ai/code/session_01PjCbMk9zjAZWvZHuznFXqh Co-authored-by: Claude <[email protected]>

SkySkimmer requested a review from a team as a code owner April 24, 2026 11:54

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 24, 2026

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 24, 2026

SkySkimmer added this to the 9.3+rc1 milestone Apr 24, 2026

ppedrot added the needs: overlay This is breaking external developments we track in CI. label Apr 26, 2026

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 28, 2026

SkySkimmer force-pushed the rm-core branch from 7496561 to bdaf6bc Compare April 28, 2026 11:12

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 28, 2026

cubic-dev-ai Bot mentioned this pull request Apr 29, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries) lukaszcz/coqhammer#215

Merged

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2026

SkySkimmer force-pushed the rm-core branch from bdaf6bc to 3f0ac81 Compare April 29, 2026 16:12

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2026

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2026

SkySkimmer force-pushed the rm-core branch from 3f0ac81 to b940770 Compare April 29, 2026 16:13

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2026

Lysxia pushed a commit to Lysxia/rocq-simple-io that referenced this pull request Apr 29, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

d035c0a

This was referenced May 5, 2026

Adapt to https://github.com/rocq-prover/rocq/pull/21955 mit-plv/rewriter#203

Merged

Adapt to rocq-prover/rocq#21955 mit-plv/fiat#133

Merged

JasonGross added a commit to mit-plv/rewriter that referenced this pull request May 6, 2026

Merge pull request #203 from JasonGross/rocq21955

16ae768

Adapt to rocq-prover/rocq#21955

SkySkimmer added a commit to rocq-community/stalmarck that referenced this pull request May 22, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

3005e3a

lukaszcz pushed a commit to lukaszcz/coqhammer that referenced this pull request May 22, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries) (#215)

6585b00

ckeller pushed a commit to smtcoq/smtcoq that referenced this pull request May 22, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries) (#167)

e7e54ca

Janno added a commit to Mtac2/Mtac2 that referenced this pull request May 22, 2026

Merge pull request #433 from SkySkimmer/rm-core

3ac607b

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

SkySkimmer added kind: cleanup Code removal, deprecation, refactorings, etc. and removed needs: overlay This is breaking external developments we track in CI. labels May 22, 2026

Lysxia pushed a commit to QuickChick/QuickChick that referenced this pull request May 22, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core compat libraries)

801cb4e

ppedrot pushed a commit to MetaRocq/metarocq that referenced this pull request May 26, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries).

7896673

Not sure if safechecker actually needs ltac or if rocq-runtime.vernac would be enough but doesn't need to be figured out in this PR.

ppedrot added a commit to MetaRocq/metarocq that referenced this pull request May 26, 2026

Merge pull request #1266 from SkySkimmer/rm-core

ba150ba

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

ppedrot pushed a commit to uds-psl/autosubst-ocaml that referenced this pull request May 26, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

b9000f7

ppedrot added a commit to uds-psl/autosubst-ocaml that referenced this pull request May 26, 2026

Merge pull request #35 from SkySkimmer/rm-core

6f34893

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

JasonGross pushed a commit to rocq-community/coq-performance-tests that referenced this pull request May 26, 2026

Adapt to rocq-prover/rocq#21955 (rm coq-core libraries) (#58)

87eab82

ppedrot self-assigned this May 28, 2026

ppedrot approved these changes May 28, 2026

View reviewed changes

coqbot-app Bot merged commit 606d39a into rocq-prover:master May 28, 2026
9 checks passed

SkySkimmer deleted the rm-core branch May 29, 2026 07:58

JasonGross mentioned this pull request Jun 13, 2026

Bump rewriter from 7fc7ef5 to 16ae768 mit-plv/fiat-crypto#2341

Merged

proux01 mentioned this pull request Jun 15, 2026

Bump rupicola from d1336d2 to 5e4f56e mit-plv/fiat-crypto#2340

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Remove compat coq-core libraries (not executables) - #21955

Remove compat coq-core libraries (not executables)#21955
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
SkySkimmer:rm-core

SkySkimmer commented Apr 24, 2026 •

edited

Loading

Uh oh!

SkySkimmer commented Apr 28, 2026

Uh oh!

SkySkimmer commented Apr 29, 2026

Uh oh!

SkySkimmer commented Apr 30, 2026

Uh oh!

SkySkimmer commented May 5, 2026

Uh oh!

JasonGross commented May 5, 2026

Uh oh!

SkySkimmer commented May 21, 2026

Uh oh!

SkySkimmer commented May 28, 2026

Uh oh!

ppedrot commented May 28, 2026

Uh oh!

coqbot-app Bot commented May 28, 2026

Uh oh!

ppedrot commented May 28, 2026

Uh oh!

Uh oh!

coqbot-app Bot commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

SkySkimmer commented Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SkySkimmer commented Apr 28, 2026

Uh oh!

SkySkimmer commented Apr 29, 2026

Uh oh!

SkySkimmer commented Apr 30, 2026

Uh oh!

SkySkimmer commented May 5, 2026

Uh oh!

JasonGross commented May 5, 2026

Uh oh!

SkySkimmer commented May 21, 2026

Uh oh!

SkySkimmer commented May 28, 2026

Uh oh!

ppedrot commented May 28, 2026

Uh oh!

coqbot-app Bot commented May 28, 2026

Uh oh!

ppedrot commented May 28, 2026

Uh oh!

Uh oh!

coqbot-app Bot commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

SkySkimmer commented Apr 24, 2026 •

edited

Loading