From 749dcebf4e5633daeea328aad012d1267fcc9f52 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 3 Sep 2020 18:28:44 +0200 Subject: [PATCH 1/8] [stanza] Bump dune lang to 2.8 in preparation for coq lang 0.3 Signed-off-by: Emilio Jesus Gallego Arias --- doc/dune-files.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/dune-files.rst b/doc/dune-files.rst index d0d113bf3d2..c5f95cd1fba 100644 --- a/doc/dune-files.rst +++ b/doc/dune-files.rst @@ -1899,9 +1899,9 @@ a typical ``dune-workspace`` file looks like: .. code:: scheme (lang dune 2.8) - (context (opam (switch 4.02.3))) - (context (opam (switch 4.03.0))) - (context (opam (switch 4.04.0))) + (context (opam (switch 4.07.1))) + (context (opam (switch 4.08.1))) + (context (opam (switch 4.11.1))) The rest of this section describe the stanzas available. From d1679c6a94d89708c0f2e7012164bd056d76792d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Nov 2020 02:14:10 +0100 Subject: [PATCH 2/8] [coq] [ci] Add lower bound on the Coq version to test. This is so the native tests run, not worth to introduce conditional logic in the test suite for this. Signed-off-by: Emilio Jesus Gallego Arias --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b130a996c47..ad47ac51a68 100644 --- a/Makefile +++ b/Makefile @@ -11,7 +11,7 @@ BIN := ./dune.exe TEST_DEPS := \ bisect_ppx \ cinaps \ -coq \ +"coq>=8.12.1" \ core_bench \ "csexp>=1.3.0" \ js_of_ocaml \ From d3a39b42af3b209e551bd446bc34731c2497fac2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 31 Mar 2019 21:58:25 +0200 Subject: [PATCH 3/8] [coq] Add support for native-mode compilation. We add a `(mode ...)` field to the `(coq.theory ...)` stanza that when set to `native` will have the Coq compiler to generate and install "native" objects, that is to say, `.cmxs` libraries containing an ML-level version of the corresponding Coq module. As of today, Coq itself does call the `ocamlfind ocaml` to compile the object files, this restriction may be lifted in the future however it is not easy as tactics do have access to "Just-In-Time" native compilation too. The patch itself should have been straightforward except for a big problem due to the way Coq outputs native targets and the limitations of Dune. By default, `coqc -native-compute on` will generate the OCaml-level objects files under `.coq-native/`, and the regular `.vo` object in the build dir. This scheme doesn't work well with the restriction than a rule can only produce targets in the same directory. To workaround this limitation, we pass a special flag to Coq so `.coq-native` is dropped from the output path; at install time we do set the rules up so indeed the objects will be installed under `.coq-native` for compatibility. This means this feature will only work in Coq >= 8.12.1 Moreover, the non-standard location of native objects defeats Coq's default native include path, so we must pass the additional non-standard include paths to `coqc`. Note that native compilation is disabled by default in the `dev` profile, as to speed up build. Please use the release or a custom profile if you want to avoid this. Signed-off-by: Emilio Jesus Gallego Arias --- src/dune_rules/coq_lib.ml | 1 + src/dune_rules/coq_lib_name.mli | 1 + src/dune_rules/coq_mode.ml | 10 ++ src/dune_rules/coq_mode.mli | 10 ++ src/dune_rules/coq_module.ml | 56 +++++--- src/dune_rules/coq_module.mli | 24 +++- src/dune_rules/coq_rules.ml | 127 ++++++++++++++---- src/dune_rules/coq_rules.mli | 1 + src/dune_rules/coq_sources.ml | 22 ++- src/dune_rules/coq_sources.mli | 2 + src/dune_rules/coq_stanza.ml | 12 +- src/dune_rules/coq_stanza.mli | 1 + src/dune_rules/profile.mli | 2 +- .../test-cases/coq/github3624.t/run.t | 2 +- .../test-cases/coq/native-compose.t/bar/bar.v | 3 + .../test-cases/coq/native-compose.t/bar/dune | 7 + .../test-cases/coq/native-compose.t/base.opam | 0 .../test-cases/coq/native-compose.t/dune | 3 + .../coq/native-compose.t/dune-project | 3 + .../test-cases/coq/native-compose.t/foo/dune | 6 + .../test-cases/coq/native-compose.t/foo/foo.v | 1 + .../test-cases/coq/native-compose.t/run.t | 22 +++ .../test-cases/coq/native-single.t/bar.v | 3 + .../test-cases/coq/native-single.t/base.opam | 0 .../test-cases/coq/native-single.t/dune | 10 ++ .../coq/native-single.t/dune-project | 3 + .../test-cases/coq/native-single.t/foo.v | 1 + .../test-cases/coq/native-single.t/run.t | 22 +++ 28 files changed, 299 insertions(+), 56 deletions(-) create mode 100644 src/dune_rules/coq_mode.ml create mode 100644 src/dune_rules/coq_mode.mli create mode 100644 test/blackbox-tests/test-cases/coq/native-compose.t/bar/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/native-compose.t/bar/dune create mode 100644 test/blackbox-tests/test-cases/coq/native-compose.t/base.opam create mode 100644 test/blackbox-tests/test-cases/coq/native-compose.t/dune create mode 100644 test/blackbox-tests/test-cases/coq/native-compose.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/native-compose.t/foo/dune create mode 100644 test/blackbox-tests/test-cases/coq/native-compose.t/foo/foo.v create mode 100644 test/blackbox-tests/test-cases/coq/native-compose.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/native-single.t/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/native-single.t/base.opam create mode 100644 test/blackbox-tests/test-cases/coq/native-single.t/dune create mode 100644 test/blackbox-tests/test-cases/coq/native-single.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/native-single.t/foo.v create mode 100644 test/blackbox-tests/test-cases/coq/native-single.t/run.t diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml index af986905087..ff447aac629 100644 --- a/src/dune_rules/coq_lib.ml +++ b/src/dune_rules/coq_lib.ml @@ -2,6 +2,7 @@ open! Dune_engine (* This file is licensed under The MIT License *) (* (c) MINES ParisTech 2018-2019 *) +(* (c) INRIA 2020 *) (* Written by: Emilio Jesús Gallego Arias *) open! Stdune diff --git a/src/dune_rules/coq_lib_name.mli b/src/dune_rules/coq_lib_name.mli index 03cbd1950eb..a4978bc7aa2 100644 --- a/src/dune_rules/coq_lib_name.mli +++ b/src/dune_rules/coq_lib_name.mli @@ -2,6 +2,7 @@ open! Dune_engine (* This file is licensed under The MIT License *) (* (c) MINES ParisTech 2018-2019 *) +(* (c) INRIA 2020 *) (* Written by: Emilio Jesús Gallego Arias *) open! Stdune diff --git a/src/dune_rules/coq_mode.ml b/src/dune_rules/coq_mode.ml new file mode 100644 index 00000000000..1bf1d2d6f52 --- /dev/null +++ b/src/dune_rules/coq_mode.ml @@ -0,0 +1,10 @@ +(* This file is licensed under The MIT License *) +(* (c) MINES ParisTech 2018-2019 *) +(* (c) INRIA 2020 *) +(* Written by: Emilio Jesús Gallego Arias *) + +type t = + | VoOnly + | Native + +let decode = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ]) diff --git a/src/dune_rules/coq_mode.mli b/src/dune_rules/coq_mode.mli new file mode 100644 index 00000000000..ebdea59ee2d --- /dev/null +++ b/src/dune_rules/coq_mode.mli @@ -0,0 +1,10 @@ +(* This file is licensed under The MIT License *) +(* (c) MINES ParisTech 2018-2019 *) +(* (c) INRIA 2020 *) +(* Written by: Emilio Jesús Gallego Arias *) + +type t = + | VoOnly + | Native + +val decode : t Dune_lang.Decoder.t diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/coq_module.ml index 6a68e7ee717..e93da5bfbc3 100644 --- a/src/dune_rules/coq_module.ml +++ b/src/dune_rules/coq_module.ml @@ -2,6 +2,7 @@ open! Dune_engine (* This file is licensed under The MIT License *) (* (c) MINES ParisTech 2018-2019 *) +(* (c) INRIA 2020 *) (* Written by: Emilio Jesús Gallego Arias *) open! Stdune @@ -39,23 +40,44 @@ let name x = x.name let build_vo_dir ~obj_dir x = List.fold_left x.prefix ~init:obj_dir ~f:Path.Build.relative -type obj = - | Dep - | Aux - | Glob - | Obj - -let fname_of_obj t obj = - match obj with - | Dep -> t.name ^ ".v.d" - | Aux -> "." ^ t.name ^ ".aux" - | Glob -> t.name ^ ".glob" - | Obj -> t.name ^ ".vo" - -let obj_file t obj ~obj_dir = - let vo_dir = build_vo_dir ~obj_dir t in - let fname = fname_of_obj t obj in - Path.Build.relative vo_dir fname +let cmxs_of_mod ~wrapper_name x = + let native_base = + "N" ^ String.concat ~sep:"_" ((wrapper_name :: x.prefix) @ [ x.name ]) + in + [ native_base ^ ".cmi"; native_base ^ ".cmxs" ] + +let dep_file x ~obj_dir = + let vo_dir = build_vo_dir ~obj_dir x in + Path.Build.relative vo_dir (x.name ^ ".v.d") + +type obj_files_mode = + | Build + | Install + +(* XXX: Remove the install .coq-native hack once rules can output targets in + multiple subdirs *) +let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode = + let vo_dir = build_vo_dir ~obj_dir x in + let install_vo_dir = String.concat ~sep:"/" x.prefix in + let native_objs = + match mode with + | Coq_mode.Native -> + let cmxs_obj = cmxs_of_mod ~wrapper_name x in + List.map + ~f:(fun x -> + ( Path.Build.relative vo_dir x + , Filename.(concat (concat install_vo_dir ".coq-native") x) )) + cmxs_obj + | VoOnly -> [] + in + let obj_files = + match obj_files_mode with + | Build -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ] + | Install -> [ x.name ^ ".vo" ] + in + List.map obj_files ~f:(fun fname -> + (Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname)) + @ native_objs let to_dyn { source; prefix; name } = let open Dyn.Encoder in diff --git a/src/dune_rules/coq_module.mli b/src/dune_rules/coq_module.mli index 1dcb648cbad..5c48f061c71 100644 --- a/src/dune_rules/coq_module.mli +++ b/src/dune_rules/coq_module.mli @@ -38,13 +38,23 @@ val prefix : t -> string list val name : t -> Name.t -type obj = - | Dep - | Aux - | Glob - | Obj - -val obj_file : t -> obj -> obj_dir:Path.Build.t -> Path.Build.t +val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t + +(** Some of the object files should not be installed, we control this with the + following parameter *) +type obj_files_mode = + | Build + | Install + +(** This returns a list of pairs [(obj_file, install_path)] due to native files + having a different install location *) +val obj_files : + t + -> wrapper_name:string + -> mode:Coq_mode.t + -> obj_dir:Path.Build.t + -> obj_files_mode:obj_files_mode + -> (Path.Build.t * string) list val to_dyn : t -> Dyn.t diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 1e0099df6c1..ad402035efe 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -4,6 +4,7 @@ open! Dune_engine (* (c) MINES ParisTech 2018-2019 *) (* (c) INRIA 2020 *) (* Written by: Emilio Jesús Gallego Arias *) +(* Written by: Rudi Grinberg *) open! Stdune open Coq_stanza @@ -19,6 +20,13 @@ module Util = struct let info = Lib.info t in Lib_info.src_dir info) + let native_paths ts = + List.fold_left ts ~init:Path.Set.empty ~f:(fun acc t -> + let info = Lib.info t in + (* We want the cmi files *) + let obj_dir = Obj_dir.public_cmi_dir (Lib_info.obj_dir info) in + Path.Set.add acc obj_dir) + let include_flags ts = include_paths ts |> Lib.L.to_iflags (* coqdep expects an mlpack file next to the sources otherwise it @@ -95,6 +103,9 @@ module Context = struct ; boot_type : Bootstrap.t ; build_dir : Path.Build.t ; profile_flags : Ordered_set_lang.Unexpanded.t + ; mode : Coq_mode.t + ; native_includes : Path.Set.t Or_exn.t + ; native_theory_includes : Path.Build.Set.t Or_exn.t } let coqc ?stdout_to t args = @@ -137,6 +148,30 @@ module Context = struct in [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ] + let coqc_native_flags cctx = + match cctx.mode with + | Coq_mode.VoOnly -> [] + | Coq_mode.Native -> + let native_include_ml_args = + Path.Set.fold + (Result.ok_exn cctx.native_includes) + ~f:(fun dir acc -> Command.Args.Path dir :: A "-nI" :: acc) + ~init:[] + in + let native_include_theory_output = + Path.Build.Set.fold + (Result.ok_exn cctx.native_theory_includes) + ~f:(fun dir acc -> + Command.Args.Path (Path.build dir) :: A "-nI" :: acc) + ~init:[] + in + (* This dir is relative to the file, by default [.coq-native/] *) + [ Command.Args.As [ "-native-output-dir"; "." ] + ; Command.Args.As [ "-native-compiler"; "on" ] + ; Command.Args.S (List.rev native_include_ml_args) + ; Command.Args.S (List.rev native_include_theory_output) + ] + (* compute include flags and mlpack rules *) let setup_ml_deps ~lib_db libs theories = (* Pair of include flags and paths to mlpack *) @@ -152,7 +187,24 @@ module Context = struct (* If the mlpack files don't exist, don't fail *) Build.paths_existing (List.concat_map ~f:Util.ml_pack_files libs)) ) - let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps + let directories_of_lib ~sctx lib = + let name = Coq_lib.name lib in + let dir = Coq_lib.src_root lib in + let dir_contents = Dir_contents.get sctx ~dir in + let coq_sources = Dir_contents.coq dir_contents in + Coq_sources.directories coq_sources ~name + + let setup_native_theory_includes ~sctx ~mode + ~(theories_deps : Coq_lib.t list Or_exn.t) ~theory_dirs = + match mode with + | Coq_mode.Native -> + Result.map theories_deps ~f:(fun theories_deps -> + List.fold_left theories_deps ~init:theory_dirs ~f:(fun acc lib -> + let theory_dirs = directories_of_lib ~sctx lib in + Path.Build.Set.(union acc (of_list theory_dirs)))) + | Coq_mode.VoOnly -> Or_exn.return Path.Build.Set.empty + + let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps ~theory_dirs (buildable : Buildable.t) = let loc = buildable.loc in let rr = resolve_program sctx ~dir ~loc in @@ -163,6 +215,13 @@ module Context = struct let ml_flags, mlpack_rule = setup_ml_deps ~lib_db buildable.libraries theories_deps in + let native_includes = + Lib.DB.resolve lib_db (Loc.none, Lib_name.of_string "coq.kernel") + |> Result.map ~f:(fun lib -> Util.native_paths [ lib ]) + in + let native_theory_includes = + setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs + in let build_dir = (Super_context.context sctx).build_dir in { coqdep = rr "coqdep" ; coqc = (rr "coqc", coqc_dir) @@ -177,6 +236,9 @@ module Context = struct ; boot_type = Bootstrap.No_boot ; build_dir ; profile_flags = Super_context.coq sctx ~dir + ; mode = snd buildable.mode + ; native_includes + ; native_theory_includes } let for_module t coq_module = @@ -240,7 +302,7 @@ let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module :: deps ) let deps_of ~dir ~boot_type coq_module = - let stdout_to = Coq_module.obj_file ~obj_dir:dir coq_module Dep in + let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in Build.dyn_paths_unit (Build.map (Build.lines_of (Path.build stdout_to)) @@ -255,7 +317,7 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module = ; Dep (Path.build source) ] in - let stdout_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Dep in + let stdout_to = Coq_module.dep_file ~obj_dir:cctx.dir coq_module in (* Coqdep has to be called in the stanza's directory *) let open Build.With_targets.O in Build.with_no_targets cctx.mlpack_rule @@ -265,10 +327,15 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module = let coqc_rule (cctx : _ Context.t) ~file_flags coq_module = let source = Coq_module.source coq_module in let file_flags = - let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Obj in - let aux = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Aux in - let glob = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Glob in - [ Command.Args.Hidden_targets [ object_to; aux; glob ] + let wrapper_name, mode = (cctx.wrapper_name, cctx.mode) in + let objects_to = + Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:cctx.dir + ~obj_files_mode:Coq_module.Build coq_module + |> List.map ~f:fst + in + let native_flags = Context.coqc_native_flags cctx in + [ Command.Args.Hidden_targets objects_to + ; S native_flags ; S file_flags ; Command.Args.Dep (Path.build source) ] @@ -329,19 +396,20 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) = let coq_lib_db = Scope.coq_libs scope in let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in + let coq_dir_contents = Dir_contents.coq dir_contents in + let cctx = let wrapper_name = Coq_lib.wrapper theory in - (* Coq flags for depending libraries *) let theories_deps = Coq_lib.DB.requires coq_lib_db theory in + let theory_dirs = Coq_sources.directories coq_dir_contents ~name in + let theory_dirs = Path.Build.Set.of_list theory_dirs in let coqc_dir = (Super_context.context sctx).build_dir in - Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps s.buildable + Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps ~theory_dirs + s.buildable in (* List of modules to compile for this library *) - let coq_modules = - let coq = Dir_contents.coq dir_contents in - Coq_sources.library coq ~name - in + let coq_modules = Coq_sources.library coq_dir_contents ~name in let source_rule = let theories = @@ -393,7 +461,7 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) = let install_rules ~sctx ~dir s = match s with | { Theory.package = None; _ } -> [] - | { Theory.package = Some package; _ } -> + | { Theory.package = Some package; buildable = { mode; _ }; _ } -> let loc = s.buildable.loc in let scope = SC.find_scope_by_dir sctx dir in let dir_contents = Dir_contents.get sctx ~dir in @@ -417,21 +485,29 @@ let install_rules ~sctx ~dir s = else coq_plugins_install_rules ~scope ~package ~dst_dir s in + let wrapper_name = dst_suffix in + let mode = snd mode in + let to_path f = Path.reach ~from:(Path.build dir) (Path.build f) in + let to_dst f = Path.Local.to_string @@ Path.Local.relative dst_dir f in + let make_entry (orig_file : Path.Build.t) (dst_file : string) = + ( Some loc + , (* Entry.make Section.Lib_root ~dst:(to_dst (to_path dst_file)) + orig_file) *) + Install.Entry.make Section.Lib_root ~dst:(to_dst dst_file) orig_file ) + in Dir_contents.coq dir_contents |> Coq_sources.library ~name |> List.concat_map ~f:(fun (vfile : Coq_module.t) -> - let to_path f = Path.reach ~from:(Path.build dir) (Path.build f) in - let to_dst f = - Path.Local.to_string @@ Path.Local.relative dst_dir f + let obj_files = + Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:dir + ~obj_files_mode:Coq_module.Install vfile + |> List.map + ~f:(fun ((vo_file : Path.Build.t), (install_vo_file : string)) + -> make_entry vo_file install_vo_file) in - let vofile = Coq_module.obj_file ~obj_dir:dir vfile Obj in let vfile = Coq_module.source vfile in - let make_entry file = - ( Some loc - , Install.(Entry.make Lib_root ~dst:(to_dst (to_path file)) file) - ) - in - [ make_entry vfile; make_entry vofile ]) + let vfile_dst = to_path vfile in + make_entry vfile vfile_dst :: obj_files) |> List.rev_append coq_plugins_install_rules let coqpp_rules ~sctx ~dir (s : Coqpp.t) = @@ -453,8 +529,9 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) = let coq_lib_db = Scope.coq_libs scope in Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories in + let theory_dirs = Path.Build.Set.empty in Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps - s.buildable + ~theory_dirs s.buildable in let coq_module = let coq = Dir_contents.coq dir_contents in diff --git a/src/dune_rules/coq_rules.mli b/src/dune_rules/coq_rules.mli index c3070625476..1ecaff74a94 100644 --- a/src/dune_rules/coq_rules.mli +++ b/src/dune_rules/coq_rules.mli @@ -2,6 +2,7 @@ open! Dune_engine (* This file is licensed under The MIT License *) (* (c) MINES ParisTech 2018-2019 *) +(* (c) INRIA 2020 *) (* Written by: Emilio Jesús Gallego Arias *) (* Build rules for Coq's .v -> .vo files *) diff --git a/src/dune_rules/coq_sources.ml b/src/dune_rules/coq_sources.ml index 562b74a9cb8..935fa7168ff 100644 --- a/src/dune_rules/coq_sources.ml +++ b/src/dune_rules/coq_sources.ml @@ -8,10 +8,17 @@ open Coq_stanza In Coq all libs are "wrapped" so including a module twice is not so bad. *) type t = { libraries : Coq_module.t list Coq_lib_name.Map.t + ; directories : Path.Build.t list Coq_lib_name.Map.t + (* [directories] is used to compute the include paths for Coq's native + mode *) ; extract : Coq_module.t Loc.Map.t } -let empty = { libraries = Coq_lib_name.Map.empty; extract = Loc.Map.empty } +let empty = + { libraries = Coq_lib_name.Map.empty + ; directories = Coq_lib_name.Map.empty + ; extract = Loc.Map.empty + } let coq_modules_of_files ~dirs = let filter_v_files (dir, local, files) = @@ -31,10 +38,15 @@ let coq_modules_of_files ~dirs = let library t ~name = Coq_lib_name.Map.find_exn t.libraries name +let directories t ~name = Coq_lib_name.Map.find_exn t.directories name + let check_no_unqualified (loc, (qualif_mode : Dune_file.Include_subdirs.t)) = if qualif_mode = Include Unqualified then User_error.raise ~loc - [ Pp.text "(include_subdirs unqualified) is not supported yet" ] + [ Pp.text + "(include_subdirs unqualified) is not supported yet with (coq.theory \ + ...) stanzas" + ] let extract t (stanza : Extraction.t) = Loc.Map.find_exn t.extract stanza.buildable.loc @@ -47,10 +59,14 @@ let of_dir (d : _ Dir_with_dune.t) ~include_subdirs ~dirs = let modules = Coq_module.eval ~dir:d.ctx_dir coq.modules ~standard:modules in + let directories = + Coq_lib_name.Map.add_exn acc.directories (snd coq.name) + (List.map dirs ~f:(fun (d, _, _) -> d)) + in let libraries = Coq_lib_name.Map.add_exn acc.libraries (snd coq.name) modules in - { acc with libraries } + { acc with directories; libraries } | Coq_stanza.Extraction.T extract -> let loc, prelude = extract.prelude in let m = diff --git a/src/dune_rules/coq_sources.mli b/src/dune_rules/coq_sources.mli index 5ff5dcb9ff0..89f9ac5001e 100644 --- a/src/dune_rules/coq_sources.mli +++ b/src/dune_rules/coq_sources.mli @@ -10,6 +10,8 @@ val empty : t (** Coq modules of library [name] is the Coq library name. *) val library : t -> name:Coq_lib_name.t -> Coq_module.t list +val directories : t -> name:Coq_lib_name.t -> Path.Build.t list + val extract : t -> Coq_stanza.Extraction.t -> Coq_module.t val of_dir : diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml index 1cdfc8893e2..d7e14575c85 100644 --- a/src/dune_rules/coq_stanza.ml +++ b/src/dune_rules/coq_stanza.ml @@ -21,11 +21,15 @@ end let coq_syntax = Dune_lang.Syntax.create ~name:"coq" ~desc:"the coq extension (experimental)" - [ ((0, 1), `Since (1, 9)); ((0, 2), `Since (2, 5)) ] + [ ((0, 1), `Since (1, 9)) + ; ((0, 2), `Since (2, 5)) + ; ((0, 3), `Since (2, 8)) + ] module Buildable = struct type t = { flags : Ordered_set_lang.Unexpanded.t + ; mode : Loc.t * Coq_mode.t ; libraries : (Loc.t * Lib_name.t) list (** ocaml libraries *) ; theories : (Loc.t * Coq_lib_name.t) list (** coq libraries *) ; loc : Loc.t @@ -34,6 +38,10 @@ module Buildable = struct let decode = let+ loc = loc and+ flags = Ordered_set_lang.Unexpanded.field "flags" + and+ mode = + located + (field "mode" ~default:Coq_mode.VoOnly + (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode)) and+ libraries = field "libraries" (repeat (located Lib_name.decode)) ~default:[] and+ theories = @@ -41,7 +49,7 @@ module Buildable = struct (Dune_lang.Syntax.since coq_syntax (0, 2) >>> repeat Coq_lib_name.decode) ~default:[] in - { flags; libraries; theories; loc } + { flags; mode; libraries; theories; loc } end module Extraction = struct diff --git a/src/dune_rules/coq_stanza.mli b/src/dune_rules/coq_stanza.mli index dd14ce1b550..9435c256cd8 100644 --- a/src/dune_rules/coq_stanza.mli +++ b/src/dune_rules/coq_stanza.mli @@ -4,6 +4,7 @@ open Import module Buildable : sig type t = { flags : Ordered_set_lang.Unexpanded.t + ; mode : Loc.t * Coq_mode.t ; libraries : (Loc.t * Lib_name.t) list (** ocaml libraries *) ; theories : (Loc.t * Coq_lib_name.t) list (** coq libraries *) ; loc : Loc.t diff --git a/src/dune_rules/profile.mli b/src/dune_rules/profile.mli index 9fcbbcb26aa..977ec26cec6 100644 --- a/src/dune_rules/profile.mli +++ b/src/dune_rules/profile.mli @@ -1,5 +1,5 @@ (** Defines build profile for dune. Only one profile is active per context. Some - profiles are treat specially by dune. *) + profiles are treated specially by dune. *) open! Import type t = diff --git a/test/blackbox-tests/test-cases/coq/github3624.t/run.t b/test/blackbox-tests/test-cases/coq/github3624.t/run.t index ecf8c83b1be..6dba3d9b862 100644 --- a/test/blackbox-tests/test-cases/coq/github3624.t/run.t +++ b/test/blackbox-tests/test-cases/coq/github3624.t/run.t @@ -5,4 +5,4 @@ In github #3624, dune created a dune-project with an incorrect using line. > (name foo)) > EOF $ dune build 2>&1 | grep using - Info: Appending this line to dune-project: (using coq 0.2) + Info: Appending this line to dune-project: (using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/bar/bar.v b/test/blackbox-tests/test-cases/coq/native-compose.t/bar/bar.v new file mode 100644 index 00000000000..afe3c3b25d9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/bar/bar.v @@ -0,0 +1,3 @@ +From foo Require Import foo. + +Definition mynum (i : mynat) := 3. diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/bar/dune b/test/blackbox-tests/test-cases/coq/native-compose.t/bar/dune new file mode 100644 index 00000000000..632f5a43a55 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/bar/dune @@ -0,0 +1,7 @@ +(coq.theory + (name bar) + (package base) + (mode native) + (theories foo) + (modules :standard) + (synopsis "Test Coq library")) diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/base.opam b/test/blackbox-tests/test-cases/coq/native-compose.t/base.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/dune b/test/blackbox-tests/test-cases/coq/native-compose.t/dune new file mode 100644 index 00000000000..b53cf1eb053 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/dune @@ -0,0 +1,3 @@ +(rule + (alias default) + (action (echo "%{read:base.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/dune-project b/test/blackbox-tests/test-cases/coq/native-compose.t/dune-project new file mode 100644 index 00000000000..23ca7faaa0e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) + +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/foo/dune b/test/blackbox-tests/test-cases/coq/native-compose.t/foo/dune new file mode 100644 index 00000000000..72c8061029f --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/foo/dune @@ -0,0 +1,6 @@ +(coq.theory + (name foo) + (package base) + (mode native) + (modules :standard) + (synopsis "Test Coq library")) diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/foo/foo.v b/test/blackbox-tests/test-cases/coq/native-compose.t/foo/foo.v new file mode 100644 index 00000000000..53e0ce1b152 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/foo/foo.v @@ -0,0 +1 @@ +Definition mynat := nat. diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t new file mode 100644 index 00000000000..c03453c21e9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t @@ -0,0 +1,22 @@ + $ dune build --profile=release --display short --debug-dependency-path @all + coqdep bar/bar.v.d + coqdep foo/foo.v.d + coqc foo/.foo.aux,foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo} + coqc bar/.bar.aux,bar/Nbar_bar.{cmi,cmxs},bar/bar.{glob,vo} + + $ dune build --profile=release --debug-dependency-path @default + lib: [ + "_build/install/default/lib/base/META" + "_build/install/default/lib/base/dune-package" + "_build/install/default/lib/base/opam" + ] + lib_root: [ + "_build/install/default/lib/coq/user-contrib/bar/.coq-native/Nbar_bar.cmi" {"coq/user-contrib/bar/.coq-native/Nbar_bar.cmi"} + "_build/install/default/lib/coq/user-contrib/bar/.coq-native/Nbar_bar.cmxs" {"coq/user-contrib/bar/.coq-native/Nbar_bar.cmxs"} + "_build/install/default/lib/coq/user-contrib/bar/bar.v" {"coq/user-contrib/bar/bar.v"} + "_build/install/default/lib/coq/user-contrib/bar/bar.vo" {"coq/user-contrib/bar/bar.vo"} + "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi"} + "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs"} + "_build/install/default/lib/coq/user-contrib/foo/foo.v" {"coq/user-contrib/foo/foo.v"} + "_build/install/default/lib/coq/user-contrib/foo/foo.vo" {"coq/user-contrib/foo/foo.vo"} + ] diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/bar.v b/test/blackbox-tests/test-cases/coq/native-single.t/bar.v new file mode 100644 index 00000000000..4627b76131c --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-single.t/bar.v @@ -0,0 +1,3 @@ +From basic Require Import foo. + +Definition mynum (i : mynat) := 3. diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/base.opam b/test/blackbox-tests/test-cases/coq/native-single.t/base.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/dune b/test/blackbox-tests/test-cases/coq/native-single.t/dune new file mode 100644 index 00000000000..11e0122c97d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-single.t/dune @@ -0,0 +1,10 @@ +(coq.theory + (name basic) + (package base) + (mode native) + (modules :standard) + (synopsis "Test Coq library")) + +(rule + (alias default) + (action (echo "%{read:base.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/dune-project b/test/blackbox-tests/test-cases/coq/native-single.t/dune-project new file mode 100644 index 00000000000..23ca7faaa0e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-single.t/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) + +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/foo.v b/test/blackbox-tests/test-cases/coq/native-single.t/foo.v new file mode 100644 index 00000000000..53e0ce1b152 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-single.t/foo.v @@ -0,0 +1 @@ +Definition mynat := nat. diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/run.t b/test/blackbox-tests/test-cases/coq/native-single.t/run.t new file mode 100644 index 00000000000..1b01b367361 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-single.t/run.t @@ -0,0 +1,22 @@ + $ dune build --profile=release --display short --debug-dependency-path @all + coqdep bar.v.d + coqdep foo.v.d + coqc .foo.aux,Nbasic_foo.{cmi,cmxs},foo.{glob,vo} + coqc .bar.aux,Nbasic_bar.{cmi,cmxs},bar.{glob,vo} + + $ dune build --profile=release --debug-dependency-path @default + lib: [ + "_build/install/default/lib/base/META" + "_build/install/default/lib/base/dune-package" + "_build/install/default/lib/base/opam" + ] + lib_root: [ + "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmi"} + "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs"} + "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi"} + "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs"} + "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"} + "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"} + "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"} + "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"} + ] From c6a80cefc537269deb1509dc3c4a4a7e85e96fcf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 2 Sep 2020 20:15:07 +0200 Subject: [PATCH 4/8] [coq] Don't build native files when profile == dev Signed-off-by: Emilio Jesus Gallego Arias --- src/dune_rules/coq_rules.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index ad402035efe..93b81c64cc5 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -88,6 +88,13 @@ end (* get_libraries from Coq's ML dependencies *) let libs_of_coq_deps ~lib_db = Result.List.map ~f:(Lib.DB.resolve lib_db) +let select_native_mode ~sctx ~(buildable : Buildable.t) = + let profile = (SC.context sctx).profile in + if Profile.is_dev profile then + Coq_mode.VoOnly + else + snd buildable.mode + module Context = struct type 'a t = { coqdep : Action.Prog.t @@ -215,6 +222,7 @@ module Context = struct let ml_flags, mlpack_rule = setup_ml_deps ~lib_db buildable.libraries theories_deps in + let mode = select_native_mode ~sctx ~buildable in let native_includes = Lib.DB.resolve lib_db (Loc.none, Lib_name.of_string "coq.kernel") |> Result.map ~f:(fun lib -> Util.native_paths [ lib ]) @@ -236,7 +244,7 @@ module Context = struct ; boot_type = Bootstrap.No_boot ; build_dir ; profile_flags = Super_context.coq sctx ~dir - ; mode = snd buildable.mode + ; mode ; native_includes ; native_theory_includes } @@ -461,7 +469,8 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) = let install_rules ~sctx ~dir s = match s with | { Theory.package = None; _ } -> [] - | { Theory.package = Some package; buildable = { mode; _ }; _ } -> + | { Theory.package = Some package; buildable; _ } -> + let mode = select_native_mode ~sctx ~buildable in let loc = s.buildable.loc in let scope = SC.find_scope_by_dir sctx dir in let dir_contents = Dir_contents.get sctx ~dir in @@ -486,7 +495,6 @@ let install_rules ~sctx ~dir s = coq_plugins_install_rules ~scope ~package ~dst_dir s in let wrapper_name = dst_suffix in - let mode = snd mode in let to_path f = Path.reach ~from:(Path.build dir) (Path.build f) in let to_dst f = Path.Local.to_string @@ Path.Local.relative dst_dir f in let make_entry (orig_file : Path.Build.t) (dst_file : string) = From f688adf65784ac85b50eb033365cec4a2d6f3ad3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 14 Oct 2020 20:44:05 +0200 Subject: [PATCH 5/8] [coq] Documentation and changes for `(mode native)` Signed-off-by: Emilio Jesus Gallego Arias --- CHANGES.md | 2 ++ doc/dune-files.rst | 8 ++++++++ 2 files changed, 10 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 0c1e36e6748..e3af170f3c6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -91,6 +91,8 @@ Unreleased - [coq] Add `-q` flag to `:standard` `coqc` flags , fixes #3924, (#3931 , @ejgallego) +- Add support for Coq's native compute compilation mode (@ejgallego, #3210) + 2.7.1 (2/09/2020) ----------------- diff --git a/doc/dune-files.rst b/doc/dune-files.rst index c5f95cd1fba..cbfc31f3ce0 100644 --- a/doc/dune-files.rst +++ b/doc/dune-files.rst @@ -1625,6 +1625,7 @@ The basic form for defining Coq libraries is very similar to the OCaml form: (modules ) (libraries ) (flags ) + (mode ) (theories )) The stanza will build all ``.v`` files on the given directory. The semantics of fields is: @@ -1668,6 +1669,13 @@ The stanza will build all ``.v`` files on the given directory. The semantics of composition with the Coq's standard library is supported, but in this case the ``Coq`` prefix will be made available in a qualified way. Since Coq's lang version ``0.2``. +- you can enable the production of Coq's native compiler object files + by setting ```` to ``native``, this will pass + ``-native-compiler on`` to Coq and install the corresponding object + files under `.coq-native`. Note that the support for native compute + is experimental, and requires Coq >= 8.12.1; moreover, depending + libraries *must* be built with ``(mode native)`` too for this to + work. Recursive qualification of modules ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From fd6a7124dcd9a2dbdf5f81b5feb20e1a501f8f40 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Wed, 25 Nov 2020 15:29:02 -0800 Subject: [PATCH 6/8] coqc_native_flags: Do not raise exceptions eagerly Signed-off-by: Rudi Grinberg --- src/dune_rules/coq_rules.ml | 44 +++++++++++++++++++------------------ 1 file changed, 23 insertions(+), 21 deletions(-) diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 93b81c64cc5..95105a6bc4a 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -155,29 +155,31 @@ module Context = struct in [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ] - let coqc_native_flags cctx = + let coqc_native_flags cctx : _ Command.Args.t = match cctx.mode with - | Coq_mode.VoOnly -> [] + | Coq_mode.VoOnly -> Command.Args.empty | Coq_mode.Native -> - let native_include_ml_args = - Path.Set.fold - (Result.ok_exn cctx.native_includes) - ~f:(fun dir acc -> Command.Args.Path dir :: A "-nI" :: acc) - ~init:[] + let args = + let open Result.O in + let* native_includes = cctx.native_includes in + let include_ dir acc = Command.Args.Path dir :: A "-nI" :: acc in + let native_include_ml_args = + Path.Set.fold native_includes ~init:[] ~f:include_ + in + let+ native_theory_includes = cctx.native_theory_includes in + let native_include_theory_output = + Path.Build.Set.fold native_theory_includes ~init:[] ~f:(fun dir acc -> + include_ (Path.build dir) acc) + in + (* This dir is relative to the file, by default [.coq-native/] *) + Command.Args.S + [ Command.Args.As [ "-native-output-dir"; "." ] + ; Command.Args.As [ "-native-compiler"; "on" ] + ; Command.Args.S (List.rev native_include_ml_args) + ; Command.Args.S (List.rev native_include_theory_output) + ] in - let native_include_theory_output = - Path.Build.Set.fold - (Result.ok_exn cctx.native_theory_includes) - ~f:(fun dir acc -> - Command.Args.Path (Path.build dir) :: A "-nI" :: acc) - ~init:[] - in - (* This dir is relative to the file, by default [.coq-native/] *) - [ Command.Args.As [ "-native-output-dir"; "." ] - ; Command.Args.As [ "-native-compiler"; "on" ] - ; Command.Args.S (List.rev native_include_ml_args) - ; Command.Args.S (List.rev native_include_theory_output) - ] + Command.of_result args (* compute include flags and mlpack rules *) let setup_ml_deps ~lib_db libs theories = @@ -343,7 +345,7 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module = in let native_flags = Context.coqc_native_flags cctx in [ Command.Args.Hidden_targets objects_to - ; S native_flags + ; native_flags ; S file_flags ; Command.Args.Dep (Path.build source) ] From 0337d3edac01e86cbf17976a8f8c619796edc83d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Nov 2020 21:02:51 +0100 Subject: [PATCH 7/8] [coq] Be explicit about native mode in command line flags This is more robust for Coq 8.13, as the user can specify this option at configure time, which for now we don't really respect. Signed-off-by: Emilio Jesus Gallego Arias --- doc/dune-files.rst | 8 ++++++-- src/dune_rules/coq_rules.ml | 4 +++- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/doc/dune-files.rst b/doc/dune-files.rst index cbfc31f3ce0..6b5c599ad5a 100644 --- a/doc/dune-files.rst +++ b/doc/dune-files.rst @@ -1673,9 +1673,13 @@ The stanza will build all ``.v`` files on the given directory. The semantics of by setting ```` to ``native``, this will pass ``-native-compiler on`` to Coq and install the corresponding object files under `.coq-native`. Note that the support for native compute - is experimental, and requires Coq >= 8.12.1; moreover, depending + is **experimental**, and requires Coq >= 8.12.1; moreover, depending libraries *must* be built with ``(mode native)`` too for this to - work. + work; also Coq must be configured to support native + compilation. Note that Dune will by explicitly disable output of + native compilation objects when `(mode vo)` even if the default + Coq's configure flag enabled it. This will be improved in the + future. Recursive qualification of modules ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 95105a6bc4a..8f0334d0894 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -157,7 +157,9 @@ module Context = struct let coqc_native_flags cctx : _ Command.Args.t = match cctx.mode with - | Coq_mode.VoOnly -> Command.Args.empty + | Coq_mode.VoOnly -> + Command.Args.As + [ "-w"; "-native-compiler-disabled"; "-native-compiler"; "ondemand" ] | Coq_mode.Native -> let args = let open Result.O in From 454dae628f4e8a75a5018914b19a221e599fb6b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Nov 2020 21:04:29 +0100 Subject: [PATCH 8/8] [coq] Renaming function as suggested in review. Signed-off-by: Emilio Jesus Gallego Arias --- src/dune_rules/coq_rules.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 8f0334d0894..f13b0bbb56e 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -20,7 +20,7 @@ module Util = struct let info = Lib.info t in Lib_info.src_dir info) - let native_paths ts = + let coq_nativelib_cmi_dirs ts = List.fold_left ts ~init:Path.Set.empty ~f:(fun acc t -> let info = Lib.info t in (* We want the cmi files *) @@ -229,7 +229,7 @@ module Context = struct let mode = select_native_mode ~sctx ~buildable in let native_includes = Lib.DB.resolve lib_db (Loc.none, Lib_name.of_string "coq.kernel") - |> Result.map ~f:(fun lib -> Util.native_paths [ lib ]) + |> Result.map ~f:(fun lib -> Util.coq_nativelib_cmi_dirs [ lib ]) in let native_theory_includes = setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs