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.

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

[coq] Add dependency to META file for Coq plugins #6167

Merged
merged 2 commits into from
Oct 11, 2022
Merged

[coq] Add dependency to META file for Coq plugins #6167

merged 2 commits into from
Oct 11, 2022

Commits on Oct 11, 2022

  1. [coq] Add dependency to META file for Coq plugins 

    Traditionally, `coqdep` requires the source files of all involved
theories to be present in the filesystem, as to resolve logical paths
to files.

For `.v` files this process is easy, however for plugins, `coqdep`
relies on the presence of a `plugin.mlpack` file as a hint that a
`plugin.cmxs` file will be produced, so it can correctly map `Declare
Ml` to the right `.cmxs`.

Starting with 8.16, `coqdep` can alternatively use `META` files to do
this mapping, but that requires `META` files to be present in the
build tree, at the right path pointed by `OCAMLPATH`.

We thus add the `META` files as a dependency for coqdep, which is
backwards compatible and will allow us to fix Dune to work with the
new findlib-based plugin loading method in Coq 8.16.

Unfortunately, the code in Coq upstream seems pretty broken (it seems
to produce paths that are wrong w.r.t. our `META` files), so this will
need fixing in Coq to fully work, but this is the Dune part, so the
rest of work belongs to Coq upstream IIANM.

The issue upstream is coq/coq#16571

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
    @ejgallego
    ejgallego committed Oct 11, 2022
    Configuration menu
    Copy the full SHA
    bc980a1 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into coq+add_meta_dep_for_plugins

    @ejgallego
    ejgallego authored Oct 11, 2022
    Configuration menu
    Copy the full SHA
    6311044 View commit details
    Browse the repository at this point in the history