From e6acc179ab25ce41b748709d3094831e36562df5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 1 Apr 2019 13:29:33 +0200 Subject: [PATCH] [coq] Allow dependencies and composition with local Coq libraries. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We support simple composition of Coq libraries using the `(theories ...)` field. The main changes are: - Coq libraries now have a `Coq_lib.t` type - Stanza scanning does now initialize a `Coq_lib.DB`, per scope. Supporting inter-scope public libraries is left for a future PR. - We properly compose when the stdlib is in scope, this allows to have a compositional build with Coq itself; note that as of today, in a composed build the stdlib prefix `Coq` is introduced qualified; this reflects upstream roadmap of deprecating implicit libs. See comment in `Scope.public_libs` We have added tests for: - simple composition - composition with plugin - cyclic composition - boot composition [disabled until Coq 8.12 is released] - inter-scope composition [fails for now] We leave for future work: - Allow to depend on theories in a different scope - Allow to depend on theories installed globally, likely this will require the 2.0 version of the Coq language - Validation of Coq library names should be improved [clarify upstream rules] Includes changes by Rudi Grinberg [many suggestions] and Théo Zimmerman [documentation review] Signed-off-by: Emilio Jesus Gallego Arias --- CHANGES.md | 6 + doc/dune-files.rst | 22 +- src/dune/coq_lib.ml | 124 +++++++++++ src/dune/coq_lib.mli | 39 ++++ src/dune/coq_lib_name.ml | 5 +- src/dune/coq_lib_name.mli | 5 +- src/dune/coq_rules.ml | 203 +++++++++++------- src/dune/coq_rules.mli | 1 + src/dune/dune_file.ml | 6 + src/dune/dune_file.mli | 2 + src/dune/gen_rules.ml | 2 +- src/dune/lib.ml | 9 +- src/dune/lib.mli | 1 + src/dune/scope.ml | 18 +- src/dune/scope.mli | 2 + src/dune/super_context.ml | 5 + src/stdune/list.ml | 5 + src/stdune/list.mli | 2 + .../coq/compose_boot/boot/Init/Prelude.v | 1 + .../test-cases/coq/compose_boot/boot/dune | 7 + .../test-cases/coq/compose_boot/cboot.opam | 0 .../test-cases/coq/compose_boot/dune | 3 + .../test-cases/coq/compose_boot/dune-project | 3 + .../test-cases/coq/compose_boot/user/dune | 5 + .../test-cases/coq/compose_boot/user/user.v | 1 + .../test-cases/coq/compose_cycle/a/a.v | 1 + .../test-cases/coq/compose_cycle/a/dune | 4 + .../test-cases/coq/compose_cycle/b/b.v | 3 + .../test-cases/coq/compose_cycle/b/dune | 4 + .../test-cases/coq/compose_cycle/ccycle.opam | 0 .../test-cases/coq/compose_cycle/dune | 3 + .../test-cases/coq/compose_cycle/dune-project | 3 + .../coq/compose_plugin/cplugin.opam | 1 + .../test-cases/coq/compose_plugin/dune | 3 + .../coq/compose_plugin/dune-project | 3 + .../test-cases/coq/compose_plugin/src_a/dune | 7 + .../coq/compose_plugin/src_a/gram.mlg | 9 + .../coq/compose_plugin/src_a/gram.mli | 1 + .../compose_plugin/src_a/ml_plugin_a.mlpack | 0 .../coq/compose_plugin/src_a/simple.ml | 2 + .../test-cases/coq/compose_plugin/src_b/dune | 5 + .../compose_plugin/src_b/ml_plugin_b.mlpack | 0 .../coq/compose_plugin/src_b/simple_b.ml | 1 + .../test-cases/coq/compose_plugin/thy1/a.v | 3 + .../test-cases/coq/compose_plugin/thy1/dune | 6 + .../test-cases/coq/compose_plugin/thy2/a.v | 3 + .../test-cases/coq/compose_plugin/thy2/dune | 6 + .../test-cases/coq/compose_simple/a/a.v | 1 + .../test-cases/coq/compose_simple/a/dune | 3 + .../test-cases/coq/compose_simple/b/b.v | 3 + .../test-cases/coq/compose_simple/b/dune | 4 + .../coq/compose_simple/csimple.opam | 0 .../test-cases/coq/compose_simple/dune | 3 + .../coq/compose_simple/dune-project | 3 + .../test-cases/coq/compose_two_scopes/b/b.v | 3 + .../test-cases/coq/compose_two_scopes/b/dune | 4 + .../coq/compose_two_scopes/cvendor.opam | 0 .../test-cases/coq/compose_two_scopes/dune | 3 + .../coq/compose_two_scopes/dune-project | 3 + .../coq/compose_two_scopes/vendor/a/a.v | 1 + .../coq/compose_two_scopes/vendor/a/dune | 3 + .../compose_two_scopes/vendor/cvendor2.opam | 0 .../compose_two_scopes/vendor/dune-project | 3 + test/blackbox-tests/test-cases/coq/run.t | 92 ++++++++ 64 files changed, 585 insertions(+), 89 deletions(-) create mode 100644 src/dune/coq_lib.ml create mode 100644 src/dune/coq_lib.mli create mode 100644 test/blackbox-tests/test-cases/coq/compose_boot/boot/Init/Prelude.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_boot/boot/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_boot/cboot.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose_boot/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_boot/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose_boot/user/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_boot/user/user.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_cycle/a/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_cycle/a/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_cycle/b/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_cycle/b/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_cycle/ccycle.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose_cycle/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_cycle/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/cplugin.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/src_a/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/src_a/gram.mlg create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/src_a/gram.mli create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/src_a/ml_plugin_a.mlpack create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/src_a/simple.ml create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/src_b/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/src_b/ml_plugin_b.mlpack create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/src_b/simple_b.ml create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/thy1/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/thy1/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/thy2/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_plugin/thy2/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_simple/a/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_simple/a/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_simple/b/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_simple/b/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_simple/csimple.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose_simple/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_simple/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/b/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/b/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/cvendor.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/a/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/a/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/cvendor2.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/dune-project diff --git a/CHANGES.md b/CHANGES.md index 76c4b7468bff..4b68bd5715a6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,9 @@ +unreleased +---------- + +- [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 5f32b91d395d..52f747dcb01e 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 000000000000..31fd34a06ab3 --- /dev/null +++ b/src/dune/coq_lib.ml @@ -0,0 +1,124 @@ +(* 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 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 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) -> + let loc = (snd w2).loc in + User_error.raise ~loc + [ Pp.textf "Duplicate theory name: %s" (Coq_lib_name.to_string name) ] + 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) :: _ -> + User_error.raise ~loc:s2.loc + [ Pp.textf "Cannot have more than one boot library: %s)" + (Coq_lib_name.to_string (snd s2.name)) + ] + in + { boot; libs } + + let resolve db (loc, name) = + match Coq_lib_name.Map.find db.libs name with + | None -> + Error + User_error.( + E + (make ~loc + [ Pp.textf "Theory %s not found" (Coq_lib_name.to_string name) ])) + | Some s -> Ok s + + let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name)) + + (* Where should we move this? *) + module Result_monad : Monad_intf.S with type 'a t = ('a, exn) Result.t = + struct + type 'a t = ('a, exn) Result.t + + let return x = Ok x + + let ( >>= ) = Result.O.( >>= ) + end + + module Coq_lib_closure = Top_closure.Make (String.Set) (Result_monad) + + 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* theories = Result.List.map ~f:(resolve db) theories in + let key t = Coq_lib_name.to_string (snd t.name) in + let deps t = Result.List.map ~f:(resolve db) t.theories in + Result.bind (Coq_lib_closure.top_closure theories ~key ~deps) ~f:(function + | Ok libs -> Ok libs + | Error cycle -> + let msg = + [ Pp.textf "Cycle found" + ; Pp.enumerate cycle ~f:(fun t -> + Pp.text (Coq_lib_name.to_string (snd t.name))) + ] + in + Error User_error.(E (make ~loc:(fst t.name) msg))) +end diff --git a/src/dune/coq_lib.mli b/src/dune/coq_lib.mli new file mode 100644 index 000000000000..9dea478c0e7c --- /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 f0f27b67a0ad..9b8d8470a4bb 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 fmt x = Fmt.text fmt (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 db418fc8bf38..f0c692257853 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 Fmt.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 ade95955bbea..5fcb32f9f530 100644 --- a/src/dune/coq_rules.ml +++ b/src/dune/coq_rules.ml @@ -1,6 +1,7 @@ (* This file is licensed under The MIT License *) (* (c) MINES ParisTech 2018-2019 *) -(* Written by: Emilio Jesús Gallego Arias *) +(* (c) INRIA 2020 *) +(* Written by: Emilio Jesús Gallego Arias *) open! Stdune module SC = Super_context @@ -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.nth_opt (Coq_module.prefix coq_module) 0) + (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 d8187be11e19..84833a929e95 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 ec30adca34e3..aa33fc36d8a0 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 b44a40f26491..ac5a495f1261 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 bbd5629eeed3..618e554beeec 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 02107de73a15..0e6b2cfd8eab 100644 --- a/src/dune/lib.ml +++ b/src/dune/lib.ml @@ -1657,13 +1657,15 @@ 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 let check_valid_external_variants libmap stanzas = 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 @@ -1784,7 +1786,10 @@ module DB = struct else [ (name, Found info) ; (Lib_name.of_local conf.name, Redirect (None, 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 v2 -> let res = match (v1, v2) with diff --git a/src/dune/lib.mli b/src/dune/lib.mli index d2ec6fae564d..695f5397e635 100644 --- a/src/dune/lib.mli +++ b/src/dune/lib.mli @@ -186,6 +186,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 6e4c86bbb262..0f3e3194a99c 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 cb3bb1dc151d..f752262983da 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 c61514380878..f424f3ddda47 100644 --- a/src/dune/super_context.ml +++ b/src/dune/super_context.ml @@ -454,6 +454,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 4f1302d2dcdd..5954414505e0 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 a793ef9958a0..bb0e3f13cf77 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/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 000000000000..eaaf0e55b2cf --- /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 000000000000..cb370c83b613 --- /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 000000000000..e69de29bb2d1 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 000000000000..32d3fd982714 --- /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 000000000000..c1fd9ec67850 --- /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 000000000000..5402df7cc246 --- /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 000000000000..cdda78d422b5 --- /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 000000000000..d4389c6d37db --- /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 000000000000..478550e09852 --- /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 000000000000..e184683b4d42 --- /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 000000000000..5f42b4087e99 --- /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 000000000000..e69de29bb2d1 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 000000000000..e622b2ade9e6 --- /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 000000000000..c1fd9ec67850 --- /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 000000000000..8d1c8b69c3fc --- /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 000000000000..d6032cc01e2e --- /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 000000000000..c1fd9ec67850 --- /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 000000000000..268e6ede624e --- /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 000000000000..80481ac46318 --- /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 000000000000..bcc533d2e623 --- /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 000000000000..e69de29bb2d1 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 000000000000..555166169c99 --- /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 000000000000..a636d09f518b --- /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 000000000000..e69de29bb2d1 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 000000000000..04ea5df11e89 --- /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 000000000000..340c0d8abb5f --- /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 000000000000..c3e194a70ff4 --- /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 000000000000..340c0d8abb5f --- /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 000000000000..3646943458b1 --- /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 000000000000..d4389c6d37db --- /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 000000000000..099b8f56a24d --- /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 000000000000..e184683b4d42 --- /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 000000000000..e4edf23190e7 --- /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 000000000000..e69de29bb2d1 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 000000000000..f7a7db897dbd --- /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 000000000000..c1fd9ec67850 --- /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 000000000000..e184683b4d42 --- /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 000000000000..41f401aad43f --- /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 000000000000..e69de29bb2d1 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 000000000000..7e780eb3f8eb --- /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 000000000000..c1fd9ec67850 --- /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 000000000000..d4389c6d37db --- /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 000000000000..ee076f21132a --- /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 000000000000..e69de29bb2d1 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 000000000000..c1fd9ec67850 --- /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/run.t b/test/blackbox-tests/test-cases/coq/run.t index f7d882c554d9..763f7b3d2907 100644 --- a/test/blackbox-tests/test-cases/coq/run.t +++ b/test/blackbox-tests/test-cases/coq/run.t @@ -68,3 +68,95 @@ "_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 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]