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

Coq < 8.10 does not compile with ocaml 4.08.0, probably due to change in dynlink #8868

Open
garrigue opened this issue Aug 11, 2019 · 6 comments

Comments

@garrigue
Copy link
Contributor

commented Aug 11, 2019

Coq 8.9.1, and apparently previous versions too, do not compile with ocaml 4.08.0.
They fail with errors of the form:

- CAMLP5O   plugins/ssrmatching/g_ssrmatching.ml4
- Error while loading “/Users/garrigue/.opam/4.08.0/lib/camlp5/pr_dump.cmo”: The module `Pr_dump’ is already loaded (either by the main program or a previously-dynlinked library).

Apparently, the coq Makefile.build wrongly asks camlp5o to load pr_dump.cmo, while it is already included.
However, until 4.07.1 this worked, so I suppose the behavior was more laxist.
I proposed PRs for Coq (coq/coq#10650) and opam (ocaml/opam-repository#14668), but the problem is extensive, so a fix in ocaml might be simpler.
The problem was only discovered late because coq was waiting for the porting of camlp5, which happened just before 4.08.1.

@nojb

This comment has been minimized.

Copy link
Contributor

commented Aug 11, 2019

This is probably due to #1063

@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Aug 11, 2019

Indeed, it looks like the coq team didn't follow this discussion...

@ejgallego

This comment has been minimized.

Copy link

commented Aug 11, 2019

Indeed, it looks like the coq team didn't follow this discussion...

Yes we did [as you can see in the thread], however we removed the dependency on camlp5 before testing that version of OCaml so we never found that issue.

@gasche

This comment has been minimized.

Copy link
Member

commented Aug 11, 2019

I'm not convinced that we need a "fix" in the compiler.

This is a build-system bug and your fix is quite simple -- a one-liner.

The Coq development team is free to decide whether this is a big deal for them, and release new patch-level releases of their older Coq versions, or just to backport your fix in their older release branches (so that enthusiasts can build from the release branch if they want to try an older Coq version with a newer OCaml version). Or maybe this can be just a patch in the opam-repository as you suggest, but my understanding is that opam-repo people are trying to shift away from patches and prompt new upstream releases in these situations.

@gasche

This comment has been minimized.

Copy link
Member

commented Aug 11, 2019

To expand on Emilio's comment: in #1063 (comment) it is clear that Maxime found this exact issue (double module loading in camlp5) in April 2017, and decided that it was fine to fix it on the Coq side.

@ejgallego

This comment has been minimized.

Copy link

commented Aug 11, 2019

Indeed I don't think this is a bug in OCaml at all, IMHO camlp5 should be patched so it retains cmdline compatibility. No point on patching old Coq versions IMO.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
4 participants
You can’t perform that action at this time.