diff --git a/CHANGES.md b/CHANGES.md index 800eafd6adf9..e6b8731d6565 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -166,6 +166,8 @@ Unreleased - Handle renaming of `coq.kernel` library to `coq-core.kernel` in Coq 8.14 (#4713, @proux01) +- Support new Coq 8.14 standalone native compiler mode (# , @ejgallego @ppedrot @Zimmi48) + 2.8.5 (28/03/2021) ------------------ diff --git a/doc/dune-files.rst b/doc/dune-files.rst index 6f25b299ca91..a48bc05bde3e 100644 --- a/doc/dune-files.rst +++ b/doc/dune-files.rst @@ -1691,6 +1691,8 @@ The supported Coq language versions are: - ``0.1``: basic Coq theory support, - ``0.2``: support for the ``theories`` field, and composition of theories in the same scope, - ``0.3``: support for ``(mode native)``, requires Coq >= 8.10 (and dune >= 2.9 for Coq >= 8.14). + This mode is deprecated and we strongly recommend native users to move to version ``0.4`` +- ``0.5``: reworked ``(mode native)`` using the standalone Coq native compiler, requires Coq >= 8.14 and dune >= 3.0. Guarantees with respect to stability are not provided yet, however, as implementation of features progresses, we hope to reach @@ -1753,18 +1755,26 @@ 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`` when in ``release`` profile. The regular - ``dev`` profile will skip native compilation to make the build - faster. Since Coq's lang version ``0.3``. 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; also Coq must be configured to support native - compilation. Note that Dune will 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. + +- you can control the production of Coq's native compiler object files + by setting ```` to ``native`` [the default] or to + ``vo``, to disable the rules relative to Coq native objects. + + By default, Dune uses the ``coqnative`` binary introduced in Coq + 8.14 and will setup the rules for the compilation and install of + native objects when using the ``release`` Dune profile. This can be + tweaked using the ``profile`` field, to enable such rules for + different profiles, for example ``(mode (native (profile dev + release)))`` will enable the rules for the dev profile too. + + Additionally, Dune provides support for installing the native object + files to a different package; by default, Dune will place the Coq + native object files in the main package for the corresponding + ``(coq.theory ...)`` stanza, but users can override that to provide + split compilation using the ``package`` field; example, using: + ``(mode (native (package coq-bar-native)))`` will allow users to use + ``dune -p coq-bar`` and ``dune -p coq-bar-native`` to build the + native files separately, if so desired. Recursive qualification of modules ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml index 92b7eec2857f..791b26047431 100644 --- a/src/dune_rules/coq_lib.ml +++ b/src/dune_rules/coq_lib.ml @@ -81,6 +81,7 @@ module DB = struct type nonrec t = { boot : (Loc.t * t) option ; libs : t Coq_lib_name.Map.t + ; obj_root_revmap : t Path.Build.Map.t } let boot_library { boot; _ } = boot @@ -113,7 +114,12 @@ module DB = struct | _ :: (_, s2) :: _ -> Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.buildable.loc s2) in - { boot; libs } + let obj_root_revmap = + Coq_lib_name.Map.fold libs ~init:Path.Build.Map.empty ~f:(fun lib rmap -> + let dir = obj_root lib in + Path.Build.Map.add_exn rmap dir lib) + in + { boot; libs; obj_root_revmap } let resolve ?(allow_private_deps = true) db (loc, name) = match Coq_lib_name.Map.find db.libs name with @@ -165,4 +171,17 @@ module DB = struct top_closure db theories ~loc ~allow_private_deps:true let resolve db l = resolve db l + + let module_of_source_file { obj_root_revmap; _ } file = + let name = Path.Build.basename file in + let dir = Path.Build.parent_exn file in + let rec aux acc_prefix dir = + match Path.Build.Map.find obj_root_revmap dir with + | None -> + let acc_prefix = Path.Build.basename dir :: acc_prefix in + let dir = Path.Build.parent_exn dir in + aux acc_prefix dir + | Some lib -> (lib, List.rev acc_prefix, name) + in + aux [] dir end diff --git a/src/dune_rules/coq_lib.mli b/src/dune_rules/coq_lib.mli index 06494d517435..84613b5882a8 100644 --- a/src/dune_rules/coq_lib.mli +++ b/src/dune_rules/coq_lib.mli @@ -43,5 +43,14 @@ module DB : sig val requires_for_user_written : t -> (Loc.t * Coq_lib_name.t) list -> lib list Or_exn.t + + (** Reverse map from source names to a matching lib, plus the matching suffix; + this is only required because coqdep doesn't handle native dependencies, + so for a dependency [path/bar/foo.vo] we must correctly translate it to + its mangled Coq native form, which requires locating the library which a + source does belong to. The current matching function does return a triple + [lib, + prefix, name] for a given input path, or raises if not found *) + val module_of_source_file : t -> Path.Build.t -> lib * string list * string end with type lib := t diff --git a/src/dune_rules/coq_mode.ml b/src/dune_rules/coq_mode.ml index e28650f628a4..0426d9bf8aa8 100644 --- a/src/dune_rules/coq_mode.ml +++ b/src/dune_rules/coq_mode.ml @@ -10,5 +10,25 @@ type t = | Legacy | VoOnly | Native + | Split of + { package : string option + ; profile : string list + } -let decode = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ]) +let default_profile = [ "release" ] + +let default = Split { package = None; profile = default_profile } + +let decode_v03 = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ]) + +let decode_v04 = + let open Dune_lang.Decoder in + let native = + fields + (let+ package = field_o "package" string + and+ profile = + field ~default:default_profile "profile" (repeat string) + in + Split { package; profile }) + in + sum [ ("vo", return VoOnly); ("native", native) ] diff --git a/src/dune_rules/coq_mode.mli b/src/dune_rules/coq_mode.mli index 44de8b5bec44..a8a6addb1bfd 100644 --- a/src/dune_rules/coq_mode.mli +++ b/src/dune_rules/coq_mode.mli @@ -10,5 +10,14 @@ type t = | Legacy | VoOnly | Native + | Split of + { package : string option + ; profile : string list + } -val decode : t Dune_lang.Decoder.t +val default : t + +(* We provide two different decoders depending on the Coq language syntax *) +val decode_v03 : t Dune_lang.Decoder.t + +val decode_v04 : t Dune_lang.Decoder.t diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/coq_module.ml index 6b160d4b1639..458a9d4ab2ca 100644 --- a/src/dune_rules/coq_module.ml +++ b/src/dune_rules/coq_module.ml @@ -37,37 +37,50 @@ let prefix x = x.prefix let name x = x.name -let build_vo_dir ~obj_dir x = - List.fold_left x.prefix ~init:obj_dir ~f:Path.Build.relative +let build_vo_dir ~obj_dir ~prefix = + List.fold_left prefix ~init:obj_dir ~f:Path.Build.relative + +let mangled_native_filename ~wrapper_name ~prefix ~name = + "N" ^ String.concat ~sep:"_" (wrapper_name :: prefix @ [ name ]) let cmxs_of_mod ~wrapper_name x = let native_base = - "N" ^ String.concat ~sep:"_" (wrapper_name :: x.prefix @ [ x.name ]) + mangled_native_filename ~wrapper_name ~prefix:x.prefix ~name:x.name in [ native_base ^ ".cmi"; native_base ^ ".cmxs" ] +let native_mangle_filename ~wrapper_name ~prefix ~name ~obj_dir ~ext = + let native_base = mangled_native_filename ~wrapper_name ~prefix ~name in + let vo_dir = build_vo_dir ~obj_dir ~prefix in + Path.Build.relative vo_dir (native_base ^ ext) + let dep_file x ~obj_dir = - let vo_dir = build_vo_dir ~obj_dir x in + let vo_dir = build_vo_dir ~obj_dir ~prefix:x.prefix in Path.Build.relative vo_dir (x.name ^ ".v.d") type obj_files_mode = | Build | Install +let native_obj_files_core x ~wrapper_name ~vo_dir ~install_vo_dir = + 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 + (* 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 vo_dir = build_vo_dir ~obj_dir ~prefix:x.prefix 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 + native_obj_files_core x ~wrapper_name ~vo_dir ~install_vo_dir + (* split mode doesn't produce any file for coqc *) + | Split _ | VoOnly | Legacy -> [] @@ -81,6 +94,16 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode = (Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname)) @ native_objs +let vo_obj_file x ~obj_dir = + let vo_dir = build_vo_dir ~obj_dir ~prefix:x.prefix in + let fname = x.name ^ ".vo" in + Path.Build.relative vo_dir fname + +let native_obj_files x ~wrapper_name ~obj_dir = + let vo_dir = build_vo_dir ~obj_dir ~prefix:x.prefix in + let install_vo_dir = String.concat ~sep:"/" x.prefix in + native_obj_files_core x ~wrapper_name ~vo_dir ~install_vo_dir + let to_dyn { source; prefix; name } = let open Dyn.Encoder in record diff --git a/src/dune_rules/coq_module.mli b/src/dune_rules/coq_module.mli index 5c48f061c715..0dc9c7fb2bc9 100644 --- a/src/dune_rules/coq_module.mli +++ b/src/dune_rules/coq_module.mli @@ -46,8 +46,11 @@ 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 *) +(** [obj_files t wrapper_name mode obj_dir obj_files_mode] returns the list of + object files produced by a [coqc] invocation. + + Note that This returns a list of pairs [(obj_file, install_path)] due to + native files having a different install / build location *) val obj_files : t -> wrapper_name:string @@ -56,6 +59,39 @@ val obj_files : -> obj_files_mode:obj_files_mode -> (Path.Build.t * string) list +(** [obj_file t] returns just the .vo file of a module, this is the input to the + standalone Coq native compiler; we should likely refactor this to pass the + kind of object to obj_files as it was done some time ago by Rudi *) +val vo_obj_file : t -> obj_dir:Path.Build.t -> Path.Build.t + +(** [native_obj_files] is the equivalent of [obj_files] but for the new + [coqnative] separate Coq native compiler, it is used in the setup of the + separate rules. *) +val native_obj_files : + t + -> wrapper_name:string + -> obj_dir:Path.Build.t + -> (Path.Build.t * string) list + +(** [native_mangle_filename ~wrapper_name ~prefix ~name ~ext] will generate a + mangled Coq native module file name from its arguments, determining a Coq + module. Coq's native compiler needs to mangle filenames for a module + [bar/foo.vo] bound to a [wrapper_name] [baz] to [NBaz_Bar_Foo.cmxs] to + prevent collisions, as the OCaml compiler doesn't support encoding hiearchy + of modules using the filesystem. We should eventually improve the clients of + this API so we can just pass here a [Coq_module.t] *) +val native_mangle_filename : + wrapper_name:string + -> prefix:string list + -> name:string + -> obj_dir:Path.Build.t + -> ext:string + -> Path.Build.t + +(** [vo_to_native file ~ext] will transform a file of the form , note we need a + reverse lookup from .vo file to Coq module *) +(* val vo_to_native : Path.Build.t -> ext:string -> Path.Build.t *) + val to_dyn : t -> Dyn.t val eval : dir:Path.Build.t -> standard:t list -> Ordered_set_lang.t -> t list diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 01e2c72ed6a5..8d0f650f3b43 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -91,10 +91,18 @@ let libs_of_coq_deps ~lib_db = Resolve.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 + let profile_name = Profile.to_string profile in + match snd buildable.mode with + | Coq_mode.Split { profile; _ } as mode -> + if List.mem ~equal:String.equal profile profile_name then + mode + else + Coq_mode.VoOnly + | _ -> + if Profile.is_dev profile then + Coq_mode.VoOnly + else + snd buildable.mode let rec resolve_first lib_db = function | [] -> assert false @@ -109,6 +117,7 @@ let rec resolve_first lib_db = function module Context = struct type 'a t = { coqdep : Action.Prog.t + ; coqnative : Action.Prog.t * Path.Build.t ; coqc : Action.Prog.t * Path.Build.t ; wrapper_name : string ; dir : Path.Build.t @@ -130,6 +139,10 @@ module Context = struct let dir = Path.build (snd t.coqc) in Command.run ~dir ?stdout_to (fst t.coqc) args + let coqnative ?stdout_to t args = + let dir = Path.build (snd t.coqnative) in + Command.run ~dir ?stdout_to (fst t.coqnative) args + let standard_coq_flags = Action_builder.return [ "-q" ] let coq_flags t = @@ -173,7 +186,13 @@ module Context = struct | Coq_mode.Legacy -> Command.Args.As [] | Coq_mode.VoOnly -> Command.Args.As - [ "-w"; "-native-compiler-disabled"; "-native-compiler"; "ondemand" ] + [ "-w" + ; "-deprecated-native-compiler-option" + ; "-w" + ; "-native-compiler-disabled" + ; "-native-compiler" + ; "ondemand" + ] | Coq_mode.Native -> let args = let open Resolve.O in @@ -190,12 +209,35 @@ module Context = struct (* This dir is relative to the file, by default [.coq-native/] *) Command.Args.S [ Command.Args.As [ "-native-output-dir"; "." ] + ; Command.Args.As [ "-w"; "-deprecated-native-compiler-option" ] ; 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 Resolve.args args + (* In split mode coqc will produce no files *) + | Coq_mode.Split _ -> Command.Args.As [] + + let coqnative_flags cctx : _ Command.Args.t = + (let open Resolve.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.S (List.rev native_include_ml_args) + ; Command.Args.S (List.rev native_include_theory_output) + ]) + |> Resolve.args (* compute include flags and mlpack rules *) let setup_ml_deps ~lib_db libs theories = @@ -224,6 +266,8 @@ module Context = struct let setup_native_theory_includes ~sctx ~mode ~(theories_deps : Coq_lib.t list Resolve.t) ~theory_dirs = match mode with + (* In split mode, we do use the same includes than in legacy coqc mode *) + | Coq_mode.Split _ | Coq_mode.Native -> Resolve.Build.bind theories_deps ~f:(fun theories_deps -> let+ l = @@ -255,10 +299,12 @@ module Context = struct let+ native_theory_includes = setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs and+ coqdep = rr "coqdep" + and+ coqnative = rr "coqnative" and+ coqc = rr "coqc" and+ profile_flags = Super_context.coq sctx ~dir in { coqdep ; coqc = (coqc, coqc_dir) + ; coqnative = (coqnative, coqc_dir) ; wrapper_name ; dir ; expander @@ -284,7 +330,7 @@ module Context = struct end let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module - (lines : string list) = + (lines : string list) : Path.Build.t list = if coq_debug then Format.eprintf "Parsing coqdep @\n%!"; let source = Coq_module.source coq_module in let invalid phase = @@ -326,21 +372,54 @@ let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module deps; (* Add prelude deps for when stdlib is in scope and we are not actually compiling the prelude *) - let deps = List.map ~f:(Path.relative (Path.build dir)) deps in + let deps = List.map ~f:(Path.Build.relative dir) deps in match boot_type with | No_boot | Bootstrap_prelude -> deps | Bootstrap lib -> - Path.relative (Path.build (Coq_lib.src_root lib)) "Init/Prelude.vo" - :: deps) + Path.Build.relative (Coq_lib.src_root lib) "Init/Prelude.vo" :: deps) let deps_of ~dir ~boot_type coq_module = let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in Action_builder.dyn_paths_unit (Action_builder.map (Action_builder.lines_of (Path.build stdout_to)) - ~f:(parse_coqdep ~dir ~boot_type ~coq_module)) + ~f:(fun line -> + parse_coqdep ~dir ~boot_type ~coq_module line |> List.map ~f:Path.build)) + +(* Coqdep is not aware of dependencies of Coq native compilation at all, see + coq/coq#13035; hopefully the new coqnative setup will help us alleviate these + problems, but meanwhile we need to do a hack to transform deps into the right + native ones *) +let amend_for_native ~coq_lib_db ~ext vofile = + (* FIXME: need to make this principled and link with the code in coq_module *) + let vfile = Path.Build.set_extension vofile ~ext:".v" in + let lib, prefix, name = Coq_lib.DB.module_of_source_file coq_lib_db vfile in + let obj_dir = Coq_lib.obj_root lib in + let wrapper_name = Coq_lib.wrapper lib in + let name, _ = Filename.split_extension name in + Coq_module.native_mangle_filename ~wrapper_name ~prefix ~name ~obj_dir ~ext + |> Path.build + +let parse_coqdep_and_amend_for_native ~dir ~coq_lib_db ~boot_type ~coq_module + lines = + parse_coqdep ~dir ~boot_type ~coq_module lines + |> List.filter ~f:(fun file -> String.equal (Path.Build.extension file) ".vo") + |> List.concat_map ~f:(fun vo_file -> + [ amend_for_native ~coq_lib_db ~ext:".cmi" vo_file + ; amend_for_native ~coq_lib_db ~ext:".cmxs" vo_file + ]) + +(* Factorize to avoid doubly-parsing coqdep *) +let deps_of_native ~coq_lib_db ~dir ~boot_type coq_module = + let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in + Action_builder.dyn_paths_unit + (Action_builder.map + (Action_builder.lines_of (Path.build stdout_to)) + ~f: + (parse_coqdep_and_amend_for_native ~coq_lib_db ~dir ~boot_type + ~coq_module)) let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module = (* coqdep needs the full source + plugin's mlpack to be present :( *) @@ -383,14 +462,38 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module = let coq_flags = Context.coq_flags cctx in Context.coqc cctx (Command.Args.dyn coq_flags :: file_flags) +let coqnative_rule (cctx : _ Context.t) ~file_flags coq_module = + let obj_dir = cctx.dir in + let vo_source = Coq_module.vo_obj_file coq_module ~obj_dir in + let objects_to = + Coq_module.native_obj_files ~wrapper_name:cctx.wrapper_name ~obj_dir + coq_module + |> List.map ~f:fst + in + let native_flags = Context.coqnative_flags cctx in + let file_flags = + [ Command.Args.Hidden_targets objects_to + ; native_flags + ; S file_flags + ; Command.Args.Dep (Path.build vo_source) + ] + in + let open Action_builder.With_targets.O in + (* The way we handle the transitive dependencies of .vo files is not safe for + sandboxing *) + Action_builder.with_no_targets + (Action_builder.dep (Dep.sandbox_config Sandbox_config.no_sandboxing)) + >>> Context.coqnative cctx file_flags + module Module_rule = struct type t = { coqdep : Action.t Action_builder.With_targets.t ; coqc : Action.t Action_builder.With_targets.t + ; coqnative : Action.t Action_builder.With_targets.t option } end -let setup_rule cctx ~source_rule coq_module = +let setup_rule cctx ~coq_lib_db ~source_rule coq_module = let open Action_builder.With_targets.O in if coq_debug then Format.eprintf "gen_rule coq_module: %a@\n%!" Pp.to_fmt @@ -398,12 +501,23 @@ let setup_rule cctx ~source_rule coq_module = let file_flags = Context.coqc_file_flags cctx in let coqdep_rule = coqdep_rule cctx ~source_rule ~file_flags coq_module in (* Process coqdep and generate rules *) - let deps_of = deps_of ~dir:cctx.dir ~boot_type:cctx.boot_type coq_module in + let deps_of_vo = deps_of ~dir:cctx.dir ~boot_type:cctx.boot_type coq_module in + let deps_of_native = + deps_of_native ~coq_lib_db ~dir:cctx.dir ~boot_type:cctx.boot_type + coq_module + in (* Rules for the files *) { Module_rule.coqdep = coqdep_rule ; coqc = - Action_builder.with_no_targets deps_of + Action_builder.with_no_targets deps_of_vo >>> coqc_rule cctx ~file_flags coq_module + ; coqnative = + (match cctx.mode with + | Split _ -> + Some + (Action_builder.with_no_targets deps_of_native + >>> coqnative_rule cctx ~file_flags coq_module) + | _ -> None) } let coq_modules_of_theory ~sctx lib = @@ -454,8 +568,10 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) = in List.concat_map coq_modules ~f:(fun m -> let cctx = Context.for_module cctx m in - let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule m in - [ coqc; coqdep ]) + let { Module_rule.coqc; coqdep; coqnative } = + setup_rule cctx ~coq_lib_db ~source_rule m + in + [ coqc; coqdep ] @ Option.to_list coqnative) (******************************************************************************) (* Install rules *) @@ -524,16 +640,19 @@ let install_rules ~sctx ~dir s = 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 ) + , Install.Entry.make Section.Lib_root ~dst:(to_dst dst_file) orig_file ) in let+ coq_sources = Dir_contents.coq dir_contents in coq_sources |> Coq_sources.library ~name |> List.concat_map ~f:(fun (vfile : Coq_module.t) -> + (* FIXME: take into account the package override *) let obj_files = - Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:dir - ~obj_files_mode:Coq_module.Install vfile + (match mode with + | Split _ -> + Coq_module.native_obj_files ~wrapper_name ~obj_dir:dir vfile + | _ -> []) + @ 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) @@ -555,11 +674,11 @@ let coqpp_rules ~sctx ~dir (s : Coqpp.t) = List.map ~f:mlg_rule s.modules let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) = + let scope = SC.find_scope_by_dir sctx dir in + let coq_lib_db = Scope.coq_libs scope in let* cctx = let wrapper_name = "DuneExtraction" in let theories_deps = - let scope = SC.find_scope_by_dir sctx dir in - let coq_lib_db = Scope.coq_libs scope in Resolve.of_result (Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories) in @@ -579,6 +698,8 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) = let open Action_builder.O in theories >>> Action_builder.path (Path.build (Coq_module.source coq_module)) in - let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule coq_module in + let { Module_rule.coqc; coqdep; coqnative = _ } = + setup_rule cctx ~coq_lib_db ~source_rule coq_module + in let coqc = Action_builder.With_targets.add coqc ~targets:ml_targets in [ coqdep; coqc ] diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml index 8520de6fa4f1..849a8be34147 100644 --- a/src/dune_rules/coq_stanza.ml +++ b/src/dune_rules/coq_stanza.ml @@ -24,6 +24,7 @@ let coq_syntax = [ ((0, 1), `Since (1, 9)) ; ((0, 2), `Since (2, 5)) ; ((0, 3), `Since (2, 8)) + ; ((0, 5), `Since (3, 0)) ] module Buildable = struct @@ -41,14 +42,20 @@ module Buildable = struct and+ mode = let* version = Dune_lang.Syntax.get_exn coq_syntax in let default = - if version < (0, 3) then - Coq_mode.Legacy + if version < (0, 5) then + if version < (0, 3) then + Coq_mode.Legacy + else + Coq_mode.VoOnly else - Coq_mode.VoOnly + Coq_mode.default in located (field "mode" ~default - (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode)) + (if version < (0, 5) then + Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode_v03 + else + Dune_lang.Syntax.since coq_syntax (0, 5) >>> Coq_mode.decode_v04)) and+ libraries = field "libraries" (repeat (located Lib_name.decode)) ~default:[] and+ theories = diff --git a/test/blackbox-tests/test-cases/coq/compose-plugin.t/src_a/dune b/test/blackbox-tests/test-cases/coq/compose-plugin.t/src_a/dune index 268e6ede624e..7404181175f9 100644 --- a/test/blackbox-tests/test-cases/coq/compose-plugin.t/src_a/dune +++ b/test/blackbox-tests/test-cases/coq/compose-plugin.t/src_a/dune @@ -2,6 +2,6 @@ (public_name cplugin.ml_plugin_a) (name ml_plugin_a) (flags :standard -rectypes) - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules gram)) 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 c3914ff4f2b5..3aa947fcadf3 100644 --- a/test/blackbox-tests/test-cases/coq/github3624.t/run.t +++ b/test/blackbox-tests/test-cases/coq/github3624.t/run.t @@ -12,5 +12,5 @@ that the error message is good when the coq extension is not enabled. 1 | (coq.theory 2 | (name foo)) Error: 'coq.theory' is available only when coq is enabled in the dune-project - file. You must enable it using (using coq 0.3) in your dune-project file. + file. You must enable it using (using coq 0.5) in your dune-project file. [1] diff --git a/test/blackbox-tests/test-cases/coq/ml-lib.t/src_a/dune b/test/blackbox-tests/test-cases/coq/ml-lib.t/src_a/dune index 7e053c7bba02..2bbf566373d1 100644 --- a/test/blackbox-tests/test-cases/coq/ml-lib.t/src_a/dune +++ b/test/blackbox-tests/test-cases/coq/ml-lib.t/src_a/dune @@ -2,6 +2,6 @@ (public_name ml_lib.ml_plugin_a) (name ml_plugin_a) (flags :standard -rectypes) - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules gram)) diff --git a/test/blackbox-tests/test-cases/coq/native-split.t/bar/bar.v b/test/blackbox-tests/test-cases/coq/native-split.t/bar/bar.v new file mode 100644 index 000000000000..afe3c3b25d94 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-split.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-split.t/bar/dune b/test/blackbox-tests/test-cases/coq/native-split.t/bar/dune new file mode 100644 index 000000000000..632f5a43a551 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-split.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-split.t/base.opam b/test/blackbox-tests/test-cases/coq/native-split.t/base.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/native-split.t/dune b/test/blackbox-tests/test-cases/coq/native-split.t/dune new file mode 100644 index 000000000000..b53cf1eb0537 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-split.t/dune @@ -0,0 +1,3 @@ +(rule + (alias default) + (action (echo "%{read:base.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/native-split.t/dune-project b/test/blackbox-tests/test-cases/coq/native-split.t/dune-project new file mode 100644 index 000000000000..baf5b85ccb83 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-split.t/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.0) +(using coq 0.5) diff --git a/test/blackbox-tests/test-cases/coq/native-split.t/foo/dune b/test/blackbox-tests/test-cases/coq/native-split.t/foo/dune new file mode 100644 index 000000000000..72c8061029f1 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-split.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-split.t/foo/foo.v b/test/blackbox-tests/test-cases/coq/native-split.t/foo/foo.v new file mode 100644 index 000000000000..53e0ce1b1526 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-split.t/foo/foo.v @@ -0,0 +1 @@ +Definition mynat := nat. diff --git a/test/blackbox-tests/test-cases/coq/native-split.t/run.t b/test/blackbox-tests/test-cases/coq/native-split.t/run.t new file mode 100644 index 000000000000..07c976a10baa --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/native-split.t/run.t @@ -0,0 +1,24 @@ + $ 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/foo.{glob,vo} + coqnative foo/Nfoo_foo.{cmi,cmxs} + coqc bar/.bar.aux,bar/bar.{glob,vo} + coqnative bar/Nbar_bar.{cmi,cmxs} + + $ 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"} + ]