From 252ab2f9ceed6b353cbf3832ce86bd36c8dc18a0 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 26 May 2022 16:47:15 +0100 Subject: [PATCH] feature(coq): support for inter-project composition of theories Signed-off-by: Ali Caglayan --- src/dune_rules/coq_lib.ml | 19 ++-- src/dune_rules/coq_lib.mli | 2 +- src/dune_rules/scope.ml | 36 +++++--- .../coq/compose-coq-projects.t/A/A.opam | 0 .../coq/compose-coq-projects.t/A/a.v | 2 + .../coq/compose-coq-projects.t/A/dune | 4 + .../coq/compose-coq-projects.t/A/dune-project | 2 + .../coq/compose-coq-projects.t/B/b.v | 4 + .../coq/compose-coq-projects.t/B/dune | 4 + .../coq/compose-coq-projects.t/B/dune-project | 2 + .../coq/compose-coq-projects.t/OtherLib/dune | 3 + .../OtherLib/dune-project | 1 + .../compose-coq-projects.t/OtherLib/foo.ml | 1 + .../OtherLib/other-lib.opam | 0 .../coq/compose-coq-projects.t/dune-workspace | 1 + .../coq/compose-coq-projects.t/run.t | 9 ++ .../test-cases/coq/compose-two-scopes.t/run.t | 92 ++++++++++++++++--- 17 files changed, 150 insertions(+), 32 deletions(-) create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/A.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/foo.ml create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/other-lib.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/dune-workspace create mode 100644 test/blackbox-tests/test-cases/coq/compose-coq-projects.t/run.t diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml index 5a7155ecae6c..dc89ebb4896a 100644 --- a/src/dune_rules/coq_lib.ml +++ b/src/dune_rules/coq_lib.ml @@ -76,9 +76,10 @@ end module DB = struct type lib = t - type nonrec t = - { boot : (Loc.t * t) option - ; libs : t Coq_lib_name.Map.t + type t = + { boot : (Loc.t * lib) option + ; libs : lib Coq_lib_name.Map.t + ; parent : t option } let boot_library { boot; _ } = boot @@ -97,7 +98,7 @@ module DB = struct } ) (* Should we register errors and printers, or raise is OK? *) - let create_from_coqlib_stanzas sl = + let create_from_coqlib_stanzas ~(parent : t option) sl = let libs = match Coq_lib_name.Map.of_list_map ~f:create_from_stanza sl with | Ok m -> m @@ -111,15 +112,19 @@ module DB = struct | _ :: (_, s2) :: _ -> Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.buildable.loc s2) in - { boot; libs } + { boot; libs; parent } - let resolve ?(allow_private_deps = true) db (loc, name) = + (* TODO: what is the point of this flag? *) + let rec 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 + | None -> ( + match db.parent with + | Some parent -> resolve ~allow_private_deps parent (loc, name) + | None -> Error.theory_not_found ~loc name) let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name)) diff --git a/src/dune_rules/coq_lib.mli b/src/dune_rules/coq_lib.mli index 5ac26f80baf8..64f2991b7be0 100644 --- a/src/dune_rules/coq_lib.mli +++ b/src/dune_rules/coq_lib.mli @@ -27,7 +27,7 @@ module DB : sig type t - val create_from_coqlib_stanzas : + val create_from_coqlib_stanzas : parent:t option -> (Path.Build.t * Coq_stanza.Theory.t) list -> t val find_many : t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Or_exn.t diff --git a/src/dune_rules/scope.ml b/src/dune_rules/scope.ml index c6a15f3ffc67..44c62d24650a 100644 --- a/src/dune_rules/scope.ml +++ b/src/dune_rules/scope.ml @@ -132,6 +132,11 @@ module DB = struct Lib.DB.Resolve_result.redirect (Some scope.db) (Loc.none, name) | Some (Name name) -> Lib.DB.Resolve_result.redirect None name + let public_theories coq_stanzas = + List.filter coq_stanzas ~f:(fun (_, (stanza : Coq_stanza.Theory.t)) -> + Option.is_some stanza.package) + |> Coq_lib.DB.create_from_coqlib_stanzas ~parent:None + (* Create a database from the public libraries defined in the stanzas *) let public_libs t ~installed_libs ~modules_of_lib ~lib_config ~projects_by_package stanzas = @@ -178,7 +183,7 @@ module DB = struct module Path_source_map_traversals = Memo.Make_map_traversals (Path.Source.Map) let scopes_by_dir context ~projects_by_package ~modules_of_lib ~projects - ~public_libs stanzas coq_stanzas = + ~public_libs ~public_theories stanzas coq_stanzas = let open Memo.O in let projects_by_dir = List.map projects ~f:(fun (project : Dune_project.t) -> @@ -196,12 +201,21 @@ module DB = struct (Dune_project.root project, stanza)) |> Path.Source.Map.of_list_multi in - let coq_db_by_project_dir = - List.map coq_stanzas ~f:(fun (dir, t) -> - let project = t.Coq_stanza.Theory.project in - (Dune_project.root project, (dir, t))) + let coq_stanzas_by_project_dir = + List.map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) -> + let project = stanza.project in + (Dune_project.root project, (dir, stanza))) |> Path.Source.Map.of_list_multi - |> Path.Source.Map.map ~f:Coq_lib.DB.create_from_coqlib_stanzas + in + let coq_db_by_project_dir = + Path.Source.Map.merge projects_by_dir coq_stanzas_by_project_dir + ~f:(fun _dir project coq_stanzas -> + let project = Option.value_exn project in + let stanzas = Option.value coq_stanzas ~default:[] in + Some (project, stanzas)) + |> Path.Source.Map.map ~f:(fun (project, stanzas) -> + let db = Coq_lib.DB.create_from_coqlib_stanzas ~parent:(Some public_theories) stanzas in + (project, db)) in let lib_config = Context.lib_config context in let+ db_by_project_dir = @@ -221,11 +235,8 @@ module DB = struct Path.Source.Map.merge db_by_project_dir coq_db_by_project_dir ~f:(fun _dir project_and_db coq_db -> let project, db = Option.value_exn project_and_db in - let coq_db = - match coq_db with - | Some db -> db - | None -> Coq_lib.DB.create_from_coqlib_stanzas [] - in + let project', coq_db = Option.value_exn coq_db in + assert (Dune_project.equal project project'); let root = Path.Build.append_source context.build_dir (Dune_project.root project) in @@ -240,9 +251,10 @@ module DB = struct public_libs t ~installed_libs ~lib_config ~projects_by_package ~modules_of_lib stanzas in + let public_theories = public_theories coq_stanzas in let+ by_dir = scopes_by_dir context ~projects ~projects_by_package ~public_libs - ~modules_of_lib stanzas coq_stanzas + ~public_theories ~modules_of_lib stanzas coq_stanzas in let value = { by_dir } in Fdecl.set t value; diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/A.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/a.v new file mode 100644 index 000000000000..831752c569d8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/a.v @@ -0,0 +1,2 @@ + +Inductive Hello := World | Bye. diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune new file mode 100644 index 000000000000..084e1edeb448 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune @@ -0,0 +1,4 @@ +(coq.theory + (name A) + (package A)) + diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune-project new file mode 100644 index 000000000000..06314b536ad9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/b.v new file mode 100644 index 000000000000..5659f2682e6d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/b.v @@ -0,0 +1,4 @@ +From A Require Import a. + +Check Hello. + diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune new file mode 100644 index 000000000000..7fc1c5b311a3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune @@ -0,0 +1,4 @@ +(coq.theory + (name B) + (libraries other-lib) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune-project new file mode 100644 index 000000000000..06314b536ad9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune new file mode 100644 index 000000000000..31d715314ef5 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune @@ -0,0 +1,3 @@ +(library + (name otherlib) + (public_name other-lib)) diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune-project b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune-project new file mode 100644 index 000000000000..714e17a8a46b --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune-project @@ -0,0 +1 @@ +(lang dune 3.2) \ No newline at end of file diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/foo.ml b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/foo.ml new file mode 100644 index 000000000000..cab79024b03f --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/foo.ml @@ -0,0 +1 @@ +let hello = "world" diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/other-lib.opam b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/other-lib.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/dune-workspace new file mode 100644 index 000000000000..0c226b5b0c6e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/dune-workspace @@ -0,0 +1 @@ +(lang dune 3.2) diff --git a/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/run.t b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/run.t new file mode 100644 index 000000000000..a70e280b497a --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-coq-projects.t/run.t @@ -0,0 +1,9 @@ +Testing composition of theories accross a dune workspace + + $ dune build --root B + Entering directory 'B' + File "dune", line 4, characters 11-12: + 4 | (theories A)) + ^ + Error: Theory A not found + [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t index 0285fd613ea8..5d1aa4f42293 100644 --- a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t @@ -1,12 +1,80 @@ - $ dune build --debug-dependency-path - File "b/dune", line 4, characters 11-12: - 4 | (theories a)) - ^ - Error: Theory a not found - -> required by _build/default/b/b.v.d - -> required by _build/default/b/b.vo - -> required by _build/install/default/lib/coq/user-contrib/b/b.vo - -> required by _build/default/cvendor.install - -> required by %{read:cvendor.install} at dune:3 - -> required by alias default in dune:1 - [1] + $ tree + . + |-- b + | |-- b.v -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/b/b.v + | `-- dune -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/b/dune + |-- cvendor.opam -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/cvendor.opam + |-- dune -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune + |-- dune-project -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune-project + `-- vendor + |-- a + | |-- a.v -> ../../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/a/a.v + | `-- dune -> ../../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/a/dune + |-- cvendor2.opam -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/cvendor2.opam + `-- dune-project -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project + + 3 directories, 9 files + + + $ dune build --debug-dependency-path --debug-backtrace + ** resolving parent + lib: [ + "_build/install/default/lib/cvendor/META" + "_build/install/default/lib/cvendor/dune-package" + "_build/install/default/lib/cvendor/opam" + ] + lib_root: [ + "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"} + "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"} + ] + + $ tree + . + |-- _build + | |-- default + | | |-- META.cvendor + | | |-- b + | | | |-- b.glob + | | | |-- b.v + | | | |-- b.v.d + | | | |-- b.vo + | | | |-- b.vok + | | | `-- b.vos + | | |-- cvendor.dune-package + | | |-- cvendor.install + | | |-- cvendor.opam + | | `-- vendor + | | `-- a + | | |-- a.glob + | | |-- a.v + | | |-- a.v.d + | | |-- a.vo + | | |-- a.vok + | | `-- a.vos + | |-- install + | | `-- default + | | `-- lib + | | |-- coq + | | | `-- user-contrib + | | | `-- b + | | | |-- b.v -> ../../../../../../default/b/b.v + | | | `-- b.vo -> ../../../../../../default/b/b.vo + | | `-- cvendor + | | |-- META -> ../../../../default/META.cvendor + | | |-- dune-package -> ../../../../default/cvendor.dune-package + | | `-- opam -> ../../../../default/cvendor.opam + | `-- log + |-- b + | |-- b.v -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/b/b.v + | `-- dune -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/b/dune + |-- cvendor.opam -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/cvendor.opam + |-- dune -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune + |-- dune-project -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune-project + `-- vendor + |-- a + | |-- a.v -> ../../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/a/a.v + | `-- dune -> ../../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/a/dune + |-- cvendor2.opam -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/cvendor2.opam + `-- dune-project -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project + + 15 directories, 31 files