From b739d97adcd4c6e7209cdbe210406bbd18d2e4be Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 28 Sep 2022 16:47:47 +0200 Subject: [PATCH] [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. Signed-off-by: Emilio Jesus Gallego Arias --- CHANGES.md | 8 +++- src/dune_rules/coq_rules.ml | 43 ++++++++++++++++--- .../coq/deprecate-libraries.t/bar.opam | 0 .../coq/deprecate-libraries.t/run.t | 30 +++++++------ 4 files changed, 59 insertions(+), 22 deletions(-) create mode 100644 test/blackbox-tests/test-cases/coq/deprecate-libraries.t/bar.opam diff --git a/CHANGES.md b/CHANGES.md index 553f0c069efe..2a74fcf5af0b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -68,7 +68,7 @@ - The test suite for Coq now requires Coq >= 8.16 due to changes in the plugin loading mechanism upstream (which now uses findlib). - + - Starting with Coq build language 0.6, theories can be built without importing Coq's standard library by including `(stdlib no)`. (#6165 #6164, fixes #6163, @ejgallego @Alizter @LasseBlaauwbroek) @@ -76,6 +76,12 @@ - on macOS, sign executables produced by artifact substitution (#6137, fixes #5650, @emillon) +- The `(coq.theory ...)` stanza will now ensure that for each declared + `(plugin ...)`, the `META` file for is built before calling + `coqdep`. This enables to use the new `findlib`-based loading method + in Coq 8.16, however as of Coq 8.16.0, Coq itself has some bugs + preventing this to work yet. (#6167 , workarounds #5767, @ejgallego) + 3.4.1 (26-07-2022) ------------------ diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 29196427149e..2c4e31688085 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -56,8 +56,30 @@ let resolve_program sctx ~loc ~dir prog = ~hint:"opam install coq" module Coq_plugin = struct + let meta_info ~coq_lang_version ~plugin_loc ~context (lib : Lib.t) = + let debug = false in + let name = Lib.name lib |> Lib_name.to_string in + if debug then Format.eprintf "Meta info for %s@\n" name; + match Lib_info.status (Lib.info lib) with + | Public (_, pkg) -> + let package = Package.name pkg in + let meta_i = + Path.Build.relative + (Local_install_path.lib_dir ~context ~package) + "META" + in + if debug then + Format.eprintf "Meta for %s: %s@\n" name (Path.Build.to_string meta_i); + Some (Path.build meta_i) + | Installed -> None + | Installed_private | Private _ -> + let is_error = coq_lang_version >= (0,6) in + User_warning.emit ?loc:plugin_loc ~is_error + [ Pp.textf "Using private library %s as a Coq plugins is deprecated" name ]; + None + (* compute include flags and mlpack rules *) - let setup_ml_deps libs theories = + let setup_ml_deps ~coq_lang_version ~context ~plugin_loc libs theories = (* Pair of include flags and paths to mlpack *) let libs = let open Resolve.Memo.O in @@ -76,10 +98,14 @@ module Coq_plugin = struct ( flags , let* libs = Resolve.Memo.read libs in (* If the mlpack files don't exist, don't fail *) - Action_builder.paths_existing (List.concat_map ~f:Util.ml_pack_files libs) - ) - - let of_buildable ~lib_db ~theories_deps (buildable : Coq_stanza.Buildable.t) = + Action_builder.all_unit + [ Action_builder.paths (List.filter_map ~f:(meta_info ~plugin_loc ~coq_lang_version ~context) libs) + ; Action_builder.paths_existing + (List.concat_map ~f:Util.ml_pack_files libs) + ] ) + + let of_buildable ~context ~lib_db ~theories_deps + (buildable : Coq_stanza.Buildable.t) = let res = let open Resolve.Memo.O in let+ libs = @@ -87,7 +113,9 @@ module Coq_plugin = struct let+ lib = Lib.DB.resolve lib_db (loc, name) in (loc, lib)) in - setup_ml_deps libs theories_deps + let coq_lang_version = buildable.coq_lang_version in + let plugin_loc = List.hd_opt buildable.plugins |> Option.map ~f:fst in + setup_ml_deps ~plugin_loc ~coq_lang_version ~context libs theories_deps in let ml_flags = Resolve.Memo.map res ~f:fst in let mlpack_rule = @@ -290,12 +318,13 @@ module Context = struct let loc = buildable.loc in let use_stdlib = buildable.use_stdlib in let rr = resolve_program sctx ~dir ~loc in + let context = Super_context.context sctx |> Context.name in let* expander = Super_context.expander sctx ~dir in let* scope = Scope.DB.find_by_dir dir in let lib_db = Scope.libs scope in (* ML-level flags for depending libraries *) let ml_flags, mlpack_rule = - Coq_plugin.of_buildable ~theories_deps ~lib_db buildable + Coq_plugin.of_buildable ~context ~theories_deps ~lib_db buildable in let mode = select_native_mode ~sctx ~buildable in let* native_includes = diff --git a/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/bar.opam b/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/bar.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t b/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t index dfd0a43d782a..94a3429b3a22 100644 --- a/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t +++ b/test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t @@ -1,40 +1,42 @@ The libraries field is deprecated $ cat > dune << EOF > (library + > (public_name bar.foo) > (name foo)) > - > (coq.theory + > (coq.theory > (name bar) - > (libraries foo)) + > (libraries bar.foo)) > EOF $ dune build - File "dune", line 6, characters 1-16: - 6 | (libraries foo)) - ^^^^^^^^^^^^^^^ + File "dune", line 7, characters 1-20: + 7 | (libraries bar.foo)) + ^^^^^^^^^^^^^^^^^^^ Warning: 'libraries' was deprecated in version 0.5 of the Coq language. It has been renamed to 'plugins'. Having both a libraries and plugins field is an error $ cat > dune << EOF > (library + > (public_name bar.foo) > (name foo)) > - > (coq.theory + > (coq.theory > (name bar) - > (libraries foo) - > (plugins foo)) + > (libraries bar.foo) + > (plugins bar.foo)) > EOF $ dune build - File "dune", line 6, characters 1-16: - 6 | (libraries foo) - ^^^^^^^^^^^^^^^ + File "dune", line 7, characters 1-20: + 7 | (libraries bar.foo) + ^^^^^^^^^^^^^^^^^^^ Warning: 'libraries' was deprecated in version 0.5 of the Coq language. It has been renamed to 'plugins'. - File "dune", line 6, characters 12-15: - 6 | (libraries foo) - ^^^ + File "dune", line 7, characters 12-19: + 7 | (libraries bar.foo) + ^^^^^^^ Error: Cannot both use 'plugins' and 'libraries', please remove 'libraries' as it has been deprecated since version 0.5 of the Coq language. It will be removed before version 1.0.