Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add -allow-unreleased-menhir #530

Closed
wants to merge 1 commit into from

Conversation

JasonGross
Copy link
Contributor

This will allow https://github.com/coq/opam/tree/master/extra-dev/packages/coq-compcert/coq-compcert.dev to drop the patch that makes ./configure compatible with unreleased / dev versions of menhir.

@xavierleroy
Copy link
Contributor

I must have missed something. Why do we need to support unreleased / dev versions of Menhir? They are unreleased for a reason...

@JasonGross
Copy link
Contributor Author

Hm, I guess I was poking at things I don't understand, sorry.

@MSoegtropIMC added such a patch in coq/opam#1536, saying

The patched to allow unreleased menhir versions should stay permanently in the dev package, since it is not desirable to merge it upstream (a well known menhir version is preferable there).

and

FYI : this is required for the Coq platform master branch

I thought, upon seeing only the code, without looking into its history, it would make sense to add a flag here. (I originally thought it was required for the master version of Coq, but I guess not.)

I guess the reason this is required for Coq Platform is that the dev switch / master version requires that all packages it installs be compatible, and the dev version of coq-menhirlib is otherwise incompatible with CompCert. @MSoegtropIMC is this correct?

@JasonGross JasonGross closed this Oct 22, 2024
@xavierleroy
Copy link
Contributor

No problem! Thank you and @MSoegtropIMC for the clarification.

@MSoegtropIMC
Copy link
Contributor

I guess the reason this is required for Coq Platform is that the dev switch / master version requires that all packages it installs be compatible, and the dev version of coq-menhirlib is otherwise incompatible with CompCert. @MSoegtropIMC is this correct?

Yes. if we build Coq Platform dev all packages are dev packages and CompCert needs to compile with this dev version of menhir. But it is not desirable to have this outside of the dev packages, so I think it could/should stay in the dev opam package forever.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants