diff --git a/CHANGES.md b/CHANGES.md index 8430d503c55..1861f2191f3 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -13,6 +13,9 @@ Unreleased - Delay expansion errors until the rule is used to build something (#3261, fix #3252, @rgrinberg, @diml) +- [coq] Support for theory dependencies and compositional builds using + new field `(theories ...)` (#2053, @ejgallego, @rgrinberg) + 2.4.0 (06/03/2020) ------------------ diff --git a/doc/dune-files.rst b/doc/dune-files.rst index 62f18450d6d..fb7cc62447c 100644 --- a/doc/dune-files.rst +++ b/doc/dune-files.rst @@ -1548,7 +1548,8 @@ The basic form for defining Coq libraries is very similar to the OCaml form: (synopsis ) (modules ) (libraries ) - (flags )) + (flags ) + (theories )) The stanza will build all ``.v`` files on the given directory. The semantics of fields is: @@ -1580,6 +1581,15 @@ The stanza will build all ``.v`` files on the given directory. The semantics of - the path to installed locations of ```` will be passed to ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq theory to depend on a ML plugin, +- your Coq theory can depend on other theories by specifying them in + the ```` field. Dune will then pass to Coq the + corresponding flags for everything to compile correctly [ ``-Q`` + ]. As of today, we only support composition with libraries defined + in the same scope (that is to say, under the same ``dune-project`` + domain). We will lift this restriction in the future. Note that + composition with the Coq's standard library is supported, but in + this case the ``Coq`` prefix will be made available in a qualified + way. Recursive qualification of modules ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1598,11 +1608,11 @@ Coq style for sub-directories. For example, file ``A/b/C.v`` will be module Limitations ~~~~~~~~~~~ -- composition and scoping of Coq libraries is still not possible. For now, - libraries are located using Coq's built-in library management, -- ``.v`` files always depend on the native version of a plugin, -- a ``foo.mlpack`` file must the present for locally defined plugins to work, - this is a limitation of coqdep. +- ``.v`` files always depend on the native version of Coq / plugins, +- a ``foo.mlpack`` file must the present in directories of locally + defined plugins for things to work, this is a limitation of + ``coqdep``, see the template at + coq.pp ------ diff --git a/src/dune/coq_lib.ml b/src/dune/coq_lib.ml new file mode 100644 index 00000000000..4bf8e55a80e --- /dev/null +++ b/src/dune/coq_lib.ml @@ -0,0 +1,144 @@ +(* This file is licensed under The MIT License *) +(* (c) MINES ParisTech 2018-2019 *) +(* Written by: Emilio Jesús Gallego Arias *) + +open! Stdune + +(* At some point we may want to reify this into resolved status, for example: + + ; libraries : Lib.t list Or_exn.t + + etc.. *) +type t = + { name : Loc.t * Coq_lib_name.t + ; wrapper : string + ; src_root : Path.Build.t + ; obj_root : Path.Build.t + ; theories : (Loc.t * Coq_lib_name.t) list + ; libraries : (Loc.t * Lib_name.t) list + ; package : Package.t option + } + +let name l = snd l.name + +let location l = fst l.name + +let wrapper l = l.wrapper + +let src_root l = l.src_root + +let obj_root l = l.obj_root + +let libraries l = l.libraries + +let package l = l.package + +module Error = struct + let make ?loc ?hints paragraphs = + 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 name = Coq_lib_name.to_string name in + make ~loc [ Pp.textf "Duplicate theory name: %s" name ] + + let theory_not_found ~loc name = + let name = Coq_lib_name.to_string name in + make ~loc [ Pp.textf "Theory %s not found" name ] + + let private_deps_not_allowed ~loc private_dep = + let name = Coq_lib_name.to_string (name private_dep) in + make ~loc + [ Pp.textf + "Theory %S is private, it cannot be a dependency of a public theory. \ + You need to associate %S to a package." + name name + ] + + let duplicate_boot_lib ~loc boot_theory = + let name = Coq_lib_name.to_string (snd boot_theory.Dune_file.Coq.name) in + make ~loc [ Pp.textf "Cannot have more than one boot library: %s)" name ] + + let cycle_found ~loc cycle = + make ~loc + [ Pp.textf "Cycle found" + ; Pp.enumerate cycle ~f:(fun t -> + Pp.text (Coq_lib_name.to_string (snd t.name))) + ] +end + +module DB = struct + type lib = t + + type nonrec t = + { boot : (Loc.t * t) option + ; libs : t Coq_lib_name.Map.t + } + + let boot_library { boot; _ } = boot + + let create_from_stanza ((dir, s) : Path.Build.t * Dune_file.Coq.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 + ; package = s.package + } ) + + (* Should we register errors and printers, or raise is OK? *) + let create_from_coqlib_stanzas sl = + let libs = + match Coq_lib_name.Map.of_list_map ~f:create_from_stanza sl with + | Ok m -> m + | Error (_name, _w1, (_, w2)) -> + 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 + | [] -> None + | [ l ] -> Some ((snd l).loc, snd (create_from_stanza l)) + | _ :: (_, s2) :: _ -> + Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.loc s2) + in + { boot; libs } + + let resolve ?(allow_private_deps = true) db (loc, name) = + match Coq_lib_name.Map.find db.libs name with + | Some s -> + if (not allow_private_deps) && Option.is_none s.package then + Error.private_deps_not_allowed ~loc s + else + Ok s + | None -> Error.theory_not_found ~loc name + + let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name)) + + 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 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 + in + let key t = Coq_lib_name.to_string (snd t.name) in + let deps t = + 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) + + let resolve db l = resolve db l +end diff --git a/src/dune/coq_lib.mli b/src/dune/coq_lib.mli new file mode 100644 index 00000000000..9dea478c0e7 --- /dev/null +++ b/src/dune/coq_lib.mli @@ -0,0 +1,39 @@ +(* This file is licensed under The MIT License *) +(* (c) MINES ParisTech 2018-2019 *) +(* Written by: Emilio Jesús Gallego Arias *) + +open! Stdune + +type t + +val name : t -> Coq_lib_name.t + +(* this is not really a wrapper for the prefix path *) +val wrapper : t -> string + +(** ml libraries *) +val libraries : t -> (Loc.t * Lib_name.t) list + +val src_root : t -> Path.Build.t + +val obj_root : t -> Path.Build.t + +val package : t -> Package.t option + +module DB : sig + type lib + + type t + + val create_from_coqlib_stanzas : (Path.Build.t * Dune_file.Coq.t) list -> t + + val find_many : t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Or_exn.t + + val boot_library : t -> (Loc.t * lib) option + + val resolve : t -> Loc.t * Coq_lib_name.t -> lib Or_exn.t + + (** Return the list of dependencies needed for compiling this library *) + val requires : t -> lib -> lib list Or_exn.t +end +with type lib := t diff --git a/src/dune/coq_lib_name.ml b/src/dune/coq_lib_name.ml index f0f27b67a0a..174291ce84c 100644 --- a/src/dune/coq_lib_name.ml +++ b/src/dune/coq_lib_name.ml @@ -12,13 +12,16 @@ let to_string x = String.concat ~sep:"." x let wrapper x = to_string x +(* We should add some further validation to Coq library names; the rules in Coq + itself have been tweaked due to Unicode, etc... so this is not trivial *) let decode : (Loc.t * t) Dune_lang.Decoder.t = Dune_lang.Decoder.plain_string (fun ~loc s -> (loc, String.split ~on:'.' s)) let encode : t Dune_lang.Encoder.t = fun lib -> Dune_lang.Encoder.string (to_string lib) -(* let pp x = Pp.text (to_string x) *) +let pp x = Pp.text (to_string x) + let to_dyn = Dyn.Encoder.(list string) module Rep = struct diff --git a/src/dune/coq_lib_name.mli b/src/dune/coq_lib_name.mli index db418fc8bf3..02aa4369cf7 100644 --- a/src/dune/coq_lib_name.mli +++ b/src/dune/coq_lib_name.mli @@ -16,7 +16,10 @@ val encode : t Dune_lang.Encoder.t val decode : (Loc.t * t) Dune_lang.Decoder.t (* to be removed in favor of encode / decode *) -(* val _pp : t -> Pp.t *) +val to_string : t -> string + +val pp : t -> t Pp.t + val to_dyn : t -> Dyn.t module Map : Map.S with type key = t diff --git a/src/dune/coq_rules.ml b/src/dune/coq_rules.ml index ade95955bbe..ea24adc4beb 100644 --- a/src/dune/coq_rules.ml +++ b/src/dune/coq_rules.ml @@ -1,5 +1,6 @@ (* 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 @@ -17,6 +18,21 @@ module Util = struct Path.Set.add acc src_dir) let include_flags ts = include_paths ts |> Lib.L.to_iflags + + (* coqdep expects an mlpack file next to the sources otherwise it + * will omit the cmxs deps *) + let ml_pack_files lib = + let plugins = + let info = Lib.info lib in + let plugins = Lib_info.plugins info in + Mode.Dict.get plugins Mode.Native + in + let to_mlpack file = + [ Path.set_extension file ~ext:".mlpack" + ; Path.set_extension file ~ext:".mllib" + ] + in + List.concat_map plugins ~f:to_mlpack end type coq_context = @@ -31,11 +47,14 @@ type coq_context = 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 - | Bootstrap + | 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 ~boot_type ~coq_module (lines : string list) = +let parse_coqdep ~dir ~boot_type ~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 = @@ -61,8 +80,8 @@ let parse_coqdep ~boot_type ~coq_module (lines : string list) = let ff = List.hd @@ String.extract_blank_separated_words basename in let depname, _ = Filename.split_extension ff in let modname = - Coq_module.( - String.concat ~sep:"/" (prefix coq_module @ [ name coq_module ])) + String.concat ~sep:"/" + Coq_module.(prefix coq_module @ [ name coq_module ]) in if coq_debug then Format.eprintf "depname / modname: %s / %s@\n%!" depname modname; @@ -74,31 +93,35 @@ let parse_coqdep ~boot_type ~coq_module (lines : string list) = 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 match boot_type with | No_boot | Bootstrap_prelude -> deps - | Bootstrap -> "Init/Prelude.vo" :: deps ) + | Bootstrap lib -> + Path.relative (Path.build (Coq_lib.src_root lib)) "Init/Prelude.vo" + :: deps ) -let get_bootstrap_type ~boot coq_module = - match boot with - | false -> No_boot - | true -> ( - (* This is inside as an optimization, TODO; replace with per_file flags *) +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 = - Option.equal String.equal - (List.nth_opt (Coq_module.prefix coq_module) 0) - (Some "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 + | false -> Bootstrap lib | true -> Bootstrap_prelude ) let flags_of_bootstrap_type ~boot_type = let open Command in match boot_type with | No_boot -> [] - | Bootstrap -> [ Args.A "-boot" ] + | Bootstrap _lib -> [ Args.A "-boot" ] | Bootstrap_prelude -> [ Args.As [ "-boot"; "-noinit" ] ] let deps_of ~dir ~boot_type coq_module = @@ -106,10 +129,7 @@ let deps_of ~dir ~boot_type coq_module = Build.dyn_paths_unit (Build.map (Build.lines_of (Path.build stdout_to)) - ~f:(fun x -> - List.map - ~f:(Path.relative (Path.build dir)) - (parse_coqdep ~boot_type ~coq_module x))) + ~f:(fun x -> parse_coqdep ~dir ~boot_type ~coq_module x)) let coqdep_rule ~dir ~coqdep ~mlpack_rule ~source_rule ~file_flags coq_module = (* coqdep needs the full source + plugin's mlpack to be present :( *) @@ -121,13 +141,15 @@ let coqdep_rule ~dir ~coqdep ~mlpack_rule ~source_rule ~file_flags coq_module = ] in let stdout_to = Coq_module.dep_file ~obj_dir: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 source_rule >>> Command.run ~dir ~stdout_to coqdep file_flags -let coqc_rule ~expander ~dir ~coqc ~coq_flags ~file_flags coq_module = +let coqc_rule ~build_dir ~expander ~dir ~coqc ~coq_flags ~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 @@ -145,17 +167,17 @@ let coqc_rule ~expander ~dir ~coqc ~coq_flags ~file_flags coq_module = let coq_flags = Expander.expand_and_eval_set expander coq_flags ~standard:(Build.return []) in - let dir = Path.build dir in + let dir = Path.build build_dir in Command.run ~dir coqc (Command.Args.dyn coq_flags :: file_flags) -let setup_rule ~expander ~dir ~cc ~source_rule ~coq_flags ~file_flags - ~mlpack_rule ~boot coq_module = +let setup_rule ~build_dir ~dir ~cc ~wrapper_name ~file_flags ~expander + ~coq_flags ~source_rule ~mlpack_rule ~boot_lib 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 coq_module in + 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 @@ -171,7 +193,8 @@ let setup_rule ~expander ~dir ~cc ~source_rule ~coq_flags ~file_flags (* Rules for the files *) [ coqdep_rule ; Build.with_no_targets deps_of - >>> coqc_rule ~expander ~dir ~coqc:cc.coqc ~coq_flags ~file_flags coq_module + >>> 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, - @@ -184,74 +207,100 @@ let create_ccoq sctx ~dir = (* get_libraries from Coq's ML dependencies *) let libs_of_coq_deps ~lib_db libs = - Result.List.map ~f:(Lib.DB.resolve lib_db) libs |> Result.ok_exn + Result.List.map ~f:(Lib.DB.resolve lib_db) libs (* compute include flags and mlpack rules *) -let setup_ml_deps ~lib_db libs = - (* coqdep expects an mlpack file next to the sources otherwise it - * will omit the cmxs deps *) - let ml_pack_files lib = - let plugins = - let info = Lib.info lib in - let plugins = Lib_info.plugins info in - Mode.Dict.get plugins Mode.Native - in - let to_mlpack file = - [ Path.set_extension file ~ext:".mlpack" - ; Path.set_extension file ~ext:".mllib" - ] - in - List.concat_map plugins ~f:to_mlpack - in +let setup_ml_deps ~lib_db libs theories = (* Pair of include flags and paths to mlpack *) - let ml_iflags, mlpack = - let libs = - libs_of_coq_deps ~lib_db libs - |> Lib.closure ~linking:false |> Result.ok_exn - in - (Util.include_flags libs, List.concat_map ~f:ml_pack_files libs) + 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 - (* If the mlpack files don't exist, don't fail *) - (ml_iflags, Build.paths_existing mlpack) + ( 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 coqlib_wrapper_name (s : Dune_file.Coq.t) = - Coq_lib_name.wrapper (snd s.name) +let coq_modules_of_theory ~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.library coq_sources ~name -let setup_rules ~sctx ~dir ~dir_contents (s : Dune_file.Coq.t) = - let scope = SC.find_scope_by_dir sctx dir in - let expander = SC.expander sctx ~dir in - if coq_debug then - Format.eprintf "[gen_rules] @[dir: %a@\nscope: %a@]@\n%!" Path.Build.pp dir - Path.Build.pp (Scope.root scope); +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 setup_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coq.t) = let cc = create_ccoq sctx ~dir in let name = snd s.name in - let coq_modules = - let coq = Dir_contents.coq dir_contents in - Coq_sources.library coq ~name + 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 - (* coqdep requires all the files to be in the tree to produce correct - dependencies *) + + (* 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.paths - (List.map coq_modules ~f:(fun m -> Path.build (Coq_module.source m))) + 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 + ] + in + + let boot_lib = Coq_lib.DB.boot_library coq_lib_db in let coq_flags = s.flags in - let wrapper_name = coqlib_wrapper_name s in - let lib_db = Scope.libs scope in - let ml_iflags, mlpack_rule = setup_ml_deps ~lib_db s.libraries in - let file_flags = [ ml_iflags; Command.Args.As [ "-R"; "."; wrapper_name ] ] in - let boot = s.boot 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 ~f: - (setup_rule ~expander ~dir ~cc ~source_rule ~coq_flags ~file_flags - ~mlpack_rule ~boot) + (setup_rule ~build_dir ~dir ~cc ~expander ~coq_flags ~source_rule + ~wrapper_name ~file_flags ~mlpack_rule ~boot_lib) coq_modules +(******************************************************************************) +(* Install rules *) +(******************************************************************************) + (* 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 lib_db = Scope.libs scope in - let ml_libs = libs_of_coq_deps ~lib_db s.libraries in + let ml_libs = libs_of_coq_deps ~lib_db s.libraries |> Result.ok_exn in let rules_for_lib lib = (* Don't install libraries that don't belong to this package *) if @@ -281,7 +330,7 @@ let install_rules ~sctx ~dir s = let dir_contents = Dir_contents.get sctx ~dir in let name = snd s.name in (* This must match the wrapper prefix for now to remain compatible *) - let dst_suffix = coqlib_wrapper_name s in + let dst_suffix = Coq_lib_name.wrapper (snd s.name) in (* These are the rules for now, coq lang 2.0 will make this uniform *) let dst_dir = if s.boot then @@ -291,6 +340,8 @@ let install_rules ~sctx ~dir s = let coq_root = Path.Local.of_string "coq/user-contrib" in Path.Local.relative coq_root dst_suffix in + (* Also, stdlib plugins are handled in a hardcoded way, so no compat install + is needed *) let coq_plugins_install_rules = if s.boot then [] diff --git a/src/dune/coq_rules.mli b/src/dune/coq_rules.mli index d8187be11e1..84833a929e9 100644 --- a/src/dune/coq_rules.mli +++ b/src/dune/coq_rules.mli @@ -8,6 +8,7 @@ open! Stdune 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 diff --git a/src/dune/dune_file.ml b/src/dune/dune_file.ml index ec30adca34e..aa33fc36d8a 100644 --- a/src/dune/dune_file.ml +++ b/src/dune/dune_file.ml @@ -1979,11 +1979,13 @@ 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 } @@ -2034,6 +2036,7 @@ module Coq = struct (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" @@ -2042,15 +2045,18 @@ module Coq = struct and+ modules = modules_field "modules" and+ libraries = field "libraries" (repeat (located Lib_name.decode)) ~default:[] + and+ theories = field "theories" (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 }) diff --git a/src/dune/dune_file.mli b/src/dune/dune_file.mli index b44a40f2649..ac5a495f126 100644 --- a/src/dune/dune_file.mli +++ b/src/dune/dune_file.mli @@ -355,11 +355,13 @@ 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 } diff --git a/src/dune/gen_rules.ml b/src/dune/gen_rules.ml index bbd5629eeed..618e554beee 100644 --- a/src/dune/gen_rules.ml +++ b/src/dune/gen_rules.ml @@ -280,7 +280,7 @@ 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 ~dir:ctx_dir ~dir_contents m + Coq_rules.setup_rules ~sctx ~build_dir ~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 diff --git a/src/dune/lib.ml b/src/dune/lib.ml index be0ef150540..e99b4807454 100644 --- a/src/dune/lib.ml +++ b/src/dune/lib.ml @@ -1683,6 +1683,7 @@ module DB = struct | Library of Path.Build.t * Dune_file.Library.t | External_variant of Dune_file.External_variant.t | Deprecated_library_name of Dune_file.Deprecated_library_name.t + | Coq_theory of Path.Build.t * Dune_file.Coq.t end module Found_or_redirect = struct @@ -1696,7 +1697,8 @@ module DB = struct List.iter stanzas ~f:(fun (stanza : Library_related_stanza.t) -> match stanza with | Library _ - | Deprecated_library_name _ -> + | Deprecated_library_name _ + | Coq_theory _ -> () | External_variant ev -> ( let loc, virtual_lib = ev.virtual_lib in @@ -1814,7 +1816,10 @@ module DB = struct else [ (name, Found info) ; (Lib_name.of_local conf.name, Redirect p.name) - ] )) + ] ) + | Coq_theory _ -> + (* As of today Coq theories do live in a separate namespace *) + []) |> Lib_name.Map.of_list_reducei ~f:(fun name (v1 : Found_or_redirect.t) v2 -> let res = diff --git a/src/dune/lib.mli b/src/dune/lib.mli index 7d71e1b8f03..96959767cb1 100644 --- a/src/dune/lib.mli +++ b/src/dune/lib.mli @@ -185,6 +185,7 @@ module DB : sig | Library of Path.Build.t * Dune_file.Library.t | External_variant of Dune_file.External_variant.t | Deprecated_library_name of Dune_file.Deprecated_library_name.t + | Coq_theory of Path.Build.t * Dune_file.Coq.t end (** Create a database from a list of library/variants stanzas *) diff --git a/src/dune/scope.ml b/src/dune/scope.ml index 04ba953a1ab..79968a630b3 100644 --- a/src/dune/scope.ml +++ b/src/dune/scope.ml @@ -4,6 +4,7 @@ open Import type t = { project : Dune_project.t ; db : Lib.DB.t + ; coq_db : Coq_lib.DB.t ; root : Path.Build.t } @@ -15,6 +16,8 @@ let project t = t.project let libs t = t.db +let coq_libs t = t.coq_db + module DB = struct type scope = t @@ -68,7 +71,11 @@ module DB = struct ; _ } -> Some - (Dune_file.Public_lib.name old_public_name, Name new_public_name)) + (Dune_file.Public_lib.name old_public_name, Name new_public_name) + | Coq_theory _ -> + (* All libraries in Coq are private to a scope for now, we will lift + this restriction soon *) + None) |> Lib_name.Map.of_list |> function | Ok x -> x @@ -112,6 +119,7 @@ module DB = struct | Library (_, lib) -> lib.project | External_variant ev -> ev.project | Deprecated_library_name x -> x.project + | Coq_theory (_, thr) -> thr.project in (Dune_project.root project, stanza)) |> Path.Source.Map.of_list_multi @@ -123,10 +131,16 @@ module DB = struct let db = Lib.DB.create_from_stanzas stanzas ~parent:public_libs ~lib_config in + let coq_stanzas = + List.filter_map stanzas ~f:(function + | Coq_theory (p, l) -> Some (p, l) + | _ -> None) + in + let coq_db = Coq_lib.DB.create_from_coqlib_stanzas coq_stanzas in let root = Path.Build.append_source build_context_dir (Dune_project.root project) in - Some { project; db; root }) + Some { project; db; coq_db; root }) let create ~projects ~context ~installed_libs ~lib_config stanzas = let t = Fdecl.create Dyn.Encoder.opaque in diff --git a/src/dune/scope.mli b/src/dune/scope.mli index cb3bb1dc151..f752262983d 100644 --- a/src/dune/scope.mli +++ b/src/dune/scope.mli @@ -15,6 +15,8 @@ val project : t -> Dune_project.t (** Return the library database associated to this scope *) val libs : t -> Lib.DB.t +val coq_libs : t -> Coq_lib.DB.t + (** Scope databases *) module DB : sig type scope = t diff --git a/src/dune/super_context.ml b/src/dune/super_context.ml index e23f79d3e12..cf9508fd0c7 100644 --- a/src/dune/super_context.ml +++ b/src/dune/super_context.ml @@ -441,6 +441,11 @@ let create ~(context : Context.t) ?host ~projects ~packages ~stanzas | Dune_file.External_variant ev -> External_variant ev :: acc | Dune_file.Deprecated_library_name d -> Deprecated_library_name d :: acc + | Dune_file.Coq.T coq_lib -> + let ctx_dir = + Path.Build.append_source context.build_dir dune_file.dir + in + Coq_theory (ctx_dir, coq_lib) :: acc | _ -> acc) in Scope.DB.create ~projects ~context:context.name ~installed_libs ~lib_config diff --git a/src/stdune/list.ml b/src/stdune/list.ml index ef3a5e0350c..7d8d982b8ef 100644 --- a/src/stdune/list.ml +++ b/src/stdune/list.ml @@ -39,6 +39,11 @@ let filteri l ~f = let concat_map l ~f = concat (map l ~f) +let rec rev_map_append l1 l2 ~f = + match l1 with + | [] -> l2 + | a :: l -> rev_map_append l (f a :: l2) ~f + let rev_partition_map = let rec loop l accl accr ~f = match l with diff --git a/src/stdune/list.mli b/src/stdune/list.mli index 0508d8a7f2c..ef8a6494992 100644 --- a/src/stdune/list.mli +++ b/src/stdune/list.mli @@ -20,6 +20,8 @@ val concat_map : 'a t -> f:('a -> 'b t) -> 'b t val partition_map : 'a t -> f:('a -> ('b, 'c) Either.t) -> 'b t * 'c t +val rev_map_append : 'a t -> 'b t -> f:('a -> 'b) -> 'b t + val rev_partition_map : 'a t -> f:('a -> ('b, 'c) Either.t) -> 'b t * 'c t type ('a, 'b) skip_or_either = diff --git a/src/stdune/monad.ml b/src/stdune/monad.ml index 3fba673b122..3fdb46702d6 100644 --- a/src/stdune/monad.ml +++ b/src/stdune/monad.ml @@ -1,7 +1,22 @@ -module Id = struct +module Make (M : Monad_intf.S1_base) = struct + include M + + module O = struct + let ( let+ ) x f = M.( >>= ) x (fun x -> M.return (f x)) + + let ( and+ ) x y = + let open M in + x >>= fun x -> + y >>= fun y -> return (x, y) + + let ( let* ) = M.( >>= ) + end +end + +module Id = Make (struct type 'a t = 'a let return x = x let ( >>= ) x f = f x -end +end) diff --git a/src/stdune/monad.mli b/src/stdune/monad.mli index 516c8ae518c..559b4bd8bac 100644 --- a/src/stdune/monad.mli +++ b/src/stdune/monad.mli @@ -1,3 +1,5 @@ (** Monad signatures *) -module Id : Monad_intf.S with type 'a t = 'a +module Make (M : Monad_intf.S1_base) : Monad_intf.S1 with type 'a t := 'a M.t + +module Id : Monad_intf.S1 with type 'a t = 'a diff --git a/src/stdune/monad_intf.ml b/src/stdune/monad_intf.ml index c825d0f1c85..596d2049109 100644 --- a/src/stdune/monad_intf.ml +++ b/src/stdune/monad_intf.ml @@ -1,7 +1,19 @@ -module type S = sig +module type S1_base = sig type 'a t val return : 'a -> 'a t val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t end + +module type S1 = sig + include S1_base + + module O : sig + val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t + + val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t + + val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t + end +end diff --git a/src/stdune/or_exn.ml b/src/stdune/or_exn.ml index 4c16fb2cb64..0065972e87a 100644 --- a/src/stdune/or_exn.ml +++ b/src/stdune/or_exn.ml @@ -1,7 +1,15 @@ -type 'a t = ('a, exn) Result.t - let equal eq x y = Result.equal eq Exn.equal x y let hash h = Result.hash h Exn.hash let to_dyn f = Result.to_dyn f Exn.to_dyn + +type 'a t = ('a, exn) Result.t + +include Monad.Make (struct + type nonrec 'a t = 'a t + + let return = Result.return + + let ( >>= ) = Result.( >>= ) +end) diff --git a/src/stdune/or_exn.mli b/src/stdune/or_exn.mli index 99989ed46b2..c0008c3a865 100644 --- a/src/stdune/or_exn.mli +++ b/src/stdune/or_exn.mli @@ -7,3 +7,5 @@ val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool val hash : ('a -> int) -> 'a t -> int val to_dyn : ('a -> Dyn.t) -> 'a t Dyn.Encoder.t + +include Monad_intf.S1 with type 'a t := 'a t diff --git a/src/stdune/result.ml b/src/stdune/result.ml index 9056ea3c116..4c61bebe850 100644 --- a/src/stdune/result.ml +++ b/src/stdune/result.ml @@ -4,6 +4,8 @@ type ('a, 'error) t = ('a, 'error) result = let ok x = Ok x +let return = ok + let is_ok = function | Ok _ -> true | Error _ -> false @@ -26,6 +28,8 @@ let bind t ~f = | Ok x -> f x | Error _ as t -> t +let ( >>= ) x f = bind x ~f + let map x ~f = match x with | Ok x -> Ok (f x) diff --git a/src/stdune/result.mli b/src/stdune/result.mli index d590a9c6323..41fa8e60d84 100644 --- a/src/stdune/result.mli +++ b/src/stdune/result.mli @@ -4,6 +4,8 @@ type ('a, 'error) t = ('a, 'error) result = | Ok of 'a | Error of 'error +val return : 'a -> ('a, _) t + val ok : 'a -> ('a, _) t val is_ok : _ t -> bool @@ -37,6 +39,8 @@ val map : ('a, 'error) t -> f:('a -> 'b) -> ('b, 'error) t val bind : ('a, 'error) t -> f:('a -> ('b, 'error) t) -> ('b, 'error) t +val ( >>= ) : ('a, 'error) t -> ('a -> ('b, 'error) t) -> ('b, 'error) t + val map_error : ('a, 'error1) t -> f:('error1 -> 'error2) -> ('a, 'error2) t val to_option : ('a, 'error) t -> 'a option diff --git a/src/stdune/top_closure.ml b/src/stdune/top_closure.ml index bd1756038df..49c59303082 100644 --- a/src/stdune/top_closure.ml +++ b/src/stdune/top_closure.ml @@ -1,4 +1,4 @@ -module Make (Keys : Top_closure_intf.Keys) (Monad : Monad_intf.S) = struct +module Make (Keys : Top_closure_intf.Keys) (Monad : Monad_intf.S1) = struct open Monad let top_closure ~key ~deps elements = diff --git a/src/stdune/top_closure.mli b/src/stdune/top_closure.mli index 00fb09355c5..b5a7e53c141 100644 --- a/src/stdune/top_closure.mli +++ b/src/stdune/top_closure.mli @@ -4,6 +4,6 @@ module Int : module String : Top_closure_intf.S with type key := string and type 'a monad := 'a Monad.Id.t -module Make (Keys : Top_closure_intf.Keys) (Monad : Monad_intf.S) : +module Make (Keys : Top_closure_intf.Keys) (Monad : Monad_intf.S1) : Top_closure_intf.S with type key := Keys.elt and type 'a monad := 'a Monad.t [@@inlined always] diff --git a/test/blackbox-tests/test-cases/coq/compose_boot/boot/Init/Prelude.v b/test/blackbox-tests/test-cases/coq/compose_boot/boot/Init/Prelude.v new file mode 100644 index 00000000000..eaaf0e55b2c --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_boot/boot/Init/Prelude.v @@ -0,0 +1 @@ +Definition id := forall (X : Type), X. diff --git a/test/blackbox-tests/test-cases/coq/compose_boot/boot/dune b/test/blackbox-tests/test-cases/coq/compose_boot/boot/dune new file mode 100644 index 00000000000..cb370c83b61 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_boot/boot/dune @@ -0,0 +1,7 @@ +(coq.theory + (name Coq) + (package cboot) + (boot)) + +(include_subdirs qualified) + diff --git a/test/blackbox-tests/test-cases/coq/compose_boot/cboot.opam b/test/blackbox-tests/test-cases/coq/compose_boot/cboot.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose_boot/dune b/test/blackbox-tests/test-cases/coq/compose_boot/dune new file mode 100644 index 00000000000..32d3fd98271 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_boot/dune @@ -0,0 +1,3 @@ +(rule + (alias default) + (action (echo "%{read:cboot.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose_boot/dune-project b/test/blackbox-tests/test-cases/coq/compose_boot/dune-project new file mode 100644 index 00000000000..c1fd9ec6785 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_boot/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/compose_boot/user/dune b/test/blackbox-tests/test-cases/coq/compose_boot/user/dune new file mode 100644 index 00000000000..5402df7cc24 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_boot/user/dune @@ -0,0 +1,5 @@ +(coq.theory + (name user) + (package cboot)) + + diff --git a/test/blackbox-tests/test-cases/coq/compose_boot/user/user.v b/test/blackbox-tests/test-cases/coq/compose_boot/user/user.v new file mode 100644 index 00000000000..cdda78d422b --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_boot/user/user.v @@ -0,0 +1 @@ +Definition a := id. diff --git a/test/blackbox-tests/test-cases/coq/compose_cycle/a/a.v b/test/blackbox-tests/test-cases/coq/compose_cycle/a/a.v new file mode 100644 index 00000000000..d4389c6d37d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_cycle/a/a.v @@ -0,0 +1 @@ +Definition foo := 3. diff --git a/test/blackbox-tests/test-cases/coq/compose_cycle/a/dune b/test/blackbox-tests/test-cases/coq/compose_cycle/a/dune new file mode 100644 index 00000000000..478550e0985 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_cycle/a/dune @@ -0,0 +1,4 @@ +(coq.theory + (name a) + (package ccycle) + (theories b)) diff --git a/test/blackbox-tests/test-cases/coq/compose_cycle/b/b.v b/test/blackbox-tests/test-cases/coq/compose_cycle/b/b.v new file mode 100644 index 00000000000..e184683b4d4 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_cycle/b/b.v @@ -0,0 +1,3 @@ +From a Require Import a. + +Definition bar := a.foo. diff --git a/test/blackbox-tests/test-cases/coq/compose_cycle/b/dune b/test/blackbox-tests/test-cases/coq/compose_cycle/b/dune new file mode 100644 index 00000000000..5f42b4087e9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_cycle/b/dune @@ -0,0 +1,4 @@ +(coq.theory + (name b) + (package ccycle) + (theories a)) diff --git a/test/blackbox-tests/test-cases/coq/compose_cycle/ccycle.opam b/test/blackbox-tests/test-cases/coq/compose_cycle/ccycle.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose_cycle/dune b/test/blackbox-tests/test-cases/coq/compose_cycle/dune new file mode 100644 index 00000000000..e622b2ade9e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_cycle/dune @@ -0,0 +1,3 @@ +(rule + (alias default) + (action (echo "%{read:ccycle.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose_cycle/dune-project b/test/blackbox-tests/test-cases/coq/compose_cycle/dune-project new file mode 100644 index 00000000000..c1fd9ec6785 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_cycle/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/cplugin.opam b/test/blackbox-tests/test-cases/coq/compose_plugin/cplugin.opam new file mode 100644 index 00000000000..8d1c8b69c3f --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/cplugin.opam @@ -0,0 +1 @@ + diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/dune b/test/blackbox-tests/test-cases/coq/compose_plugin/dune new file mode 100644 index 00000000000..d6032cc01e2 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/dune @@ -0,0 +1,3 @@ +(rule + (alias default) + (action (echo "%{read:cplugin.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/dune-project b/test/blackbox-tests/test-cases/coq/compose_plugin/dune-project new file mode 100644 index 00000000000..c1fd9ec6785 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/dune b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/dune new file mode 100644 index 00000000000..268e6ede624 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/dune @@ -0,0 +1,7 @@ +(library + (public_name cplugin.ml_plugin_a) + (name ml_plugin_a) + (flags :standard -rectypes) + (libraries coq.plugins.ltac)) + +(coq.pp (modules gram)) diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/gram.mlg b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/gram.mlg new file mode 100644 index 00000000000..80481ac4631 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/gram.mlg @@ -0,0 +1,9 @@ +DECLARE PLUGIN "gram" + +{ + +(* We don't use any coqpp specific macros as to make the test more + resilient on different Coq versions *) +let foo = 3 + +} diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/gram.mli b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/gram.mli new file mode 100644 index 00000000000..bcc533d2e62 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/gram.mli @@ -0,0 +1 @@ +val foo : int diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/ml_plugin_a.mlpack b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/ml_plugin_a.mlpack new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/simple.ml b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/simple.ml new file mode 100644 index 00000000000..555166169c9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/src_a/simple.ml @@ -0,0 +1,2 @@ +let a = 3 +let _ = a diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/src_b/dune b/test/blackbox-tests/test-cases/coq/compose_plugin/src_b/dune new file mode 100644 index 00000000000..a636d09f518 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/src_b/dune @@ -0,0 +1,5 @@ +(library + (public_name cplugin.ml_plugin_b) + (name ml_plugin_b) + (flags :standard -rectypes) + (libraries ml_plugin_a)) diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/src_b/ml_plugin_b.mlpack b/test/blackbox-tests/test-cases/coq/compose_plugin/src_b/ml_plugin_b.mlpack new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/src_b/simple_b.ml b/test/blackbox-tests/test-cases/coq/compose_plugin/src_b/simple_b.ml new file mode 100644 index 00000000000..04ea5df11e8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/src_b/simple_b.ml @@ -0,0 +1 @@ +let _ = Ml_plugin_a.Simple.a diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/thy1/a.v b/test/blackbox-tests/test-cases/coq/compose_plugin/thy1/a.v new file mode 100644 index 00000000000..340c0d8abb5 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/thy1/a.v @@ -0,0 +1,3 @@ +Declare ML Module "ml_plugin_a". +Declare ML Module "ml_plugin_b". + diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/thy1/dune b/test/blackbox-tests/test-cases/coq/compose_plugin/thy1/dune new file mode 100644 index 00000000000..c3e194a70ff --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/thy1/dune @@ -0,0 +1,6 @@ +(coq.theory + (name thy1) + (package cplugin) + (synopsis "Test Plugin") + (libraries cplugin.ml_plugin_b) + (modules :standard)) diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/thy2/a.v b/test/blackbox-tests/test-cases/coq/compose_plugin/thy2/a.v new file mode 100644 index 00000000000..340c0d8abb5 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/thy2/a.v @@ -0,0 +1,3 @@ +Declare ML Module "ml_plugin_a". +Declare ML Module "ml_plugin_b". + diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/thy2/dune b/test/blackbox-tests/test-cases/coq/compose_plugin/thy2/dune new file mode 100644 index 00000000000..3646943458b --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/thy2/dune @@ -0,0 +1,6 @@ +(coq.theory + (name thy2) + (package cplugin) + (synopsis "Test Plugin") + (theories thy1)) + diff --git a/test/blackbox-tests/test-cases/coq/compose_simple/a/a.v b/test/blackbox-tests/test-cases/coq/compose_simple/a/a.v new file mode 100644 index 00000000000..d4389c6d37d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_simple/a/a.v @@ -0,0 +1 @@ +Definition foo := 3. diff --git a/test/blackbox-tests/test-cases/coq/compose_simple/a/dune b/test/blackbox-tests/test-cases/coq/compose_simple/a/dune new file mode 100644 index 00000000000..099b8f56a24 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_simple/a/dune @@ -0,0 +1,3 @@ +(coq.theory + (name a) + (package csimple)) diff --git a/test/blackbox-tests/test-cases/coq/compose_simple/b/b.v b/test/blackbox-tests/test-cases/coq/compose_simple/b/b.v new file mode 100644 index 00000000000..e184683b4d4 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_simple/b/b.v @@ -0,0 +1,3 @@ +From a Require Import a. + +Definition bar := a.foo. diff --git a/test/blackbox-tests/test-cases/coq/compose_simple/b/dune b/test/blackbox-tests/test-cases/coq/compose_simple/b/dune new file mode 100644 index 00000000000..e4edf23190e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_simple/b/dune @@ -0,0 +1,4 @@ +(coq.theory + (name b) + (package csimple) + (theories a)) diff --git a/test/blackbox-tests/test-cases/coq/compose_simple/csimple.opam b/test/blackbox-tests/test-cases/coq/compose_simple/csimple.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose_simple/dune b/test/blackbox-tests/test-cases/coq/compose_simple/dune new file mode 100644 index 00000000000..f7a7db897db --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_simple/dune @@ -0,0 +1,3 @@ +(rule + (alias default) + (action (echo "%{read:csimple.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose_simple/dune-project b/test/blackbox-tests/test-cases/coq/compose_simple/dune-project new file mode 100644 index 00000000000..c1fd9ec6785 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_simple/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/b/b.v b/test/blackbox-tests/test-cases/coq/compose_two_scopes/b/b.v new file mode 100644 index 00000000000..e184683b4d4 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/b/b.v @@ -0,0 +1,3 @@ +From a Require Import a. + +Definition bar := a.foo. diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/b/dune b/test/blackbox-tests/test-cases/coq/compose_two_scopes/b/dune new file mode 100644 index 00000000000..41f401aad43 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/b/dune @@ -0,0 +1,4 @@ +(coq.theory + (name b) + (package cvendor) + (theories a)) diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/cvendor.opam b/test/blackbox-tests/test-cases/coq/compose_two_scopes/cvendor.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune b/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune new file mode 100644 index 00000000000..7e780eb3f8e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune @@ -0,0 +1,3 @@ +(rule + (alias default) + (action (echo "%{read:cvendor.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune-project b/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune-project new file mode 100644 index 00000000000..c1fd9ec6785 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/a/a.v b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/a/a.v new file mode 100644 index 00000000000..d4389c6d37d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/a/a.v @@ -0,0 +1 @@ +Definition foo := 3. diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/a/dune b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/a/dune new file mode 100644 index 00000000000..ee076f21132 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/a/dune @@ -0,0 +1,3 @@ +(coq.theory + (name a) + (package cvendor2)) diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/cvendor2.opam b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/cvendor2.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/dune-project b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/dune-project new file mode 100644 index 00000000000..c1fd9ec6785 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune b/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune new file mode 100644 index 00000000000..7c5eb6af132 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune @@ -0,0 +1,3 @@ +(rule + (alias default) + (action (echo "%{read:public.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune-project b/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune-project new file mode 100644 index 00000000000..c1fd9ec6785 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/public_dep_on_private/private/a.v b/test/blackbox-tests/test-cases/coq/public_dep_on_private/private/a.v new file mode 100644 index 00000000000..d4389c6d37d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/public_dep_on_private/private/a.v @@ -0,0 +1 @@ +Definition foo := 3. diff --git a/test/blackbox-tests/test-cases/coq/public_dep_on_private/private/dune b/test/blackbox-tests/test-cases/coq/public_dep_on_private/private/dune new file mode 100644 index 00000000000..fbc1a9bb1ca --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/public_dep_on_private/private/dune @@ -0,0 +1,2 @@ +(coq.theory + (name private)) diff --git a/test/blackbox-tests/test-cases/coq/public_dep_on_private/public.opam b/test/blackbox-tests/test-cases/coq/public_dep_on_private/public.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/public_dep_on_private/public/b.v b/test/blackbox-tests/test-cases/coq/public_dep_on_private/public/b.v new file mode 100644 index 00000000000..5f955f638da --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/public_dep_on_private/public/b.v @@ -0,0 +1,3 @@ +From private Require a. + +Definition bar := a.foo. diff --git a/test/blackbox-tests/test-cases/coq/public_dep_on_private/public/dune b/test/blackbox-tests/test-cases/coq/public_dep_on_private/public/dune new file mode 100644 index 00000000000..0ca7f3cf462 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/public_dep_on_private/public/dune @@ -0,0 +1,4 @@ +(coq.theory + (name public) + (package public) + (theories private)) diff --git a/test/blackbox-tests/test-cases/coq/run.t b/test/blackbox-tests/test-cases/coq/run.t index f7d882c554d..d0402a861e9 100644 --- a/test/blackbox-tests/test-cases/coq/run.t +++ b/test/blackbox-tests/test-cases/coq/run.t @@ -68,3 +68,110 @@ "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.vo" {"coq/user-contrib/rec_module/c/d/bar.vo"} "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.vo" {"coq/user-contrib/rec_module/c/ooo.vo"} ] + + $ dune build --root compose_simple/ --display short --debug-dependency-path + Entering directory 'compose_simple' + coqdep a/a.v.d + coqc a/a.vo + coqdep b/b.v.d + coqc b/b.vo + lib: [ + "_build/install/default/lib/csimple/META" + "_build/install/default/lib/csimple/dune-package" + "_build/install/default/lib/csimple/opam" + ] + lib_root: [ + "_build/install/default/lib/coq/user-contrib/a/a.vo" {"coq/user-contrib/a/a.vo"} + "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"} + ] + + $ dune build --root compose_plugin --display short --debug-dependency-path @all + Entering directory 'compose_plugin' + coqdep thy1/a.v.d + ocamlc src_b/.ml_plugin_b.objs/byte/ml_plugin_b.{cmi,cmo,cmt} + ocamlopt src_b/.ml_plugin_b.objs/native/ml_plugin_b.{cmx,o} + ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a.{cmi,cmo,cmt} + ocamlopt src_a/.ml_plugin_a.objs/native/ml_plugin_a.{cmx,o} + ocamldep src_a/.ml_plugin_a.objs/gram.mli.d + ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a__Gram.{cmi,cmti} + ocamldep src_a/.ml_plugin_a.objs/simple.ml.d + ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a__Simple.{cmi,cmo,cmt} + ocamlopt src_a/.ml_plugin_a.objs/native/ml_plugin_a__Simple.{cmx,o} + ocamldep src_b/.ml_plugin_b.objs/simple_b.ml.d + ocamlc src_b/.ml_plugin_b.objs/byte/ml_plugin_b__Simple_b.{cmi,cmo,cmt} + ocamlc src_b/ml_plugin_b.cma + coqdep thy2/a.v.d + coqpp src_a/gram.ml + ocamldep src_a/.ml_plugin_a.objs/gram.ml.d + ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a__Gram.{cmo,cmt} + ocamlc src_a/ml_plugin_a.cma + ocamlopt src_b/.ml_plugin_b.objs/native/ml_plugin_b__Simple_b.{cmx,o} + ocamlopt src_b/ml_plugin_b.{a,cmxa} + ocamlopt src_b/ml_plugin_b.cmxs + ocamlopt src_a/.ml_plugin_a.objs/native/ml_plugin_a__Gram.{cmx,o} + ocamlopt src_a/ml_plugin_a.{a,cmxa} + ocamlopt src_a/ml_plugin_a.cmxs + coqc thy1/a.vo + coqc thy2/a.vo + +# Test only works on Coq 8.12 due to boot constraints +# $ dune build --root compose_boot/ --display short --debug-dependency-path + + $ dune build --root public_dep_on_private/ --display short --debug-dependency-path + Entering directory 'public_dep_on_private' + File "public/dune", line 4, characters 11-18: + 4 | (theories private)) + ^^^^^^^ + Error: Theory "private" is private, it cannot be a dependency of a public + theory. You need to associate "private" to a package. + -> required by public/b.v.d + -> required by public/b.vo + -> required by install lib/coq/user-contrib/public/b.vo + -> required by public.install + -> required by alias default + -> required by alias default + [1] + + $ dune build --root compose_cycle/ --display short --debug-dependency-path + Entering directory 'compose_cycle' + File "a/dune", line 2, characters 7-8: + 2 | (name a) + ^ + Error: Cycle found + - b + - a + - b + -> required by a/a.v.d + -> required by a/a.vo + -> required by install lib/coq/user-contrib/a/a.vo + -> required by ccycle.install + -> required by alias default + -> required by alias default + File "b/dune", line 2, characters 7-8: + 2 | (name b) + ^ + Error: Cycle found + - a + - b + - a + -> required by b/b.v.d + -> required by b/b.vo + -> required by install lib/coq/user-contrib/b/b.vo + -> required by ccycle.install + -> required by alias default + -> required by alias default + [1] + + $ dune build --root compose_two_scopes/ --display short --debug-dependency-path + Entering directory 'compose_two_scopes' + File "b/dune", line 4, characters 11-12: + 4 | (theories a)) + ^ + Error: Theory a not found + -> required by b/b.v.d + -> required by b/b.vo + -> required by install lib/coq/user-contrib/b/b.vo + -> required by cvendor.install + -> required by alias default + -> required by alias default + [1]