From 76a91753e531f4e09941641a08db747ab262bc6f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 30 Mar 2019 19:31:54 +0100 Subject: [PATCH] [coq] Install plugin `.cmxs` files under the coq library root. This is needed for compatibility with Coq < 8.11 otherwise Coq doesn't know how to set correct OCaml `-I` path. We will remove this kludge in the "2.0" version of the plugin. We also perform some refactoring and cleanup of the rules code. Signed-off-by: Emilio Jesus Gallego Arias --- doc/coq.rst | 5 ++--- src/coq_rules.ml | 50 ++++++++++++++++++++++++++++++++---------------- 2 files changed, 35 insertions(+), 20 deletions(-) diff --git a/doc/coq.rst b/doc/coq.rst index 073fb54df21..c7097ed161d 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -42,7 +42,8 @@ The stanza will build all `.v` files on the given directory. The semantics of fi - ``public_name`` will make Dune generate install rules for the `.vo` files; files will be installed in ``lib/coq/user-contrib/``, as customary in the - make-based Coq package eco-system, + make-based Coq package eco-system. For compatibility, we also installs the `.cmxs` + files appearing in `` under the `user-contrib` prefix. - ```` will be passed to ``coqc``, - the path to installed locations of ```` will be passed to ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq @@ -67,5 +68,3 @@ Limitations - composition and scoping of Coq libraries is still not possible. For now, libraries are located using Coq's built-in library management, - .v always depend on the native version of a plugin, - a ``foo.mlpack`` file must the present for locally defined plugins to work, this is a limitation of coqdep, -- Coq plugins are installed into their regular OCaml library path, this means Coq < 8.11 won't properly detect them. - diff --git a/src/coq_rules.ml b/src/coq_rules.ml index 52d370d0ea8..952814c7726 100644 --- a/src/coq_rules.ml +++ b/src/coq_rules.ml @@ -111,6 +111,13 @@ let create_ccoq sctx ~dir = ; coqpp = rr "coqpp" } +(* get_libraries from Coq's ML dependencies *) +let libs_of_coq_deps ~loc ~scope libs = + let lib_db = Scope.libs scope in + List.concat_map ~f:Dune_file.Lib_dep.to_lib_names libs + |> Lib.DB.find_many ~loc lib_db + |> Result.ok_exn + (* compute include flags and mlpack rules *) let setup_ml_deps ~scope ~loc libs = @@ -119,22 +126,16 @@ let setup_ml_deps ~scope ~loc libs = let ml_pack_files lib = let plugins = Mode.Dict.get (Lib.plugins lib) Mode.Native in let to_mlpack file = - Path.([ set_extension file ~ext:".mlpack" - ; set_extension file ~ext:".mllib" - ]) in + [ Path.set_extension file ~ext:".mlpack" + ; Path.set_extension file ~ext:".mllib" + ] in List.concat_map plugins ~f:to_mlpack in (* Pair of include flags and paths to mlpack *) let ml_iflags, mlpack = - let lib_db = Scope.libs scope in - match Lib.DB.find_many ~loc lib_db - (List.concat_map ~f:Dune_file.Lib_dep.to_lib_names libs) with - | Ok libs -> - Util.include_flags libs, List.concat_map ~f:ml_pack_files libs - | Error exn -> - Errors.fail loc "ML dependencies for Coq library %a" - (Exn.pp_uncaught ~backtrace:"") exn + let libs = libs_of_coq_deps ~loc ~scope libs in + Util.include_flags libs, List.concat_map ~f:ml_pack_files libs in (* If the mlpack files don't exist, don't fail *) @@ -173,21 +174,36 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Dune_file.Coq.t) = ~ml_iflags ~mlpack_rule) coq_modules in coq_rules +(* This is here for compatibility with Coq < 8.11, which expects the + plugin's `.cmxs` files to be in the folder containing the `.vo` + files *) +let coq_cmx_install_rules ~dst_dir libs = + let rules_for_lib lib = + Mode.Dict.get (Lib.plugins lib) Mode.Native |> + List.map ~f:(fun plugin_file -> + let dst = Path.(to_string (relative dst_dir (basename plugin_file))) in + None, Install.(Entry.make Section.Lib_root ~dst plugin_file)) + in + List.concat_map ~f:rules_for_lib libs + let install_rules ~sctx ~dir s = match s with | { Dune_file.Coq. public = None; _ } -> [] - | { Dune_file.Coq. public = Some { package = _ ; _ } ; _ } -> + | { Dune_file.Coq. public = Some { package = _ ; _ } ; loc; _ } -> + let scope = SC.find_scope_by_dir sctx dir in let dir_contents = Dir_contents.get_without_rules sctx ~dir in let name = Dune_file.Coq.best_name s in + (* This is the usual root for now, Coq + Dune will change it! *) + let coq_root = Path.of_string "coq/user-contrib" in + (* This must match the wrapper prefix for now to remain compatible *) + let dst_suffix = coqlib_wrapper_name s in + let dst_dir = Path.relative coq_root dst_suffix in + let ml_libs = libs_of_coq_deps ~scope ~loc s.libraries in Dir_contents.coq_modules_of_library dir_contents ~name |> List.map ~f:(fun (vfile : Coq_module.t) -> let vofile = Coq_module.obj_file ~obj_dir:dir ~ext:".vo" vfile in - (* This is the usual root for now, Coq + Dune will change it! *) - let coq_root = "coq/user-contrib" in - (* This must match the wrapper prefix for now to remain compatible *) - let dst_suffix = coqlib_wrapper_name s in - let dst_dir = Path.(relative (of_string coq_root) dst_suffix) in let dst = Coq_module.obj_file ~obj_dir:dst_dir ~ext:".vo" vfile in let dst = Path.to_string dst in None, Install.(Entry.make Section.Lib_root ~dst vofile)) + |> List.rev_append (coq_cmx_install_rules ~dst_dir ml_libs)