Support development Menhir and Rocq 9.3 proof syntax - #590
Draft
JasonGross wants to merge 2 commits into
Draft
Conversation
`menhir --version` prints "menhir, version unreleased" for builds from the
upstream git repository (e.g. an opam pin on gitlab.inria.fr/fpottier/menhir).
The version-extraction sed only matched digits, so the version test fell
through to the catch-all case and reported
Error: make sure Menhir version 20200624 or later is installed.
Recognise "unreleased" and treat it as recent enough, still checking that the
Menhir API library can be located. This is the patch the opam packages
coq-compcert / coq-compcert-32 have been carrying out-of-tree since 2020.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
Rocq 9.3 turned "Proof must be the first command in an interactive proof"
into an error, so the three definitions in MenhirLib/Interpreter.v that open
with `refine`/`unshelve refine` and only then write `Proof.` no longer
compile:
File "./MenhirLib/Interpreter.v", line 194, characters 0-6:
Error: "Proof" must be the first command in an interactive proof.
Move each `Proof.` above its `refine`. This only affects the bundled copy of
MenhirLib, which is what `./configure` uses unless `-use-external-MenhirLib`
is given; the coq-menhirlib opam package already carries the same fix.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
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.
This draft fixes two development-toolchain compatibility issues.
The implementation was produced by a Claude coding-agent session working on Jason Gross's behalf. It:
unreleased, while still verifying that the Menhir API library is available; andProof.commands before theirrefinecommands in the bundled MenhirLib, as required since Rocq 9.3.The Menhir configure change matches the patch that CompCert opam packages have carried out of tree.
I independently validated the unchanged branch against
rocq-dev-testingwith an amd64-linux, 64-bit configuration. Configure recognizes the development Menhir, and the completemake -j4build succeeds, including proofs, extraction, compiler, runtime, andclightgen.Implementation credit: Claude Opus 5; both commits contain Claude session attribution and co-authorship trailers.