Skip to content

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

@garrigue

Description

@garrigue

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 (rocq-prover/rocq#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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions