diff --git a/CHANGES.md b/CHANGES.md index 5a0e8c09416e..83b03438c5b6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -38,6 +38,9 @@ Unreleased - Allow per-package `version` in generated `opam` files (#3287, @toots) +- [coq] Introduce the `coq.extraction` stanza. It can be used to extract OCaml + sources (#3299, fixes #2178, @rgrinberg) + 2.4.0 (06/03/2020) ------------------ diff --git a/doc/dune-files.rst b/doc/dune-files.rst index 911689be6ff6..e15665373d24 100644 --- a/doc/dune-files.rst +++ b/doc/dune-files.rst @@ -1635,6 +1635,31 @@ which for each ``g_mod`` in ```` is equivalent to: (deps (:mlg-file g_mod.mlg)) (action (run coqpp %{mlg-file}))) +coq.extraction +-------------- + +Coq may be instructed to *extract* OCaml sources as part of the compilation +process. This is done using the ``coq.extraction`` stanza: + +.. code:: lisp + + (coq.extraction + (prelude ) + (extracted_modules ) + ) + +- ``(prelude )`` refers to the coq source that contains the extraction + commands. + +- ``(extraced_modules )`` is an exhaustive list of OCaml modules + extracted. + +- ```` are ``flags``, ``theories``, and ``libraries``. All of + these fields have the same meaning as in the ``coq.theory`` stanza. + +The extracted sources can then be used in ``executable`` or ``library`` stanzas +as any other sources. + .. _dune-workspace: mdx (since 2.4) diff --git a/src/dune/build.ml b/src/dune/build.ml index 1695ea24ea2d..cbef90777d65 100644 --- a/src/dune/build.ml +++ b/src/dune/build.ml @@ -168,6 +168,8 @@ module With_targets = struct ; targets : Path.Build.Set.t } + let map_build t ~f = { t with build = f t.build } + let return x = { build = Pure x; targets = Path.Build.Set.empty } let add t ~targets = diff --git a/src/dune/build.mli b/src/dune/build.mli index 2a3693d891b1..d98f110202dc 100644 --- a/src/dune/build.mli +++ b/src/dune/build.mli @@ -6,11 +6,15 @@ open! Import type 'a t module With_targets : sig + type 'a build + type nonrec 'a t = { build : 'a t ; targets : Path.Build.Set.t } + val map_build : 'a t -> f:('a build -> 'b build) -> 'b t + val return : 'a -> 'a t val add : 'a t -> targets:Path.Build.t list -> 'a t @@ -38,6 +42,7 @@ module With_targets : sig val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t end end +with type 'a build := 'a t (** This function should be called before analysing build expressions using [static_deps], [lib_deps] or [exec], which all require some file system diff --git a/src/dune/coq_lib.ml b/src/dune/coq_lib.ml index 4bf8e55a80ef..9ff752947140 100644 --- a/src/dune/coq_lib.ml +++ b/src/dune/coq_lib.ml @@ -38,7 +38,7 @@ module Error = struct Error (User_error.E (User_error.make ?loc ?hints paragraphs)) let duplicate_theory_name theory = - let loc, name = theory.Dune_file.Coq.name in + let loc, name = theory.Coq_stanza.Theory.name in let name = Coq_lib_name.to_string name in make ~loc [ Pp.textf "Duplicate theory name: %s" name ] @@ -56,7 +56,9 @@ module Error = struct ] let duplicate_boot_lib ~loc boot_theory = - let name = Coq_lib_name.to_string (snd boot_theory.Dune_file.Coq.name) in + let name = + Coq_lib_name.to_string (snd boot_theory.Coq_stanza.Theory.name) + in make ~loc [ Pp.textf "Cannot have more than one boot library: %s)" name ] let cycle_found ~loc cycle = @@ -77,15 +79,15 @@ module DB = struct let boot_library { boot; _ } = boot - let create_from_stanza ((dir, s) : Path.Build.t * Dune_file.Coq.t) = + let create_from_stanza ((dir, s) : Path.Build.t * Coq_stanza.Theory.t) = let name = snd s.name in ( name , { name = s.name ; wrapper = Coq_lib_name.wrapper name ; obj_root = dir ; src_root = dir - ; theories = s.theories - ; libraries = s.libraries + ; theories = s.buildable.theories + ; libraries = s.buildable.libraries ; package = s.package } ) @@ -98,11 +100,11 @@ module DB = struct Result.ok_exn (Error.duplicate_theory_name w2) in let boot = - match List.find_all ~f:(fun (_, s) -> s.Dune_file.Coq.boot) sl with + match List.find_all ~f:(fun (_, s) -> s.Coq_stanza.Theory.boot) sl with | [] -> None - | [ l ] -> Some ((snd l).loc, snd (create_from_stanza l)) + | [ l ] -> Some ((snd l).buildable.loc, snd (create_from_stanza l)) | _ :: (_, s2) :: _ -> - Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.loc s2) + Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.buildable.loc s2) in { boot; libs } @@ -119,26 +121,41 @@ module DB = struct module Coq_lib_closure = Top_closure.Make (String.Set) (Or_exn) - let requires db t : lib list Or_exn.t = - let theories = - match db.boot with - | None -> t.theories - (* XXX: Note that this means that we will prefix Coq with -Q, not sure we - want to do that (yet), but seems like good practice. *) - | Some (loc, stdlib) -> (loc, snd stdlib.name) :: t.theories - in + let add_boot db theories = + match db.boot with + | None -> theories + (* XXX: Note that this means that we will prefix Coq with -Q, not sure we + want to do that (yet), but seems like good practice. *) + | Some (loc, stdlib) -> (loc, snd stdlib.name) :: theories + + let top_closure db theories ~allow_private_deps ~loc = let open Result.O in - let allow_private_deps = Option.is_none t.package in let* theories = - Result.List.map ~f:(resolve ~allow_private_deps db) theories + add_boot db theories + |> Result.List.map ~f:(resolve ~allow_private_deps db) in - let key t = Coq_lib_name.to_string (snd t.name) in - let deps t = + let key (t : lib) = Coq_lib_name.to_string (snd t.name) in + let deps (t : lib) = Result.List.map ~f:(resolve ~allow_private_deps db) t.theories in - Result.bind (Coq_lib_closure.top_closure theories ~key ~deps) ~f:(function - | Ok libs -> Ok libs - | Error cycle -> Error.cycle_found ~loc:(location t) cycle) + match Coq_lib_closure.top_closure theories ~key ~deps with + | Ok (Ok s) -> Ok s + | Ok (Error cycle) -> Error.cycle_found ~loc cycle + | Error exn -> Error exn + + let requires db (t : lib) : lib list Or_exn.t = + let allow_private_deps = Option.is_none t.package in + let loc = location t in + top_closure db t.theories ~loc ~allow_private_deps + + let requires_for_user_written db = function + | [] -> Ok [] + | start :: xs as theories -> + let loc = + let stop = Option.value (List.last xs) ~default:start in + Loc.span (fst start) (fst stop) + in + top_closure db theories ~loc ~allow_private_deps:true let resolve db l = resolve db l end diff --git a/src/dune/coq_lib.mli b/src/dune/coq_lib.mli index 9dea478c0e7c..8e38a65056cd 100644 --- a/src/dune/coq_lib.mli +++ b/src/dune/coq_lib.mli @@ -25,7 +25,8 @@ module DB : sig type t - val create_from_coqlib_stanzas : (Path.Build.t * Dune_file.Coq.t) list -> t + val create_from_coqlib_stanzas : + (Path.Build.t * Coq_stanza.Theory.t) list -> t val find_many : t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Or_exn.t @@ -35,5 +36,8 @@ module DB : sig (** Return the list of dependencies needed for compiling this library *) val requires : t -> lib -> lib list Or_exn.t + + val requires_for_user_written : + t -> (Loc.t * Coq_lib_name.t) list -> lib list Or_exn.t end with type lib := t diff --git a/src/dune/coq_module.ml b/src/dune/coq_module.ml index 1b8fe2194654..2b2597c015dc 100644 --- a/src/dune/coq_module.ml +++ b/src/dune/coq_module.ml @@ -11,7 +11,11 @@ module Name = struct let compare = String.compare + let equal = String.equal + let to_dyn s = Dyn.String s + + let to_string s = s end (* We keep prefix and name separated as the handling of `From Foo Require Bar.` diff --git a/src/dune/coq_module.mli b/src/dune/coq_module.mli index 47aebf0c8888..46dde433b46f 100644 --- a/src/dune/coq_module.mli +++ b/src/dune/coq_module.mli @@ -11,7 +11,11 @@ module Name : sig val compare : t -> t -> Ordering.t + val equal : t -> t -> bool + val to_dyn : t -> Dyn.t + + val to_string : t -> string end type t @@ -30,7 +34,7 @@ val source : t -> Path.Build.t val prefix : t -> string list -val name : t -> string +val name : t -> Name.t val dep_file : obj_dir:Path.Build.t -> t -> Path.Build.t diff --git a/src/dune/coq_rules.ml b/src/dune/coq_rules.ml index 3ccd99738833..bfacfd5ab584 100644 --- a/src/dune/coq_rules.ml +++ b/src/dune/coq_rules.ml @@ -4,6 +4,7 @@ (* Written by: Emilio Jesús Gallego Arias *) open! Stdune +open Coq_stanza module SC = Super_context let coq_debug = false @@ -34,33 +35,154 @@ module Util = struct List.concat_map plugins ~f:to_mlpack end -type coq_context = - { coqdep : Action.program - ; coqc : Action.program - ; coqpp : Action.program - } +let resolve_program sctx ~loc ~dir prog = + SC.resolve_program ~dir sctx prog ~loc:(Some loc) + ~hint:"try: opam install coq" + +module Bootstrap = struct + (* the internal boot flag determines if the Coq "standard library" is being + built, in case we need to explictly tell Coq where the build artifacts are + and add `Init.Prelude.vo` as a dependency; there is a further special case + when compiling the prelude, in this case we also need to tell Coq not to + try to load the prelude. *) + type t = + | No_boot (** Coq's stdlib is installed globally *) + | Bootstrap of Coq_lib.t + (** Coq's stdlib is in scope of the composed build *) + | Bootstrap_prelude + (** We are compiling the prelude itself + [should be replaced with (per_file ...) flags] *) + + let get ~boot_lib ~wrapper_name coq_module = + match boot_lib with + | None -> No_boot + | Some (_loc, lib) -> ( + (* This is here as an optimization, TODO; replace with per_file flags *) + let init = + String.equal (Coq_lib.wrapper lib) wrapper_name + && Option.equal String.equal + (List.hd_opt (Coq_module.prefix coq_module)) + (Some "Init") + in + match init with + | false -> Bootstrap lib + | true -> Bootstrap_prelude ) + + let flags = + let open Command in + function + | No_boot -> [] + | Bootstrap _lib -> [ Args.A "-boot" ] + | Bootstrap_prelude -> [ Args.As [ "-boot"; "-noinit" ] ] +end + +(* get_libraries from Coq's ML dependencies *) +let libs_of_coq_deps ~lib_db = Result.List.map ~f:(Lib.DB.resolve lib_db) + +module Context = struct + type 'a t = + { coqdep : Action.program + ; coqc : Action.program * Path.Build.t + ; wrapper_name : string + ; dir : Path.Build.t + ; expander : Expander.t + ; buildable : Buildable.t + ; theories_deps : Coq_lib.t list Or_exn.t + ; mlpack_rule : unit Build.t + ; ml_flags : 'a Command.Args.t + ; scope : Scope.t + ; boot_type : Bootstrap.t + ; build_dir : Path.Build.t + } + + let coqc ?stdout_to t args = + let dir = Path.build (snd t.coqc) in + Command.run ~dir ?stdout_to (fst t.coqc) args + + let coq_flags t = + Expander.expand_and_eval_set t.expander t.buildable.flags + ~standard:(Build.return []) + + let theories_flags = + let setup_theory_flag lib = + let wrapper = Coq_lib.wrapper lib in + let dir = Coq_lib.src_root lib in + [ Command.Args.A "-Q"; Path (Path.build dir); A wrapper ] + in + fun t -> + Command.of_result_map t.theories_deps ~f:(fun libs -> + Command.Args.S (List.concat_map libs ~f:setup_theory_flag)) + + let coqc_file_flags cctx = + let file_flags = + [ cctx.ml_flags + ; theories_flags cctx + ; Command.Args.A "-R" + ; Path (Path.build cctx.dir) + ; A cctx.wrapper_name + ] + in + [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ] + + (* compute include flags and mlpack rules *) + let setup_ml_deps ~lib_db libs theories = + (* Pair of include flags and paths to mlpack *) + let libs = + let open Result.O in + let* theories = theories in + let libs = libs @ List.concat_map ~f:Coq_lib.libraries theories in + let* libs = libs_of_coq_deps ~lib_db libs in + Lib.closure ~linking:false libs + in + ( Command.of_result_map libs ~f:Util.include_flags + , Build.of_result_map libs ~f:(fun libs -> + (* 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 + (buildable : Buildable.t) = + let loc = buildable.loc in + let rr = resolve_program sctx ~dir ~loc in + let expander = Super_context.expander sctx ~dir in + let scope = SC.find_scope_by_dir sctx dir in + let lib_db = Scope.libs scope in + (* ML-level flags for depending libraries *) + let ml_flags, mlpack_rule = + setup_ml_deps ~lib_db buildable.libraries theories_deps + in + let build_dir = Super_context.build_dir sctx in + { coqdep = rr "coqdep" + ; coqc = (rr "coqc", coqc_dir) + ; wrapper_name + ; dir + ; expander + ; buildable + ; theories_deps + ; mlpack_rule + ; ml_flags + ; scope + ; boot_type = Bootstrap.No_boot + ; build_dir + } + + let for_module t coq_module = + let boot_lib = t.scope |> Scope.coq_libs |> Coq_lib.DB.boot_library in + let boot_type = + Bootstrap.get ~boot_lib ~wrapper_name:t.wrapper_name coq_module + in + { t with boot_type } +end -(* the internal boot flag determines if the Coq "standard library" is being - built, in case we need to explictly tell Coq where the build artifacts are - and add `Init.Prelude.vo` as a dependency; there is a further special case - when compiling the prelude, in this case we also need to tell Coq not to try - to load the prelude. *) -type coq_bootstrap_type = - | No_boot (** Coq's stdlib is installed globally *) - | Bootstrap of Coq_lib.t - (** Coq's stdlib is in scope of the composed build *) - | Bootstrap_prelude - (** We are compiling the prelude itself - [should be replaced with (per_file ...) flags] *) - -let parse_coqdep ~dir ~boot_type ~coq_module (lines : string list) = +let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module + (lines : string list) = if coq_debug then Format.eprintf "Parsing coqdep @\n%!"; let source = Coq_module.source coq_module in - let invalid p = + let invalid phase = User_error.raise [ Pp.textf "coqdep returned invalid output for %s / [phase: %s]" (Path.Build.to_string_maybe_quoted source) - p + phase + ; Pp.verbatim (String.concat ~sep:"\n" lines) ] in let line = @@ -80,7 +202,8 @@ let parse_coqdep ~dir ~boot_type ~coq_module (lines : string list) = let depname, _ = Filename.split_extension ff in let modname = String.concat ~sep:"/" - Coq_module.(prefix coq_module @ [ name coq_module ]) + Coq_module.( + prefix coq_module @ [ Coq_module.Name.to_string (name coq_module) ]) in if coq_debug then Format.eprintf "depname / modname: %s / %s@\n%!" depname modname; @@ -102,28 +225,6 @@ let parse_coqdep ~dir ~boot_type ~coq_module (lines : string list) = Path.relative (Path.build (Coq_lib.src_root lib)) "Init/Prelude.vo" :: deps ) -let get_bootstrap_type ~boot_lib ~wrapper_name coq_module = - match boot_lib with - | None -> No_boot - | Some (_loc, lib) -> ( - (* This is here as an optimization, TODO; replace with per_file flags *) - let init = - String.equal (Coq_lib.wrapper lib) wrapper_name - && Option.equal String.equal - (List.hd_opt (Coq_module.prefix coq_module)) - (Some "Init") - in - match init with - | false -> Bootstrap lib - | true -> Bootstrap_prelude ) - -let flags_of_bootstrap_type ~boot_type = - let open Command in - match boot_type with - | No_boot -> [] - | Bootstrap _lib -> [ Args.A "-boot" ] - | Bootstrap_prelude -> [ Args.As [ "-boot"; "-noinit" ] ] - let deps_of ~dir ~boot_type coq_module = let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in Build.dyn_paths_unit @@ -131,7 +232,7 @@ let deps_of ~dir ~boot_type coq_module = (Build.lines_of (Path.build stdout_to)) ~f:(parse_coqdep ~dir ~boot_type ~coq_module)) -let coqdep_rule ~dir ~coqdep ~mlpack_rule ~source_rule ~file_flags 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 :( *) let source = Coq_module.source coq_module in let file_flags = @@ -140,19 +241,17 @@ let coqdep_rule ~dir ~coqdep ~mlpack_rule ~source_rule ~file_flags coq_module = ; Dep (Path.build source) ] in - let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module 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 dir = Path.build dir in let open Build.With_targets.O in - Build.with_no_targets mlpack_rule + Build.with_no_targets cctx.mlpack_rule >>> Build.with_no_targets source_rule - >>> Command.run ~dir ~stdout_to coqdep file_flags + >>> Command.run ~dir:(Path.build cctx.dir) ~stdout_to cctx.coqdep file_flags -let coqc_rule ~build_dir ~expander ~dir ~coqc ~coq_flags ~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:dir coq_module in + let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module in [ Command.Args.Hidden_targets [ object_to ] ; S file_flags ; Command.Args.Dep (Path.build source) @@ -164,64 +263,34 @@ let coqc_rule ~build_dir ~expander ~dir ~coqc ~coq_flags ~file_flags coq_module Build.with_no_targets (Build.dep (Dep.sandbox_config Sandbox_config.no_sandboxing)) >>> - let coq_flags = - Expander.expand_and_eval_set expander coq_flags ~standard:(Build.return []) - in - let dir = Path.build build_dir in - Command.run ~dir coqc (Command.Args.dyn coq_flags :: file_flags) + let coq_flags = Context.coq_flags cctx in + Context.coqc cctx (Command.Args.dyn coq_flags :: file_flags) + +module Module_rule = struct + type t = + { coqdep : Action.t Build.With_targets.t + ; coqc : Action.t Build.With_targets.t + } +end -let setup_rule ~build_dir ~dir ~cc ~wrapper_name ~file_flags ~expander - ~coq_flags ~source_rule ~mlpack_rule ~boot_lib coq_module = +let setup_rule cctx ~source_rule coq_module = let open Build.With_targets.O in if coq_debug then Format.eprintf "gen_rule coq_module: %a@\n%!" Pp.render_ignore_tags (Dyn.pp (Coq_module.to_dyn coq_module)); - let boot_type = get_bootstrap_type ~boot_lib ~wrapper_name coq_module in - let file_flags = - [ Command.Args.S (flags_of_bootstrap_type ~boot_type); S file_flags ] - in + let file_flags = Context.coqc_file_flags cctx in - let coqdep_rule = - coqdep_rule ~dir ~coqdep:cc.coqdep ~mlpack_rule ~source_rule ~file_flags - coq_module - 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 ~boot_type coq_module in + let deps_of = deps_of ~dir:cctx.dir ~boot_type:cctx.boot_type coq_module in (* Rules for the files *) - [ coqdep_rule - ; Build.with_no_targets deps_of - >>> coqc_rule ~build_dir ~expander ~dir ~coqc:cc.coqc ~coq_flags ~file_flags - coq_module - ] - -(* TODO: remove; rgrinberg points out: - resolve program is actually cached, - - better just to ask for values that we actually use. *) -let create_ccoq sctx ~dir = - let rr prg = - SC.resolve_program ~dir sctx prg ~loc:None ~hint:"try: opam install coq" - in - { coqdep = rr "coqdep"; coqc = rr "coqc"; coqpp = rr "coqpp" } - -(* get_libraries from Coq's ML dependencies *) -let libs_of_coq_deps ~lib_db = Result.List.map ~f:(Lib.DB.resolve lib_db) - -(* compute include flags and mlpack rules *) -let setup_ml_deps ~lib_db libs theories = - (* Pair of include flags and paths to mlpack *) - let libs = - let open Result.O in - let* theories = theories in - let libs = libs @ List.concat_map ~f:Coq_lib.libraries theories in - let* libs = libs_of_coq_deps ~lib_db libs in - Lib.closure ~linking:false libs - in - ( Command.of_result_map libs ~f:Util.include_flags - , Build.of_result_map libs ~f:(fun libs -> - (* If the mlpack files don't exist, don't fail *) - Build.paths_existing (List.concat_map ~f:Util.ml_pack_files libs)) ) + { Module_rule.coqdep = coqdep_rule + ; coqc = + Build.with_no_targets deps_of >>> coqc_rule cctx ~file_flags coq_module + } let coq_modules_of_theory ~sctx lib = let name = Coq_lib.name lib in @@ -230,65 +299,46 @@ let coq_modules_of_theory ~sctx lib = let coq_sources = Dir_contents.coq dir_contents in Coq_sources.library coq_sources ~name -let setup_theory_flag lib = - let wrapper = Coq_lib.wrapper lib in - let dir = Coq_lib.src_root lib in - [ Command.Args.A "-Q"; Path (Path.build dir); A wrapper ] +let source_rule ~sctx theories = + (* sources for depending libraries coqdep requires all the files to be in the + tree to produce correct dependencies, including those of dependencies *) + Build.of_result_map theories ~f:(fun theories -> + List.concat_map theories ~f:(coq_modules_of_theory ~sctx) + |> List.rev_map ~f:(fun m -> Path.build (Coq_module.source m)) + |> Build.paths) -let setup_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coq.t) = - let cc = create_ccoq sctx ~dir in +let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) = let name = snd s.name in let scope = SC.find_scope_by_dir sctx dir in - let lib_db = Scope.libs scope in let coq_lib_db = Scope.coq_libs scope in - let expander = SC.expander sctx ~dir in - let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in - (* Coq flags for depending libraries *) - let theories_deps = Coq_lib.DB.requires coq_lib_db theory in - let theories_flags = - Command.of_result_map theories_deps ~f:(fun libs -> - Command.Args.S (List.concat_map libs ~f:setup_theory_flag)) - in - - (* sources for depending libraries coqdep requires all the files to be in the - tree to produce correct dependencies, including those of dependencies *) - let source_rule = - Build.of_result_map theories_deps ~f:(fun theories -> - theory :: theories - |> List.concat_map ~f:(coq_modules_of_theory ~sctx) - |> List.rev_map ~f:(fun m -> Path.build (Coq_module.source m)) - |> Build.paths) - in - - (* ML-level flags for depending libraries *) - let ml_flags, mlpack_rule = setup_ml_deps ~lib_db s.libraries theories_deps in - - (* Final flags *) - let wrapper_name = Coq_lib.wrapper theory in - let file_flags = - [ ml_flags - ; theories_flags - ; Command.Args.A "-R" - ; Path (Path.build dir) - ; A wrapper_name - ] + 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 coqc_dir = Super_context.build_dir sctx in + Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps s.buildable in - let boot_lib = Coq_lib.DB.boot_library coq_lib_db in - let coq_flags = s.flags 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 - List.concat_map coq_modules - ~f: - (setup_rule ~build_dir ~dir ~cc ~expander ~coq_flags ~source_rule - ~wrapper_name ~file_flags ~mlpack_rule ~boot_lib) + let source_rule = + let theories = + let open Result.O in + let+ theories = cctx.theories_deps in + theory :: theories + in + source_rule ~sctx theories + 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 ]) (******************************************************************************) (* Install rules *) @@ -296,9 +346,11 @@ let setup_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coq.t) = (* This is here for compatibility with Coq < 8.11, which expects plugin files to be in the folder containing the `.vo` files *) -let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Dune_file.Coq.t) = +let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) = let lib_db = Scope.libs scope in - let ml_libs = libs_of_coq_deps ~lib_db s.libraries |> Result.ok_exn in + let ml_libs = + libs_of_coq_deps ~lib_db s.buildable.libraries |> Result.ok_exn + in let rules_for_lib lib = (* Don't install libraries that don't belong to this package *) if @@ -324,8 +376,9 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Dune_file.Coq.t) = let install_rules ~sctx ~dir s = match s with - | { Dune_file.Coq.package = None; _ } -> [] - | { Dune_file.Coq.package = Some package; loc; _ } -> + | { Theory.package = None; _ } -> [] + | { Theory.package = Some package; _ } -> + 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 let name = snd s.name in @@ -362,12 +415,39 @@ let install_rules ~sctx ~dir s = vofile) )) |> List.rev_append coq_plugins_install_rules -let coqpp_rules ~sctx ~build_dir ~dir (s : Dune_file.Coqpp.t) = - let cc = create_ccoq sctx ~dir in +let coqpp_rules ~sctx ~dir (s : Coqpp.t) = + let coqpp = resolve_program sctx ~dir ~loc:s.loc "coqpp" in let mlg_rule m = let source = Path.build (Path.Build.relative dir (m ^ ".mlg")) in let target = Path.Build.relative dir (m ^ ".ml") in let args = [ Command.Args.Dep source; Hidden_targets [ target ] ] in - Command.run ~dir:(Path.build build_dir) cc.coqpp args + Command.run ~dir:(Path.build (Super_context.build_dir sctx)) coqpp args in List.map ~f:mlg_rule s.modules + +let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) = + 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 + Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories + in + Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps + s.buildable + in + let coq_module = + let coq = Dir_contents.coq dir_contents in + Coq_sources.extract coq s + in + let ml_targets = + Extraction.ml_target_fnames s |> List.map ~f:(Path.Build.relative dir) + in + let source_rule = + let theories = source_rule ~sctx cctx.theories_deps in + let open Build.O in + theories >>> Build.path (Path.build (Coq_module.source coq_module)) + in + let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule coq_module in + let coqc = Build.With_targets.add coqc ~targets:ml_targets in + [ coqdep; coqc ] diff --git a/src/dune/coq_rules.mli b/src/dune/coq_rules.mli index 84833a929e95..c04c18f0f319 100644 --- a/src/dune/coq_rules.mli +++ b/src/dune/coq_rules.mli @@ -5,24 +5,30 @@ (* Build rules for Coq's .v -> .vo files *) open! Stdune +open Coq_stanza val setup_rules : sctx:Super_context.t - -> build_dir:Path.Build.t -> dir:Path.Build.t -> dir_contents:Dir_contents.t - -> Dune_file.Coq.t + -> Theory.t -> Action.t Build.With_targets.t list val install_rules : sctx:Super_context.t -> dir:Path.Build.t - -> Dune_file.Coq.t + -> Theory.t -> (Loc.t option * Path.Build.t Install.Entry.t) list val coqpp_rules : sctx:Super_context.t - -> build_dir:Path.Build.t -> dir:Path.Build.t - -> Dune_file.Coqpp.t + -> Coqpp.t + -> Action.t Build.With_targets.t list + +val extraction_rules : + sctx:Super_context.t + -> dir:Path.Build.t + -> dir_contents:Dir_contents.t + -> Extraction.t -> Action.t Build.With_targets.t list diff --git a/src/dune/coq_sources.ml b/src/dune/coq_sources.ml index ab4de795f6e1..ee466cc33236 100644 --- a/src/dune/coq_sources.ml +++ b/src/dune/coq_sources.ml @@ -1,12 +1,16 @@ open Stdune +open Coq_stanza (* TODO: Build reverse map and check duplicates, however, are duplicates harmful? 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 } +type t = + { libraries : Coq_module.t list Coq_lib_name.Map.t + ; extract : Coq_module.t Loc.Map.t + } -let empty = { libraries = Coq_lib_name.Map.empty } +let empty = { libraries = Coq_lib_name.Map.empty; extract = Loc.Map.empty } let coq_modules_of_files ~dirs = let filter_v_files (dir, local, files) = @@ -24,14 +28,6 @@ let coq_modules_of_files ~dirs = in List.concat_map ~f:build_mod_dir dirs -let build_coq_modules_map (d : _ Dir_with_dune.t) ~dir ~modules = - List.fold_left d.data ~init:Coq_lib_name.Map.empty ~f:(fun map -> - function - | Dune_file.Coq.T coq -> - let modules = Coq_module.eval ~dir coq.modules ~standard:modules in - Coq_lib_name.Map.add_exn map (snd coq.name) modules - | _ -> map) - let library t ~name = Coq_lib_name.Map.find_exn t.libraries name let check_no_unqualified (loc, (qualif_mode : Dune_file.Include_subdirs.t)) = @@ -39,9 +35,34 @@ let check_no_unqualified (loc, (qualif_mode : Dune_file.Include_subdirs.t)) = User_error.raise ~loc [ Pp.text "(include_subdirs unqualified) is not supported yet" ] -let of_dir d ~include_subdirs ~dirs = +let extract t (stanza : Extraction.t) = + Loc.Map.find_exn t.extract stanza.buildable.loc + +let of_dir (d : _ Dir_with_dune.t) ~include_subdirs ~dirs = check_no_unqualified include_subdirs; - { libraries = - build_coq_modules_map d ~dir:d.ctx_dir - ~modules:(coq_modules_of_files ~dirs) - } + let modules = coq_modules_of_files ~dirs in + List.fold_left d.data ~init:empty ~f:(fun acc -> + function + | Coq_stanza.Theory.T coq -> + let modules = + Coq_module.eval ~dir:d.ctx_dir coq.modules ~standard:modules + in + let libraries = + Coq_lib_name.Map.add_exn acc.libraries (snd coq.name) modules + in + { acc with libraries } + | Coq_stanza.Extraction.T extract -> + let loc, prelude = extract.prelude in + let m = + match + List.find modules ~f:(fun m -> + Coq_module.Name.equal (Coq_module.name m) prelude) + with + | Some m -> m + | None -> + User_error.raise ~loc + [ Pp.text "no coq source corresponding to prelude field" ] + in + let extract = Loc.Map.add_exn acc.extract extract.buildable.loc m in + { acc with extract } + | _ -> acc) diff --git a/src/dune/coq_sources.mli b/src/dune/coq_sources.mli index e169074b64ac..14cc8e634004 100644 --- a/src/dune/coq_sources.mli +++ b/src/dune/coq_sources.mli @@ -8,6 +8,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 extract : t -> Coq_stanza.Extraction.t -> Coq_module.t + val of_dir : Stanza.t list Dir_with_dune.t -> include_subdirs:Loc.t * Dune_file.Include_subdirs.t diff --git a/src/dune/coq_stanza.ml b/src/dune/coq_stanza.ml new file mode 100644 index 000000000000..4e8f83e441c4 --- /dev/null +++ b/src/dune/coq_stanza.ml @@ -0,0 +1,163 @@ +open Import +open Dune_lang.Decoder +open Stanza_common + +module Coqpp = struct + type t = + { modules : string list + ; loc : Loc.t + } + + let decode = + fields + (let+ modules = field "modules" (repeat string) + and+ loc = loc in + { modules; loc }) + + type Stanza.t += T of t + + let p = ("coq.pp", decode >>| fun x -> [ T x ]) +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)) ] + +module Buildable = struct + type t = + { flags : Ordered_set_lang.Unexpanded.t + ; libraries : (Loc.t * Lib_name.t) list (** ocaml libraries *) + ; theories : (Loc.t * Coq_lib_name.t) list (** coq libraries *) + ; loc : Loc.t + } + + let decode = + let+ loc = loc + and+ flags = Ordered_set_lang.Unexpanded.field "flags" + and+ libraries = + field "libraries" (repeat (located Lib_name.decode)) ~default:[] + and+ theories = + field "theories" + (Dune_lang.Syntax.since coq_syntax (0, 2) >>> repeat Coq_lib_name.decode) + ~default:[] + in + { flags; libraries; theories; loc } +end + +module Extraction = struct + type t = + { (* not a list of modules because we want to preserve whatever case coq + uses *) + extracted_modules : string list + ; prelude : Loc.t * Coq_module.Name.t + ; buildable : Buildable.t + } + + let ml_target_fnames t = + List.concat_map t.extracted_modules ~f:(fun m -> [ m ^ ".ml"; m ^ ".mli" ]) + + let decode = + fields + (let+ extracted_modules = field "extracted_modules" (repeat string) + and+ prelude = + field "prelude" (located (string >>| Coq_module.Name.make)) + and+ buildable = Buildable.decode in + { prelude; extracted_modules; buildable }) + + type Stanza.t += T of t + + let p = ("coq.extraction", decode >>| fun x -> [ T x ]) +end + +module Theory = struct + type t = + { name : Loc.t * Coq_lib_name.t + ; package : Package.t option + ; project : Dune_project.t + ; synopsis : string option + ; modules : Ordered_set_lang.t + ; boot : bool + ; enabled_if : Blang.t + ; buildable : Buildable.t + } + + let coq_public_decode = + map_validate + (let+ project = Dune_project.get_exn () + and+ loc_name = + field_o "public_name" + (Dune_lang.Decoder.plain_string (fun ~loc s -> (loc, s))) + in + (project, loc_name)) + ~f:(fun (project, loc_name) -> + match loc_name with + | None -> Ok None + | Some (loc, name) -> + let pkg = + match String.lsplit2 ~on:'.' name with + | None -> Package.Name.of_string name + | Some (pkg, _) -> Package.Name.of_string pkg + in + Pkg.resolve project pkg |> Result.map ~f:(fun pkg -> Some (loc, pkg))) + + let select_deprecation ~package ~public = + match (package, public) with + | p, None -> p + | None, Some (loc, pkg) -> + User_warning.emit ~loc + [ Pp.text + "(public_name ...) is deprecated and will be removed in the Coq \ + language version 1.0, please use (package ...) instead" + ]; + Some pkg + | Some _, Some (loc, _) -> + User_error.raise ~loc + [ Pp.text + "Cannot both use (package ...) and (public_name ...), please \ + remove the latter as it is deprecated and will be removed in the \ + 1.0 version of the Coq language" + ] + + let decode = + fields + (let+ name = field "name" Coq_lib_name.decode + and+ package = field_o "package" Pkg.decode + and+ project = Dune_project.get_exn () + and+ public = coq_public_decode + and+ synopsis = field_o "synopsis" string + and+ boot = + field_b "boot" ~check:(Dune_lang.Syntax.since coq_syntax (0, 2)) + and+ modules = modules_field "modules" + and+ enabled_if = enabled_if ~since:None + and+ buildable = Buildable.decode in + let package = select_deprecation ~package ~public in + { name + ; package + ; project + ; synopsis + ; modules + ; boot + ; buildable + ; enabled_if + }) + + type Stanza.t += T of t + + let coqlib_warn x = + User_warning.emit ~loc:x.buildable.loc + [ Pp.text + "(coqlib ...) is deprecated and will be removed in the Coq language \ + version 1.0, please use (coq.theory ...) instead" + ]; + x + + let coqlib_p = ("coqlib", decode >>| fun x -> [ T (coqlib_warn x) ]) + + let p = ("coq.theory", decode >>| fun x -> [ T x ]) +end + +let unit_stanzas = + let+ r = return [ Theory.coqlib_p; Theory.p; Coqpp.p; Extraction.p ] in + ((), r) + +let key = Dune_project.Extension.register coq_syntax unit_stanzas Unit.to_dyn diff --git a/src/dune/coq_stanza.mli b/src/dune/coq_stanza.mli new file mode 100644 index 000000000000..af0a52874ebc --- /dev/null +++ b/src/dune/coq_stanza.mli @@ -0,0 +1,48 @@ +open Import + +module Buildable : sig + type t = + { flags : Ordered_set_lang.Unexpanded.t + ; libraries : (Loc.t * Lib_name.t) list (** ocaml libraries *) + ; theories : (Loc.t * Coq_lib_name.t) list (** coq libraries *) + ; loc : Loc.t + } +end + +module Extraction : sig + type t = + { extracted_modules : string list + ; prelude : Loc.t * Coq_module.Name.t + ; buildable : Buildable.t + } + + val ml_target_fnames : t -> string list + + type Stanza.t += T of t +end + +module Theory : sig + type t = + { name : Loc.t * Coq_lib_name.t + ; package : Package.t option + ; project : Dune_project.t + ; synopsis : string option + ; modules : Ordered_set_lang.t + ; boot : bool + ; enabled_if : Blang.t + ; buildable : Buildable.t + } + + type Stanza.t += T of t +end + +module Coqpp : sig + type t = + { modules : string list + ; loc : Loc.t + } + + type Stanza.t += T of t +end + +val key : unit Dune_project.Extension.t diff --git a/src/dune/dir_contents.ml b/src/dune/dir_contents.ml index a4798859e630..759783a9cbca 100644 --- a/src/dune/dir_contents.ml +++ b/src/dune/dir_contents.ml @@ -130,7 +130,10 @@ end = struct List.concat_map stanzas ~f:(fun stanza -> match (stanza : Stanza.t) with (* XXX What about mli files? *) - | Coqpp.T { modules; _ } -> List.map modules ~f:(fun m -> m ^ ".ml") + | Coq_stanza.Coqpp.T { modules; _ } -> + List.map modules ~f:(fun m -> m ^ ".ml") + | Coq_stanza.Extraction.T s -> + Coq_stanza.Extraction.ml_target_fnames s | Menhir.T menhir -> Menhir_rules.targets menhir | Rule rule -> Simple_rules.user_rule sctx rule ~dir ~expander diff --git a/src/dune/dune_file.ml b/src/dune/dune_file.ml index dcfe0a756f91..206a4d3cf564 100644 --- a/src/dune/dune_file.ml +++ b/src/dune/dune_file.ml @@ -1,6 +1,7 @@ open! Stdune open Import open Dune_lang.Decoder +open Stanza_common (* This file defines Dune types as well as the S-expression syntax for the various supported versions of the specification. *) @@ -34,103 +35,6 @@ let variants_field = (let* () = Dune_lang.Syntax.since library_variants (0, 1) in located (repeat Variant.decode >>| Variant.Set.of_list)) -(* Parse and resolve "package" fields *) -module Pkg = struct - let listing packages = - let longest_pkg = - String.longest_map packages ~f:(fun p -> - Package.Name.to_string p.Package.name) - in - Pp.enumerate packages ~f:(fun pkg -> - Printf.ksprintf Pp.verbatim "%-*s (because of %s)" longest_pkg - (Package.Name.to_string pkg.Package.name) - (Path.Source.to_string (Package.opam_file pkg))) - - let default (project : Dune_project.t) stanza = - match Package.Name.Map.values (Dune_project.packages project) with - | [ pkg ] -> Ok pkg - | [] -> - Error - (User_error.make - [ Pp.text - "The current project defines some public elements, but no opam \ - packages are defined." - ; Pp.text - "Please add a .opam file at the project root so that \ - these elements are installed into it." - ]) - | _ :: _ :: _ -> - Error - (User_error.make - [ Pp.text - "I can't determine automatically which package this stanza is \ - for." - ; Pp.text "I have the choice between these ones:" - ; listing (Package.Name.Map.values (Dune_project.packages project)) - ; Pp.textf - "You need to add a (package ...) field to this (%s) stanza." - stanza - ]) - - let default_exn ~loc project stanza = - match default project stanza with - | Ok p -> p - | Error msg -> raise (User_error.E { msg with loc = Some loc }) - - let resolve (project : Dune_project.t) name = - let packages = Dune_project.packages project in - match Package.Name.Map.find packages name with - | Some pkg -> Ok pkg - | None -> - let name_s = Package.Name.to_string name in - if Package.Name.Map.is_empty packages then - Error - (User_error.make - [ Pp.text - "You cannot declare items to be installed without adding a \ - .opam file at the root of your project." - ; Pp.textf - "To declare elements to be installed as part of package %S, \ - add a %S file at the root of your project." - name_s - (Package.Name.opam_fn name) - ; Pp.textf "Root of the project as discovered by dune: %s" - (Path.Source.to_string_maybe_quoted - (Dune_project.root project)) - ]) - else - Error - (User_error.make - [ Pp.textf "The current scope doesn't define package %S." name_s - ; Pp.text - "The only packages for which you can declare elements to be \ - installed in this directory are:" - ; listing (Package.Name.Map.values packages) - ] - ~hints: - (User_message.did_you_mean name_s - ~candidates: - ( Package.Name.Map.keys packages - |> List.map ~f:Package.Name.to_string ))) - - let decode = - let+ p = Dune_project.get_exn () - and+ loc, name = located Package.Name.decode in - match resolve p name with - | Ok x -> x - | Error e -> raise (User_error.E { e with loc = Some loc }) - - let field stanza = - map_validate - (let+ p = Dune_project.get_exn () - and+ pkg = field_o "package" string in - (p, pkg)) - ~f:(fun (p, pkg) -> - match pkg with - | None -> default p stanza - | Some name -> resolve p (Package.Name.of_string name)) -end - module Pps_and_flags = struct let decode = let+ l, flags = @@ -269,14 +173,6 @@ module Preprocess = struct @ [ String_with_vars.make_var loc "input-file" ] ) ) end -let enabled_if ~since = - let decode = - match since with - | None -> Blang.decode - | Some since -> Dune_lang.Syntax.since Stanza.syntax since >>> Blang.decode - in - field "enabled_if" ~default:Blang.true_ decode - module Per_module = struct include Module_name.Per_item @@ -415,8 +311,6 @@ module Lib_deps = struct |> Lib_name.Map.of_list_reduce ~f:Lib_deps_info.Kind.merge end -let modules_field name = Ordered_set_lang.field name - let preprocess_fields = let+ preprocess = field "preprocess" Preprocess_map.decode ~default:Preprocess_map.default @@ -1961,132 +1855,6 @@ module Menhir = struct (return [ ("menhir", decode >>| fun x -> [ T x ]) ]) end -module Coqpp = struct - type t = - { modules : string list - ; loc : Loc.t - } - - let decode = - fields - (let+ modules = field "modules" (repeat string) - and+ loc = loc in - { modules; loc }) - - type Stanza.t += T of t -end - -module Coq = struct - type t = - { name : Loc.t * Coq_lib_name.t - ; package : Package.t option - ; project : Dune_project.t - ; synopsis : string option - ; modules : Ordered_set_lang.t - ; flags : Ordered_set_lang.Unexpanded.t - ; boot : bool - ; libraries : (Loc.t * Lib_name.t) list (** ocaml libraries *) - ; theories : (Loc.t * Coq_lib_name.t) list (** coq libraries *) - ; loc : Loc.t - ; enabled_if : Blang.t - } - - let syntax = - Dune_lang.Syntax.create ~name:"coq" ~desc:"the coq extension (experimental)" - [ ((0, 1), `Since (1, 9)); ((0, 2), `Since (2, 5)) ] - - let coq_public_decode = - map_validate - (let+ project = Dune_project.get_exn () - and+ loc_name = - field_o "public_name" - (Dune_lang.Decoder.plain_string (fun ~loc s -> (loc, s))) - in - (project, loc_name)) - ~f:(fun (project, loc_name) -> - match loc_name with - | None -> Ok None - | Some (loc, name) -> - let pkg = - match String.lsplit2 ~on:'.' name with - | None -> Package.Name.of_string name - | Some (pkg, _) -> Package.Name.of_string pkg - in - Pkg.resolve project pkg |> Result.map ~f:(fun pkg -> Some (loc, pkg))) - - let select_deprecation ~package ~public = - match (package, public) with - | p, None -> p - | None, Some (loc, pkg) -> - User_warning.emit ~loc - [ Pp.text - "(public_name ...) is deprecated and will be removed in the Coq \ - language version 1.0, please use (package ...) instead" - ]; - Some pkg - | Some _, Some (loc, _) -> - User_error.raise ~loc - [ Pp.text - "Cannot both use (package ...) and (public_name ...), please \ - remove the latter as it is deprecated and will be removed in the \ - 1.0 version of the Coq language" - ] - - let decode = - fields - (let+ name = field "name" Coq_lib_name.decode - and+ loc = loc - and+ package = field_o "package" Pkg.decode - and+ project = Dune_project.get_exn () - and+ public = coq_public_decode - and+ synopsis = field_o "synopsis" string - and+ flags = Ordered_set_lang.Unexpanded.field "flags" - and+ boot = field_b "boot" ~check:(Dune_lang.Syntax.since syntax (0, 2)) - and+ modules = modules_field "modules" - and+ libraries = - field "libraries" (repeat (located Lib_name.decode)) ~default:[] - and+ theories = - field "theories" - (Dune_lang.Syntax.since syntax (0, 2) >>> repeat Coq_lib_name.decode) - ~default:[] - and+ enabled_if = enabled_if ~since:None in - let package = select_deprecation ~package ~public in - { name - ; package - ; project - ; synopsis - ; modules - ; flags - ; boot - ; libraries - ; theories - ; loc - ; enabled_if - }) - - type Stanza.t += T of t - - let coqlib_warn x = - User_warning.emit ~loc:x.loc - [ Pp.text - "(coqlib ...) is deprecated and will be removed in the Coq language \ - version 1.0, please use (coq.theory ...) instead" - ]; - x - - let coqlib_p = ("coqlib", decode >>| fun x -> [ T (coqlib_warn x) ]) - - let coqtheory_p = ("coq.theory", decode >>| fun x -> [ T x ]) - - let coqpp_p = ("coq.pp", Coqpp.(decode >>| fun x -> [ T x ])) - - let unit_stanzas = - let+ r = return [ coqlib_p; coqtheory_p; coqpp_p ] in - ((), r) - - let key = Dune_project.Extension.register syntax unit_stanzas Unit.to_dyn -end - module Alias_conf = struct type t = { name : Alias.Name.t @@ -2382,7 +2150,8 @@ module Stanzas = struct let+ () = Dune_lang.Syntax.since Stanza.syntax (1, 1) and+ t = let enable_qualified = - Option.is_some (Dune_project.find_extension_args project Coq.key) + Option.is_some + (Dune_project.find_extension_args project Coq_stanza.key) in Include_subdirs.decode ~enable_qualified and+ loc = loc in @@ -2484,5 +2253,5 @@ let stanza_package = function | Documentation { package; _ } | Tests { package = Some package; _ } -> Some package - | Coq.T { package = Some package; _ } -> Some package + | Coq_stanza.Theory.T { package = Some package; _ } -> Some package | _ -> None diff --git a/src/dune/dune_file.mli b/src/dune/dune_file.mli index ddb859bf01d8..3ff06cbb26d8 100644 --- a/src/dune/dune_file.mli +++ b/src/dune/dune_file.mli @@ -351,33 +351,6 @@ module Rule : sig } end -module Coq : sig - type t = - { name : Loc.t * Coq_lib_name.t - ; package : Package.t option - ; project : Dune_project.t - ; synopsis : string option - ; modules : Ordered_set_lang.t - ; flags : Ordered_set_lang.Unexpanded.t - ; boot : bool - ; libraries : (Loc.t * Lib_name.t) list (** ocaml libraries *) - ; theories : (Loc.t * Coq_lib_name.t) list (** coq libraries *) - ; loc : Loc.t - ; enabled_if : Blang.t - } - - type Stanza.t += T of t -end - -module Coqpp : sig - type t = - { modules : string list - ; loc : Loc.t - } - - type Stanza.t += T of t -end - module Alias_conf : sig type t = { name : Alias.Name.t diff --git a/src/dune/gen_rules.ml b/src/dune/gen_rules.ml index b3e3bcebad1e..898fb7717ab3 100644 --- a/src/dune/gen_rules.ml +++ b/src/dune/gen_rules.ml @@ -249,7 +249,6 @@ let gen_rules sctx dir_contents cctxs in Merlin.add_rules sctx ~dir:ctx_dir ~more_src_dirs ~expander (Merlin.add_source_dir m src_dir)); - let build_dir = Super_context.build_dir sctx in List.iter stanzas ~f:(fun stanza -> match (stanza : Stanza.t) with | Menhir.T m when Expander.eval_blang expander m.enabled_if -> ( @@ -278,12 +277,15 @@ let gen_rules sctx dir_contents cctxs ]) } |> Build.with_targets ~targets ) - | Some cctx -> Menhir_rules.gen_rules cctx m ~build_dir ~dir:ctx_dir ) - | Coq.T m when Expander.eval_blang expander m.enabled_if -> - Coq_rules.setup_rules ~sctx ~build_dir ~dir:ctx_dir ~dir_contents m + | Some cctx -> Menhir_rules.gen_rules cctx m ~dir:ctx_dir ) + | Coq_stanza.Theory.T m when Expander.eval_blang expander m.enabled_if -> + Coq_rules.setup_rules ~sctx ~dir:ctx_dir ~dir_contents m |> Super_context.add_rules ~dir:ctx_dir sctx - | Coqpp.T m -> - Coq_rules.coqpp_rules ~sctx ~build_dir ~dir:ctx_dir m + | Coq_stanza.Extraction.T m -> + Coq_rules.extraction_rules ~sctx ~dir:ctx_dir ~dir_contents m + |> Super_context.add_rules ~dir:ctx_dir sctx + | Coq_stanza.Coqpp.T m -> + Coq_rules.coqpp_rules ~sctx ~dir:ctx_dir m |> Super_context.add_rules ~dir:ctx_dir sctx | _ -> ()); define_all_alias ~dir:ctx_dir ~scope ~js_targets; diff --git a/src/dune/install_rules.ml b/src/dune/install_rules.ml index 1a3de53dbeff..5dae3fd2d3ea 100644 --- a/src/dune/install_rules.ml +++ b/src/dune/install_rules.ml @@ -163,7 +163,7 @@ end = struct ~variants:exes.variants ~optional:exes.optional in Result.is_ok (Lib.Compile.direct_requires compile_info) ) - | Dune_file.Coq.T d -> Option.is_some d.package + | Coq_stanza.Theory.T d -> Option.is_some d.package | _ -> false ) stanza @@ -259,7 +259,7 @@ end = struct let sub_dir = (Option.value_exn lib.public).sub_dir in let dir_contents = Dir_contents.get sctx ~dir in lib_install_files sctx ~scope ~dir ~sub_dir lib ~dir_contents - | Dune_file.Coq.T coqlib -> + | Coq_stanza.Theory.T coqlib -> Coq_rules.install_rules ~sctx ~dir coqlib | Dune_file.Documentation d -> let dc = Dir_contents.get sctx ~dir in diff --git a/src/dune/lib.ml b/src/dune/lib.ml index be0ef1505408..41a1eb1b03a6 100644 --- a/src/dune/lib.ml +++ b/src/dune/lib.ml @@ -1365,7 +1365,7 @@ end = struct let (last, _) : Loc.t * _ = Option.value (List.last others) ~default:first in - { (fst first) with stop = last.stop } + Loc.span (fst first) last in let pps = let* pps = diff --git a/src/dune/menhir.ml b/src/dune/menhir.ml index d4ec32e995b8..6d1e2e058145 100644 --- a/src/dune/menhir.ml +++ b/src/dune/menhir.ml @@ -37,10 +37,6 @@ module type PARAMS = sig of the form [_build//src], e.g., [_build/default/src]. *) val dir : Path.Build.t - (* [build_dir] is the base directory of the context; we run menhir from this - directoy to we get correct error paths. *) - val build_dir : Path.Build.t - (* [stanza] is the [(menhir ...)] stanza, as found in the [dune] file. *) val stanza : stanza @@ -58,6 +54,10 @@ module Run (P : PARAMS) : sig end = struct let sctx = Compilation_context.super_context cctx + (* [build_dir] is the base directory of the context; we run menhir from this + directoy to we get correct error paths. *) + let build_dir = Super_context.build_dir sctx + let expander = Compilation_context.expander cctx (* ------------------------------------------------------------------------ *) @@ -288,14 +288,12 @@ let module_names (stanza : Dune_file.Menhir.t) : Module_name.t list = (* TODO the loc can improved here *) Module_name.of_string_allow_invalid (stanza.loc, s)) -let gen_rules ~build_dir ~dir cctx stanza = +let gen_rules ~dir cctx stanza = let module R = Run (struct let cctx = cctx let dir = dir - let build_dir = build_dir - let stanza = stanza end) in () diff --git a/src/dune/menhir.mli b/src/dune/menhir.mli index cb7a36d89b59..814bc036c4ec 100644 --- a/src/dune/menhir.mli +++ b/src/dune/menhir.mli @@ -12,8 +12,4 @@ val module_names : Dune_file.Menhir.t -> Module_name.t list (** Generate the rules for a [(menhir ...)] stanza. *) val gen_rules : - build_dir:Path.Build.t - -> dir:Path.Build.t - -> Compilation_context.t - -> Dune_file.Menhir.t - -> unit + dir:Path.Build.t -> Compilation_context.t -> Dune_file.Menhir.t -> unit diff --git a/src/dune/scope.ml b/src/dune/scope.ml index 14d7d2b758d1..d5ce4b430863 100644 --- a/src/dune/scope.ml +++ b/src/dune/scope.ml @@ -122,7 +122,7 @@ module DB = struct in let coq_stanzas_by_project_dir = List.map coq_stanzas ~f:(fun (dir, t) -> - let project = t.Dune_file.Coq.project in + let project = t.Coq_stanza.Theory.project in (Dune_project.root project, (dir, t))) |> Path.Source.Map.of_list_multi in @@ -185,7 +185,7 @@ module DB = struct (External_variant ev :: acc, coq_acc) | Dune_file.Deprecated_library_name d -> (Deprecated_library_name d :: acc, coq_acc) - | Dune_file.Coq.T coq_lib -> + | Coq_stanza.Theory.T coq_lib -> let ctx_dir = Path.Build.append_source context.build_dir dune_file.dir in diff --git a/src/dune/stanza_common.ml b/src/dune/stanza_common.ml new file mode 100644 index 000000000000..b9bdb39cf190 --- /dev/null +++ b/src/dune/stanza_common.ml @@ -0,0 +1,109 @@ +open Import +open Dune_lang.Decoder + +(* Parse and resolve "package" fields *) +module Pkg = struct + let listing packages = + let longest_pkg = + String.longest_map packages ~f:(fun p -> + Package.Name.to_string p.Package.name) + in + Pp.enumerate packages ~f:(fun pkg -> + Printf.ksprintf Pp.verbatim "%-*s (because of %s)" longest_pkg + (Package.Name.to_string pkg.Package.name) + (Path.Source.to_string (Package.opam_file pkg))) + + let default (project : Dune_project.t) stanza = + match Package.Name.Map.values (Dune_project.packages project) with + | [ pkg ] -> Ok pkg + | [] -> + Error + (User_error.make + [ Pp.text + "The current project defines some public elements, but no opam \ + packages are defined." + ; Pp.text + "Please add a .opam file at the project root so that \ + these elements are installed into it." + ]) + | _ :: _ :: _ -> + Error + (User_error.make + [ Pp.text + "I can't determine automatically which package this stanza is \ + for." + ; Pp.text "I have the choice between these ones:" + ; listing (Package.Name.Map.values (Dune_project.packages project)) + ; Pp.textf + "You need to add a (package ...) field to this (%s) stanza." + stanza + ]) + + let default_exn ~loc project stanza = + match default project stanza with + | Ok p -> p + | Error msg -> raise (User_error.E { msg with loc = Some loc }) + + let resolve (project : Dune_project.t) name = + let packages = Dune_project.packages project in + match Package.Name.Map.find packages name with + | Some pkg -> Ok pkg + | None -> + let name_s = Package.Name.to_string name in + if Package.Name.Map.is_empty packages then + Error + (User_error.make + [ Pp.text + "You cannot declare items to be installed without adding a \ + .opam file at the root of your project." + ; Pp.textf + "To declare elements to be installed as part of package %S, \ + add a %S file at the root of your project." + name_s + (Package.Name.opam_fn name) + ; Pp.textf "Root of the project as discovered by dune: %s" + (Path.Source.to_string_maybe_quoted + (Dune_project.root project)) + ]) + else + Error + (User_error.make + [ Pp.textf "The current scope doesn't define package %S." name_s + ; Pp.text + "The only packages for which you can declare elements to be \ + installed in this directory are:" + ; listing (Package.Name.Map.values packages) + ] + ~hints: + (User_message.did_you_mean name_s + ~candidates: + ( Package.Name.Map.keys packages + |> List.map ~f:Package.Name.to_string ))) + + let decode = + let+ p = Dune_project.get_exn () + and+ loc, name = located Package.Name.decode in + match resolve p name with + | Ok x -> x + | Error e -> raise (User_error.E { e with loc = Some loc }) + + let field stanza = + map_validate + (let+ p = Dune_project.get_exn () + and+ pkg = field_o "package" string in + (p, pkg)) + ~f:(fun (p, pkg) -> + match pkg with + | None -> default p stanza + | Some name -> resolve p (Package.Name.of_string name)) +end + +let modules_field name = Ordered_set_lang.field name + +let enabled_if ~since = + let decode = + match since with + | None -> Blang.decode + | Some since -> Dune_lang.Syntax.since Stanza.syntax since >>> Blang.decode + in + field "enabled_if" ~default:Blang.true_ decode diff --git a/src/dune/stanza_common.mli b/src/dune/stanza_common.mli new file mode 100644 index 000000000000..3c18017c7c13 --- /dev/null +++ b/src/dune/stanza_common.mli @@ -0,0 +1,18 @@ +open Import + +module Pkg : sig + val decode : Package.t Dune_lang.Decoder.t + + val resolve : + Dune_project.t -> Package.Name.t -> (Package.t, User_message.t) Result.t + + val field : string -> Package.t Dune_lang.Decoder.fields_parser + + val default_exn : loc:Loc.t -> Dune_project.t -> string -> Package.t +end + +val modules_field : string -> Ordered_set_lang.t Dune_lang.Decoder.fields_parser + +val enabled_if : + since:Dune_lang.Syntax.Version.t option + -> Blang.t Dune_lang.Decoder.fields_parser diff --git a/src/stdune/loc.ml b/src/stdune/loc.ml index 3c4b09344d55..efabd5ca8769 100644 --- a/src/stdune/loc.ml +++ b/src/stdune/loc.ml @@ -1,5 +1,15 @@ include Loc0 +module O = Comparable.Make (struct + type nonrec t = t + + let compare = Poly.compare + + let to_dyn = to_dyn +end) + +include O + let in_file p = let pos = none_pos (Path.to_string p) in { start = pos; stop = pos } @@ -126,3 +136,5 @@ let on_same_line loc1 loc2 = let same_file = String.equal start1.pos_fname start2.pos_fname in let same_line = Int.equal start1.pos_lnum start2.pos_lnum in same_file && same_line + +let span begin_ end_ = { begin_ with stop = end_.stop } diff --git a/src/stdune/loc.mli b/src/stdune/loc.mli index 6dc1b93bb99b..1277b6396f3c 100644 --- a/src/stdune/loc.mli +++ b/src/stdune/loc.mli @@ -2,6 +2,8 @@ include module type of struct include Loc0 end +module Map : Map_intf.S with type key := t + val in_file : Path.t -> t val in_dir : Path.t -> t @@ -30,3 +32,5 @@ val pp_file_colon_line : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit val on_same_line : t -> t -> bool + +val span : t -> t -> t diff --git a/test/blackbox-tests/dune.inc b/test/blackbox-tests/dune.inc index 90f3b35e5fe2..7bc8ebb47a36 100644 --- a/test/blackbox-tests/dune.inc +++ b/test/blackbox-tests/dune.inc @@ -134,6 +134,14 @@ test-cases/coq (progn (run dune-cram run run.t) (diff? run.t run.t.corrected))))) +(rule + (alias coq-extract) + (deps (package dune) (source_tree test-cases/coq/extract)) + (action + (chdir + test-cases/coq/extract + (progn (run dune-cram run run.t) (diff? run.t run.t.corrected))))) + (rule (alias corrections) (deps (package dune) (source_tree test-cases/corrections)) @@ -2957,4 +2965,4 @@ (alias (name runtest-js) (deps (alias explicit_js_mode) (alias js_of_ocaml))) -(alias (name runtest-coq) (deps (alias coq))) \ No newline at end of file +(alias (name runtest-coq) (deps (alias coq) (alias coq-extract))) \ No newline at end of file diff --git a/test/blackbox-tests/gen_tests.ml b/test/blackbox-tests/gen_tests.ml index 7aff8fb21c30..8d8a9f254037 100644 --- a/test/blackbox-tests/gen_tests.ml +++ b/test/blackbox-tests/gen_tests.ml @@ -199,6 +199,7 @@ let exclusions = [ make "js_of_ocaml" ~external_deps:true ~js:true ~env:("NODE", Sexp.parse "%{bin:node}") ; make "coq" ~coq:true + ; make "coq/extract" ~coq:true ; make "github25" ~env:("OCAMLPATH", Dune_lang.atom "./findlib-packages") ; odoc "odoc-simple" ; odoc "odoc-package-mld-link" diff --git a/test/blackbox-tests/test-cases/coq/extract/run.t b/test/blackbox-tests/test-cases/coq/extract/run.t new file mode 100644 index 000000000000..427e383d39ea --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/extract/run.t @@ -0,0 +1,49 @@ + $ cat >dune-project < (lang dune 2.5) + > (using coq 0.2) + + $ cat >extract.v < Definition nb (b : bool) : bool := + > match b with + > | false => true + > | true => false + > end. + > + > Require Extraction. + > Separate Extraction nb. + > EOF + + $ cat >dune < (coq.extraction + > (prelude extract) + > (extracted_modules Datatypes extract)) + > + > (executable + > (name foo)) + > EOF + + $ cat >foo.ml < open Datatypes + > let () = + > print_endline ( + > match Extract.nb Datatypes.Coq_true with + > | Coq_true -> "true" + > | Coq_false -> "false" + > ) + > EOF + + $ dune exec ./foo.exe + false + $ ls _build/default + Datatypes.ml + Datatypes.mli + extract.glob + extract.ml + extract.mli + extract.v + extract.v.d + extract.vo + extract.vok + extract.vos + foo.exe + foo.ml