From bc980a13ec5eb040e00f539ec5a86b1e8cd47e63 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. The issue upstream is https://github.com/coq/coq/issues/16571 Signed-off-by: Emilio Jesus Gallego Arias --- CHANGES.md | 12 +++-- src/dune_rules/coq_rules.ml | 47 ++++++++++++++++--- .../coq/deprecate-libraries.t/bar.opam | 0 .../coq/deprecate-libraries.t/run.t | 30 ++++++------ .../test-cases/coq/plugin-meta.t/bar.opam | 0 .../test-cases/coq/plugin-meta.t/bar.v | 0 .../test-cases/coq/plugin-meta.t/dune-project | 2 + .../test-cases/coq/plugin-meta.t/foo.ml | 1 + .../test-cases/coq/plugin-meta.t/run.t | 15 ++++++ .../test-cases/coq/plugin-private.t/bar.opam | 0 .../test-cases/coq/plugin-private.t/bar.v | 0 .../coq/plugin-private.t/dune-project | 2 + .../test-cases/coq/plugin-private.t/foo.ml | 1 + .../test-cases/coq/plugin-private.t/run.t | 16 +++++++ 14 files changed, 102 insertions(+), 24 deletions(-) create mode 100644 test/blackbox-tests/test-cases/coq/deprecate-libraries.t/bar.opam create mode 100644 test/blackbox-tests/test-cases/coq/plugin-meta.t/bar.opam create mode 100644 test/blackbox-tests/test-cases/coq/plugin-meta.t/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/plugin-meta.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/plugin-meta.t/foo.ml create mode 100644 test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/plugin-private.t/bar.opam create mode 100644 test/blackbox-tests/test-cases/coq/plugin-private.t/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/plugin-private.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/plugin-private.t/foo.ml create mode 100644 test/blackbox-tests/test-cases/coq/plugin-private.t/run.t diff --git a/CHANGES.md b/CHANGES.md index 72ffb526be5..0dbafeceb3d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -71,8 +71,8 @@ #6169, @shonfeder) - The test suite for Coq now requires Coq >= 8.16 due to changes in the - plugin loading mechanism upstream (which now uses findlib). - + 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) @@ -81,7 +81,13 @@ #5650, @emillon) - Added an (aliases ...) field to the (rules ...) stanza which allows the - specification of multiple aliases per rule (#6194, @Alizter) + specification of multiple aliases per rule (#6194, @Alizter) + +- The `(coq.theory ...)` stanza will now ensure that for each declared `(plugin + ...)`, the `META` file for it is built before calling `coqdep`. This enables + the use of 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 f725a541422..68c3421407a 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -55,8 +55,31 @@ let resolve_program sctx ~loc ~dir ?(hint = "opam install coq") prog = Super_context.resolve_program ~dir sctx prog ~loc:(Some loc) ~hint 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 + let text = if is_error then "not supported" else "deprecated" in + User_warning.emit ?loc:plugin_loc ~is_error + [ Pp.textf "Using private library %s as a Coq plugin is %s" name text ]; + 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 @@ -75,10 +98,17 @@ 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 = @@ -86,7 +116,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 = @@ -289,12 +321,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 00000000000..e69de29bb2d 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 dfd0a43d782..94a3429b3a2 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. diff --git a/test/blackbox-tests/test-cases/coq/plugin-meta.t/bar.opam b/test/blackbox-tests/test-cases/coq/plugin-meta.t/bar.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/plugin-meta.t/bar.v b/test/blackbox-tests/test-cases/coq/plugin-meta.t/bar.v new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/plugin-meta.t/dune-project b/test/blackbox-tests/test-cases/coq/plugin-meta.t/dune-project new file mode 100644 index 00000000000..4dad2a1c9b9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/plugin-meta.t/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.5) +(using coq 0.6) diff --git a/test/blackbox-tests/test-cases/coq/plugin-meta.t/foo.ml b/test/blackbox-tests/test-cases/coq/plugin-meta.t/foo.ml new file mode 100644 index 00000000000..4b3fcfa724c --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/plugin-meta.t/foo.ml @@ -0,0 +1 @@ +let foo = "bar" diff --git a/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t b/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t new file mode 100644 index 00000000000..20097849b12 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t @@ -0,0 +1,15 @@ +The META file for plugins is built before calling coqdep + $ cat > dune << EOF + > (library + > (public_name bar.foo) + > (name foo)) + > + > (coq.theory + > (name bar) + > (plugins bar.foo)) + > EOF + + $ dune build bar.v.d + $ ls _build/install/default/lib/bar + META + diff --git a/test/blackbox-tests/test-cases/coq/plugin-private.t/bar.opam b/test/blackbox-tests/test-cases/coq/plugin-private.t/bar.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/plugin-private.t/bar.v b/test/blackbox-tests/test-cases/coq/plugin-private.t/bar.v new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/plugin-private.t/dune-project b/test/blackbox-tests/test-cases/coq/plugin-private.t/dune-project new file mode 100644 index 00000000000..4dad2a1c9b9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/plugin-private.t/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.5) +(using coq 0.6) diff --git a/test/blackbox-tests/test-cases/coq/plugin-private.t/foo.ml b/test/blackbox-tests/test-cases/coq/plugin-private.t/foo.ml new file mode 100644 index 00000000000..4b3fcfa724c --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/plugin-private.t/foo.ml @@ -0,0 +1 @@ +let foo = "bar" diff --git a/test/blackbox-tests/test-cases/coq/plugin-private.t/run.t b/test/blackbox-tests/test-cases/coq/plugin-private.t/run.t new file mode 100644 index 00000000000..81dac547d5f --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/plugin-private.t/run.t @@ -0,0 +1,16 @@ +In Coq >= 0.6, depending on a private library as a plugin is an error. + $ cat > dune << EOF + > (library + > (name foo)) + > + > (coq.theory + > (name bar) + > (plugins foo)) + > EOF + + $ dune build + File "dune", line 6, characters 10-13: + 6 | (plugins foo)) + ^^^ + Error: Using private library foo as a Coq plugin is not supported + [1]