From 14f44ff6c6322e9844d76cb46d49ce54aee10450 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. --- CHANGES.md | 5 +++ src/dune_rules/coq_rules.ml | 40 +++++++++++++++---- .../coq/deprecate-libraries.t/bar.opam | 0 .../coq/deprecate-libraries.t/run.t | 30 +++++++------- 4 files changed, 54 insertions(+), 21 deletions(-) create mode 100644 test/blackbox-tests/test-cases/coq/deprecate-libraries.t/bar.opam diff --git a/CHANGES.md b/CHANGES.md index 2e6b0ace7d0a..89fffc2e9a15 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -61,6 +61,11 @@ - update vendored copy of cmdliner to 1.1.1. This improves the built-in documentation for command groups such as `dune ocaml`. (#6038, @emillon) +- `(coq.theory ...)` will now depend on the `META` files for declared + `(plugin ...)`, so `coqdep` can see them. This enables to use the + new `findlib`-based loading method implemented in 8.16 (as of 8.16.0 + tho Coq itself has some bugs preventing this to work) + 3.4.1 (26-07-2022) ------------------ diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index a48f825c96a3..2b479ead66fd 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -56,8 +56,29 @@ let resolve_program sctx ~loc ~dir prog = ~hint:"opam install coq" module Coq_plugin = struct + let meta_info ~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 _ -> + (* XXX: Do a warning here? Or maybe guard on the Dune lang version ? *) + User_error.raise + [ Pp.textf "can't depend on private libraries as Coq plugins %s" name ] + (* compute include flags and mlpack rules *) - let setup_ml_deps libs theories = + let setup_ml_deps ~context libs theories = (* Pair of include flags and paths to mlpack *) let libs = let open Resolve.Memo.O in @@ -76,10 +97,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 ~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 +112,7 @@ module Coq_plugin = struct let+ lib = Lib.DB.resolve lib_db (loc, name) in (loc, lib)) in - setup_ml_deps libs theories_deps + setup_ml_deps ~context libs theories_deps in let ml_flags = Resolve.Memo.map res ~f:fst in let mlpack_rule = @@ -290,12 +315,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.