Skip to content

Makefile.menhir: specify menhirLib.cmxa instead of menhirLib.cmx. #330

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.

Sign up for GitHub

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

Jump to bottom
Closed
wants to merge 1 commit into from
Closed

Makefile.menhir: specify menhirLib.cmxa instead of menhirLib.cmx. #330

wants to merge 1 commit into from

Conversation

@fpottier
Copy link
Contributor

@fpottier fpottier commented Jan 27, 2020

This should allow CompCert to compile with Menhir 20200123 and newer.

@bschommer
Copy link
Member

bschommer commented Jan 27, 2020

Indeed that should work, however this is not really backward compatible, since older menhir versions did not install the .cmxa file as far as I know.

@fpottier
Copy link
Contributor Author

fpottier commented Jan 27, 2020

Hi Bernhard, you are correct, older versions of Menhir installed menhirLib.{cmi,cmo,cmx,cmxs,o} whereas the new version installs menhirLib.{a,cma,cmi,cmt,cmti,cmx,cmxa,cmxs}. The old set of files was hardcoded somewhere in our Makefiles, whereas the new set of files is automatically chosen by dune and/or opam.

I suppose you could complicate Makefile.menhir by testing which of menhirLib.cmx and menhirLib.cmxa exists. This would allow to preserve compatibility between a new CompCert and an old Menhir. But it may be simpler to just require a newer Menhir. (Also, the compatibility between an old CompCert and a new Menhir will remain broken, unless you apply the patch retroactively.)

xavierleroy added a commit that referenced this pull request Jan 30, 2020
@xavierleroy
Revised menhirLib autoconfiguration
477f19b 
Since Menhir version 20200123, we need to link with menhirLib.cmxa
instead of menhirLib.cmx.

This commit chooses automatically the file to link with:
menhirLib.cmxa if it exists in the menhirLib installation directory,
menhirLib.cmx otherwise.

To reliably find the installation directory, configure was changed
to record the menhirLib directory in Makefile.config, variable MENHIR_DIR,
instead of a pre-cooked command-line option MENHIR_INCLUDES.

Makefile.extr was adapted accordingly.

Fixes: #329
Closes: #330
@xavierleroy xavierleroy mentioned this pull request Jan 30, 2020
Merged
@xavierleroy
Copy link
Contributor

xavierleroy commented Jan 30, 2020

I suppose you could complicate Makefile.menhir by testing which of menhirLib.cmx and menhirLib.cmxa exists. This would allow to preserve compatibility between a new CompCert and an old Menhir.

See #331 for an implementation of this idea. It might be worth preserving compatibility for a few versions of CompCert.

@xavierleroy
Copy link
Contributor

xavierleroy commented Feb 5, 2020

We went with the more convoluted fix at #331. Thanks for having diagnosed the issue, anyway.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@fpottier @bschommer @xavierleroy