Adapt to https://github.com/rocq-prover/rocq/pull/21955 - #203
Merged
Conversation
Add the META file to COMPATIBILITY_FILES so it's regenerated from a versioned source like the other plugin files. The unversioned META.coq-rewriter is now generated at build time and gitignored; otherwise the compat copy rule would overwrite a tracked file. Per-version copies (.v816 through .v93) currently have identical content; .v815 is empty, matching the previous behavior where META_FILE_FRAGMENT was unset for 8.15. The @meta@ template logic in the top-level Makefile and _CoqProject.in is no longer needed since COMPATIBILITY_FILES handles the META path.
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.
JasonGross
enabled auto-merge
May 5, 2026 19:16
JasonGross
added a commit
to mit-plv/fiat-crypto
that referenced
this pull request
Jun 13, 2026
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]>
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.
Adapt to rocq-prover/rocq#21955 (removal of the deprecated
coq-core.*library aliases): replacecoq-corewithrocq-runtimeinMETA.coq-rewriterandMakefile.local-late.