From 30043d83e35c729e72128a6a4a423d6eeef1d7ff Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 12 Feb 2023 00:26:01 +0100 Subject: [PATCH 1/3] feature(coq): call coqdep once per theory Signed-off-by: Ali Caglayan --- src/dune_rules/coq/coq_rules.ml | 81 +++++++++++++++++-- .../test-cases/coq/base-unsound.t/run.t | 3 +- .../test-cases/coq/base.t/run.t | 3 +- .../test-cases/coq/compose-cycle.t/run.t | 3 +- .../test-cases/coq/compose-installed.t/run.t | 3 +- .../test-cases/coq/compose-plugin.t/run.t | 4 +- .../coq/compose-projects-cycle.t/run.t | 3 + .../coq/compose-projects-missing.t/run.t | 1 + .../test-cases/coq/compose-self.t/run.t | 3 +- .../test-cases/coq/coqdep-on-rebuild.t/run.t | 7 +- .../coq/coqdoc-multi-theory.t/run.t | 2 + .../test-cases/coq/coqdoc-with-boot.t/run.t | 1 + .../test-cases/coq/coqdoc.t/run.t | 1 + .../test-cases/coq/coqtop/coqtop-recomp.t | 6 +- .../test-cases/coq/ml-lib.t/run.t | 2 +- .../test-cases/coq/native-compose.t/run.t | 5 +- .../test-cases/coq/native-single.t/run.t | 3 +- .../test-cases/coq/no-stdlib.t/run.t | 3 +- .../coq/public-dep-on-private.t/run.t | 1 + .../test-cases/coq/rec-module.t/run.t | 5 +- 20 files changed, 103 insertions(+), 37 deletions(-) diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index a62289f7bc5..b2f4971801e 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/src/dune_rules/coq/coq_rules.ml @@ -307,6 +307,73 @@ let boot_type ~dir ~use_stdlib ~wrapper_name coq_module = if init then `Bootstrap_prelude else `Bootstrap lib else `Bootstrap_prelude +let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name + ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule ~theory_name coq_modules = + let* boot_type = + (* TODO find the boot type a better way *) + boot_type ~dir ~use_stdlib ~wrapper_name (List.hd coq_modules) + in + (* coqdep needs the full source + plugin's mlpack to be present :( *) + let sources = + List.rev_map + ~f:(fun module_ -> Coq_module.source module_ |> Path.build) + coq_modules + in + let file_flags = + [ Command.Args.S + (coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags) + ; As [ "-dyndep"; "opt" ] + ; Deps sources + ] + in + let stdout_to = + Path.Build.relative dir (Coq_lib_name.to_string theory_name) + |> Path.Build.set_extension ~ext:".theory.d" + in + let* coqdep = + Super_context.resolve_program sctx "coqdep" ~dir ~loc:(Some loc) + ~hint:"opam install coq" + in + (* Coqdep has to be called in the stanza's directory *) + Super_context.add_rule ~loc sctx ~dir + (let open Action_builder.With_targets.O in + Action_builder.with_no_targets mlpack_rule + >>> Action_builder.(with_no_targets (goal source_rule)) + >>> Command.run ~dir:(Path.build dir) ~stdout_to coqdep file_flags) + +let setup_coqdep_for_mod_rule ~loc ~sctx ~dir ~wrapper_name coq_module = + let theory_deps_file = + Path.Build.relative dir wrapper_name + |> Path.Build.set_extension ~ext:".theory.d" + |> Path.build + in + let deps_file = Coq_module.dep_file ~obj_dir:dir coq_module in + let vo_file = + String.concat ~sep:"/" + (Coq_module.prefix coq_module + @ [ Coq_module.Name.to_string (Coq_module.name coq_module) ]) + ^ ".vo" + in + let action = + let line = + let open Action_builder.O in + let+ lines = Action_builder.lines_of theory_deps_file in + List.find ~f:(String.is_prefix ~prefix:vo_file) lines |> function + | None -> + Code_error.raise "coqdep output doesn't match theory modules" + [ ("theory_deps_file", Path.to_dyn theory_deps_file) + ; ("vo_file", Dyn.string vo_file) + ; ("lines", Dyn.list Dyn.string lines) + ; ("coq_module", Coq_module.to_dyn coq_module) + ; ("dir", Path.to_dyn (Path.build dir)) + ; ("wrapper_name", Dyn.string wrapper_name) + ] + | Some line -> line + in + Action_builder.write_file_dyn deps_file line + in + Super_context.add_rule ~loc sctx ~dir action + let setup_coqdep_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule coq_module = let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in @@ -558,17 +625,21 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) = source_rule ~sctx theories in let coqc_dir = (Super_context.context sctx).build_dir in - let* mode = select_native_mode ~sctx ~dir s.buildable in - Memo.parallel_iter coq_modules - ~f: - (setup_coqdep_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name - ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule) + let theory_name = snd s.name in + (* First we setup the rule calling coqdep *) + setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name + ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule ~theory_name coq_modules + (* Next the rules filtering that file per module *) + >>> Memo.parallel_iter coq_modules + ~f:(setup_coqdep_for_mod_rule ~sctx ~dir ~loc ~wrapper_name) + (* Then we setup the coqc rules *) >>> Memo.parallel_iter coq_modules ~f: (setup_coqc_rule ~loc ~dir ~sctx ~file_targets:[] ~stanza_flags ~coqc_dir ~theories_deps ~mode ~wrapper_name ~use_stdlib ~ml_flags ~theory_dirs) + (* And finally the coqdoc rules *) >>> setup_coqdoc_rules ~sctx ~dir ~theories_deps s coq_modules let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) diff --git a/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t b/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t index f704c496a6a..53d190ebade 100644 --- a/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t +++ b/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t @@ -1,5 +1,4 @@ $ dune build --display short --profile unsound --debug-dependency-path @all - coqdep bar.v.d - coqdep foo.v.d + coqdep basic.theory.d coqc foo.{glob,vo} coqc bar.{glob,vo} diff --git a/test/blackbox-tests/test-cases/coq/base.t/run.t b/test/blackbox-tests/test-cases/coq/base.t/run.t index e5bccec4b47..b632a6f243f 100644 --- a/test/blackbox-tests/test-cases/coq/base.t/run.t +++ b/test/blackbox-tests/test-cases/coq/base.t/run.t @@ -1,6 +1,5 @@ $ dune build --display short --debug-dependency-path @all - coqdep bar.v.d - coqdep foo.v.d + coqdep basic.theory.d coqc foo.{glob,vo} coqc bar.{glob,vo} diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t index 13b65eea34e..6faaf3ad451 100644 --- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t @@ -4,8 +4,7 @@ We check cycles are detected theory A in A -> theory B in B -> theory A in A - -> required by _build/default/A/a.v.d - -> required by _build/default/A/a.glob + -> required by _build/default/A/A.theory.d -> required by alias A/all -> required by alias default [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t index 223e50bd5ed..46099480358 100644 --- a/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t @@ -12,8 +12,7 @@ TODO: Currently this is not supported so the output is garbage ^ Theory B not found -> required by theory A in . - -> required by _build/default/a.v.d - -> required by _build/default/a.glob + -> required by _build/default/A.theory.d -> required by alias all -> required by alias default [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t b/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t index 91f762e850b..3c2361b1bf5 100644 --- a/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t @@ -1,11 +1,11 @@ $ dune build --display short --debug-dependency-path @all - coqdep thy1/a.v.d + coqdep thy1/thy1.theory.d ocamlc src_b/.ml_plugin_b.objs/byte/ml_plugin_b.{cmi,cmo,cmt} ocamldep src_b/.ml_plugin_b.objs/ml_plugin_b__Simple_b.impl.d ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a.{cmi,cmo,cmt} ocamldep src_a/.ml_plugin_a.objs/ml_plugin_a__Gram.intf.d ocamldep src_a/.ml_plugin_a.objs/ml_plugin_a__Simple.impl.d - coqdep thy2/a.v.d + coqdep thy2/thy2.theory.d coqpp src_a/gram.ml ocamlopt src_b/.ml_plugin_b.objs/native/ml_plugin_b.{cmx,o} ocamlopt src_a/.ml_plugin_a.objs/native/ml_plugin_a.{cmx,o} diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t index 69986b89cd8..5c6449072cb 100644 --- a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t @@ -7,6 +7,7 @@ dependencies. -> theory B in B -> theory C in C -> theory A in A + -> required by _build/default/A/A.theory.d -> required by _build/default/A/a.v.d -> required by _build/default/A/a.vo -> required by _build/install/default/lib/coq/user-contrib/A/a.vo @@ -21,6 +22,7 @@ dependencies. -> theory C in C -> theory A in A -> theory B in B + -> required by _build/default/B/B.theory.d -> 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 @@ -35,6 +37,7 @@ dependencies. -> theory A in A -> theory B in B -> theory C in C + -> required by _build/default/C/C.theory.d -> required by _build/default/C/c.v.d -> required by _build/default/C/c.vo -> required by _build/install/default/lib/coq/user-contrib/C/c.vo diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t index 1badfd00885..e5205c50118 100644 --- a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t @@ -8,6 +8,7 @@ dependency. Theory A not found -> required by theory B in B -> required by theory C in C + -> required by _build/default/C/C.theory.d -> required by _build/default/C/c.v.d -> required by _build/default/C/c.vo -> required by _build/install/default/lib/coq/user-contrib/C/c.vo diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/run.t b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t index 94f362f5ac4..1f47bcddafa 100644 --- a/test/blackbox-tests/test-cases/coq/compose-self.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t @@ -2,8 +2,7 @@ Composing a theory with itself should cause a cycle $ dune build Error: Dependency cycle between: theory A in A - -> required by _build/default/A/a.v.d - -> required by _build/default/A/a.glob + -> required by _build/default/A/A.theory.d -> required by alias A/all -> required by alias default [1] diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t index 8699c67504e..63fc49c1c9b 100644 --- a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t @@ -14,9 +14,8 @@ > Definition doo := a.foo. > EOF $ dune build --display short --debug-dependency-path - coqdep a/a.v.d - coqdep b/b.v.d - coqdep b/d.v.d + coqdep a/a.theory.d + coqdep b/b.theory.d coqc a/Na_a.{cmi,cmxs},a/a.{glob,vo} coqc b/Nb_b.{cmi,cmxs},b/b.{glob,vo} coqc b/Nb_d.{cmi,cmxs},b/d.{glob,vo} @@ -26,5 +25,5 @@ > Definition zoo := 4. > EOF $ dune build --display short --debug-dependency-path - coqdep b/b.v.d + coqdep b/b.theory.d coqc b/Nb_b.{cmi,cmxs},b/b.{glob,vo} diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t index 32e083c7338..ce045897014 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t @@ -20,6 +20,7 @@ Next we build the doc for the second theory $ dune build @B/doc Check that the first theory doc is not built $ ls _build/default/A/ + A.theory.d AA AB Check that the second theory doc is built @@ -52,6 +53,7 @@ Next we build the doc for the second theory $ dune build @B/doc-latex Check that the first theory doc is not built $ ls _build/default/A + A.theory.d AA AB Check that the second theory doc is built diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t index 6958d72f6ad..1edaac6b9df 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t @@ -4,6 +4,7 @@ Testing coqdoc when composed with a boot library $ ls _build/default/A A.html + A.theory.d a.glob a.v a.v.d diff --git a/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t index 6078f892148..a427fb7fe12 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t @@ -32,6 +32,7 @@ Note that this currently works due to a bug in @all detecting directory targets. bar.vos base.dune-package base.install + basic.theory.d foo.glob foo.v foo.v.d diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t index 34463fe15fb..66b5062434d 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t +++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t @@ -19,8 +19,7 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587). > (using coq 0.3) > EOF $ dune coq top --display short --toplevel echo dir/bar.v - coqdep dir/bar.v.d - coqdep dir/foo.v.d + coqdep dir/basic.theory.d coqc dir/foo.{glob,vo} -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic $ dune coq top --display short --toplevel echo dir/bar.v @@ -28,8 +27,7 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587). $ dune clean $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v) Entering directory '..' - coqdep dir/bar.v.d - coqdep dir/foo.v.d + coqdep dir/basic.theory.d coqc dir/foo.{glob,vo} Leaving directory '..' -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic diff --git a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t b/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t index 4cd43e6797b..be829ea467f 100644 --- a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t +++ b/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t @@ -1,5 +1,5 @@ $ dune build --display short --debug-dependency-path @all - coqdep theories/a.v.d + coqdep theories/Plugin.theory.d ocamlc src_b/.ml_plugin_b.objs/byte/ml_plugin_b.{cmi,cmo,cmt} ocamldep src_b/.ml_plugin_b.objs/ml_plugin_b__Simple_b.impl.d ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a.{cmi,cmo,cmt} diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t index 4981aec7e5b..826fb2a1238 100644 --- a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t @@ -1,7 +1,6 @@ $ dune build --profile=release --display short --debug-dependency-path @all - coqdep bar/bar.v.d - coqdep foo/foo.v.d - coqdep foo/a/a.v.d + coqdep bar/bar.theory.d + coqdep foo/foo.theory.d coqc foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo} coqc foo/a/Nfoo_a_a.{cmi,cmxs},foo/a/a.{glob,vo} coqc bar/Nbar_baz_bar.{cmi,cmxs},bar/bar.{glob,vo} diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/run.t b/test/blackbox-tests/test-cases/coq/native-single.t/run.t index fa612247597..b911a3e3a2c 100644 --- a/test/blackbox-tests/test-cases/coq/native-single.t/run.t +++ b/test/blackbox-tests/test-cases/coq/native-single.t/run.t @@ -1,6 +1,5 @@ $ dune build --profile=release --display short --debug-dependency-path @all - coqdep bar.v.d - coqdep foo.v.d + coqdep basic.theory.d coqc Nbasic_foo.{cmi,cmxs},foo.{glob,vo} coqc Nbasic_bar.{cmi,cmxs},bar.{glob,vo} diff --git a/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t b/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t index 15144d49c6f..6c1c2d4951d 100644 --- a/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t +++ b/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t @@ -2,7 +2,7 @@ Test that when `(stdlib no)` is provided, the standard library is not bound to ` and the prelude is not imported $ dune build --display=short foo.vo - coqdep foo.v.d + coqdep basic.theory.d *** Warning: in file foo.v, library Prelude is required from root Coq and has not been found in the loadpath! coqc foo.{glob,vo} (exit 1) File "./foo.v", line 1, characters 0-32: @@ -12,7 +12,6 @@ and the prelude is not imported [1] $ dune build --display=short bar.vo - coqdep bar.v.d coqc bar.{glob,vo} (exit 1) File "./bar.v", line 1, characters 20-23: Error: The reference nat was not found in the current environment. diff --git a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t index 785e823b623..78ac9a9e8b0 100644 --- a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t +++ b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t @@ -5,6 +5,7 @@ Theory "private" is private, it cannot be a dependency of a public theory. You need to associate "private" to a package. -> required by theory public in public + -> required by _build/default/public/public.theory.d -> required by _build/default/public/b.v.d -> required by _build/default/public/b.vo -> required by _build/install/default/lib/coq/user-contrib/public/b.vo diff --git a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t index f928963911d..d54525cc3ba 100644 --- a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t +++ b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t @@ -1,8 +1,5 @@ $ dune build --display short --debug-dependency-path @all - coqdep a/bar.v.d - coqdep b/foo.v.d - coqdep c/d/bar.v.d - coqdep c/ooo.v.d + coqdep rec_module.theory.d coqc b/foo.{glob,vo} coqc c/d/bar.{glob,vo} coqc c/ooo.{glob,vo} From ef5b971cb0a0dced3bec2b10fae67e22b6b47904 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Feb 2023 19:52:20 +0100 Subject: [PATCH 2/3] [coq] Parse coqdep output into a shared dependency map. This avoids generating the individual `.v.d` files, and should provide a modest speedup, and cleaner code. Signed-off-by: Emilio Jesus Gallego Arias Co-authored-by: Ali Caglayan --- bin/coq/coqtop.ml | 18 +- src/dune_rules/coq/coq_rules.ml | 206 +++++++----------- src/dune_rules/coq/coq_rules.mli | 9 +- .../coq/compose-projects-cycle.t/run.t | 3 - .../coq/compose-projects-missing.t/run.t | 1 - .../test-cases/coq/coqdoc-with-boot.t/run.t | 1 - .../test-cases/coq/coqdoc.t/run.t | 2 - test/blackbox-tests/test-cases/coq/extract.t | 2 +- .../test-cases/coq/plugin-meta.t/run.t | 2 +- .../coq/public-dep-on-private.t/run.t | 1 - 10 files changed, 104 insertions(+), 141 deletions(-) diff --git a/bin/coq/coqtop.ml b/bin/coq/coqtop.ml index 71f17f0998e..e1d477fbe84 100644 --- a/bin/coq/coqtop.ml +++ b/bin/coq/coqtop.ml @@ -114,11 +114,23 @@ let term = , "DuneExtraction" ) in let* (_ : unit * Dep.Fact.t Dep.Map.t) = - let deps = - Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name + let dep_map = + Dune_rules.Coq_rules.get_dep_map ~dir ~use_stdlib ~wrapper_name coq_module in - Action_builder.run deps Eager + let vo_target = + Path.Build.set_extension ~ext:".vo" + (Dune_rules.Coq_module.source coq_module) + in + Action_builder.( + run + (bind dep_map ~f:(fun dep_map -> + let vo_deps = + Dune_rules.Coq_rules.Dep_map.find_exn dep_map + (Path.build vo_target) + in + paths vo_deps))) + Eager in let* (args, _) : string list * Dep.Fact.t Dep.Map.t = let* args = diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index b2f4971801e..21a1b534e6a 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/src/dune_rules/coq/coq_rules.ml @@ -249,45 +249,6 @@ let ml_flags_and_ml_pack_rule ~context ~lib_db ~theories_deps in (ml_flags, mlpack_rule) -let parse_coqdep ~dir ~boot_type ~coq_module (lines : string list) = - let source = Coq_module.source coq_module in - let invalid phase = - User_error.raise - [ Pp.textf "coqdep returned invalid output for %s / [phase: %s]" - (Path.Build.to_string_maybe_quoted source) - phase - ; Pp.verbatim (String.concat ~sep:"\n" lines) - ] - in - let line = - match lines with - | [] | _ :: _ :: _ :: _ -> invalid "line" - | [ line ] -> line - | [ l1; _l2 ] -> - (* .vo is produced before .vio, this is fragile tho *) - l1 - in - match String.lsplit2 line ~on:':' with - | None -> invalid "split" - | Some (basename, deps) -> ( - let ff = List.hd @@ String.extract_blank_separated_words basename in - let depname, _ = Filename.split_extension ff in - let modname = - String.concat ~sep:"/" - Coq_module.( - prefix coq_module @ [ Coq_module.Name.to_string (name coq_module) ]) - in - if depname <> modname then invalid "basename"; - let deps = String.extract_blank_separated_words deps in - (* 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 lib -> - Path.relative (Path.build (Coq_lib.src_root lib)) "Init/Prelude.vo" - :: deps) - let boot_type ~dir ~use_stdlib ~wrapper_name coq_module = let* scope = Scope.DB.find_by_dir dir in let+ boot_lib = @@ -307,8 +268,12 @@ let boot_type ~dir ~use_stdlib ~wrapper_name coq_module = if init then `Bootstrap_prelude else `Bootstrap lib else `Bootstrap_prelude +let dep_theory_file ~dir ~wrapper_name = + Path.Build.relative dir wrapper_name + |> Path.Build.set_extension ~ext:".theory.d" + let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name - ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule ~theory_name coq_modules = + ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule coq_modules = let* boot_type = (* TODO find the boot type a better way *) boot_type ~dir ~use_stdlib ~wrapper_name (List.hd coq_modules) @@ -326,10 +291,7 @@ let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name ; Deps sources ] in - let stdout_to = - Path.Build.relative dir (Coq_lib_name.to_string theory_name) - |> Path.Build.set_extension ~ext:".theory.d" - in + let stdout_to = dep_theory_file ~dir ~wrapper_name in let* coqdep = Super_context.resolve_program sctx "coqdep" ~dir ~loc:(Some loc) ~hint:"opam install coq" @@ -341,74 +303,50 @@ let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name >>> Action_builder.(with_no_targets (goal source_rule)) >>> Command.run ~dir:(Path.build dir) ~stdout_to coqdep file_flags) -let setup_coqdep_for_mod_rule ~loc ~sctx ~dir ~wrapper_name coq_module = - let theory_deps_file = - Path.Build.relative dir wrapper_name - |> Path.Build.set_extension ~ext:".theory.d" - |> Path.build - in - let deps_file = Coq_module.dep_file ~obj_dir:dir coq_module in - let vo_file = - String.concat ~sep:"/" - (Coq_module.prefix coq_module - @ [ Coq_module.Name.to_string (Coq_module.name coq_module) ]) - ^ ".vo" - in - let action = - let line = - let open Action_builder.O in - let+ lines = Action_builder.lines_of theory_deps_file in - List.find ~f:(String.is_prefix ~prefix:vo_file) lines |> function - | None -> - Code_error.raise "coqdep output doesn't match theory modules" - [ ("theory_deps_file", Path.to_dyn theory_deps_file) - ; ("vo_file", Dyn.string vo_file) - ; ("lines", Dyn.list Dyn.string lines) - ; ("coq_module", Coq_module.to_dyn coq_module) - ; ("dir", Path.to_dyn (Path.build dir)) - ; ("wrapper_name", Dyn.string wrapper_name) - ] - | Some line -> line - in - Action_builder.write_file_dyn deps_file line - in - Super_context.add_rule ~loc sctx ~dir action +module Dep_map = Stdune.Map.Make (Path) -let setup_coqdep_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name ~use_stdlib - ~source_rule ~ml_flags ~mlpack_rule coq_module = - let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in - (* coqdep needs the full source + plugin's mlpack to be present :( *) - let source = Coq_module.source coq_module in - let file_flags = - [ Command.Args.S - (coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags) - ; As [ "-dyndep"; "opt" ] - ; Dep (Path.build source) +let coqdep_invalid phase line = + User_error.raise + [ Pp.textf "coqdep returned invalid output [phase: %s]" phase + ; Pp.verbatim line ] - in - let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in - let* coqdep = - Super_context.resolve_program sctx "coqdep" ~dir ~loc:(Some loc) - ~hint:"opam install coq" - in - (* Coqdep has to be called in the stanza's directory *) - Super_context.add_rule ~loc sctx ~dir - (let open Action_builder.With_targets.O in - Action_builder.with_no_targets mlpack_rule - >>> Action_builder.(with_no_targets (goal source_rule)) - >>> Command.run ~dir:(Path.build dir) ~stdout_to coqdep file_flags) -let deps_of ~dir ~use_stdlib ~wrapper_name coq_module = - let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in +let parse_line ~dir ~boot_type line = + match String.lsplit2 line ~on:':' with + | None -> coqdep_invalid "split" line + | Some (basename, deps) -> + let target = List.hd @@ String.extract_blank_separated_words basename in + (* let depname, ext = Filename.split_extension ff in *) + let target = Path.relative (Path.build dir) target in + let deps = String.extract_blank_separated_words deps in + (* Add prelude deps for when stdlib is in scope and we are not actually + compiling the prelude *) + let deps = List.map ~f:(Path.relative (Path.build dir)) deps in + let deps = + match boot_type with + | `No_boot | `Bootstrap_prelude -> deps + | `Bootstrap lib -> + Path.relative (Path.build (Coq_lib.src_root lib)) "Init/Prelude.vo" + :: deps + in + (target, deps) + +let get_dep_map ~dir ~boot_type ~wrapper_name : + Path.t list Dep_map.t Action_builder.t = + let file = dep_theory_file ~dir ~wrapper_name in let open Action_builder.O in - let* boot_type = - Action_builder.of_memo - @@ boot_type ~dir ~use_stdlib ~wrapper_name coq_module - in - Action_builder.dyn_paths_unit - (Action_builder.map - (Action_builder.lines_of (Path.build stdout_to)) - ~f:(parse_coqdep ~dir ~boot_type ~coq_module)) + let f = parse_line ~dir ~boot_type in + Action_builder.lines_of (Path.build file) >>| fun lines -> + List.map ~f lines |> Dep_map.of_list |> function + | Ok map -> map + | Error (k, r1, r2) -> + User_error.raise + [ Pp.textf "problem with dup keys" + ; Pp.text (String.concat ~sep:"\n>> " lines) + ; Dyn.pp (Path.to_dyn k) + ; Dyn.pp (Dyn.list Path.to_dyn r1) + ; Dyn.pp (Dyn.list Path.to_dyn r2) + ] let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs coq_module = @@ -453,21 +391,37 @@ let setup_coqc_rule ~loc ~dir ~sctx ~coqc_dir ~file_targets ~stanza_flags coq_module = (* Process coqdep and generate rules *) let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in - let deps_of = deps_of ~dir ~use_stdlib ~wrapper_name coq_module in + (* let deps_of = deps_of ~dir ~use_stdlib ~wrapper_name coq_module in *) let* coqc = coqc ~loc ~dir ~sctx in - let target_obj_files = - Command.Args.Hidden_targets - (Coq_module.obj_files ~wrapper_name ~mode ~obj_files_mode:Coq_module.Build - ~obj_dir:dir coq_module - |> List.map ~f:fst) + let obj_files = + Coq_module.obj_files ~wrapper_name ~mode ~obj_files_mode:Coq_module.Build + ~obj_dir:dir coq_module + |> List.map ~f:fst in + let target_obj_files = Command.Args.Hidden_targets obj_files in let* args = generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs ~mode ~coq_prog:`Coqc coq_module in + let open Action_builder.O in + let vo_target = + Path.Build.set_extension ~ext:".vo" (Coq_module.source coq_module) + in + let deps_of = + get_dep_map ~dir ~boot_type ~wrapper_name >>| fun dep_map -> + match Dep_map.find dep_map (Path.build vo_target) with + | None -> + User_error.raise + [ Pp.textf "Dep_map.find failed for" + ; Dyn.pp (Coq_module.to_dyn coq_module) + ; Dyn.pp (Dep_map.to_dyn (Dyn.list Path.to_dyn) dep_map) + ] + | Some deps -> deps + in + let open Action_builder.With_targets.O in Super_context.add_rule ~loc ~dir sctx - (Action_builder.with_no_targets deps_of + (Action_builder.(with_no_targets (Action_builder.bind ~f:paths deps_of)) >>> Action_builder.With_targets.add ~file_targets @@ Command.run ~dir:(Path.build coqc_dir) coqc (target_obj_files :: args) (* The way we handle the transitive dependencies of .vo files is not safe for @@ -626,14 +580,9 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) = in let coqc_dir = (Super_context.context sctx).build_dir in let* mode = select_native_mode ~sctx ~dir s.buildable in - let theory_name = snd s.name in (* First we setup the rule calling coqdep *) setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name - ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule ~theory_name coq_modules - (* Next the rules filtering that file per module *) - >>> Memo.parallel_iter coq_modules - ~f:(setup_coqdep_for_mod_rule ~sctx ~dir ~loc ~wrapper_name) - (* Then we setup the coqc rules *) + ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule coq_modules >>> Memo.parallel_iter coq_modules ~f: (setup_coqc_rule ~loc ~dir ~sctx ~file_targets:[] ~stanza_flags @@ -798,10 +747,11 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents let lib_db = Scope.libs scope in ml_flags_and_ml_pack_rule ~context ~theories_deps ~lib_db s.buildable in + let loc = s.buildable.loc in + let use_stdlib = s.buildable.use_stdlib in let* mode = select_native_mode ~sctx ~dir s.buildable in - setup_coqdep_rule ~sctx ~loc:s.buildable.loc ~source_rule ~dir ~theories_deps - ~wrapper_name ~use_stdlib:s.buildable.use_stdlib ~ml_flags ~mlpack_rule - coq_module + setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name + ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule [ coq_module ] >>> setup_coqc_rule ~file_targets ~stanza_flags:s.buildable.flags ~sctx ~loc:s.buildable.loc ~coqc_dir:dir coq_module ~dir ~theories_deps ~mode ~wrapper_name ~use_stdlib:s.buildable.use_stdlib ~ml_flags @@ -825,3 +775,11 @@ let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module = generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog:`Coqtop ~stanza_flags:s.buildable.flags ~ml_flags ~theories_deps ~theory_dirs:Path.Build.Set.empty coq_module + +(* Version for export *) +let get_dep_map ~dir ~use_stdlib ~wrapper_name coq_module = + let open Action_builder.O in + let* boot_type = + Action_builder.of_memo (boot_type ~dir ~use_stdlib ~wrapper_name coq_module) + in + get_dep_map ~dir ~boot_type ~wrapper_name diff --git a/src/dune_rules/coq/coq_rules.mli b/src/dune_rules/coq/coq_rules.mli index cef75676357..61ed22baa12 100644 --- a/src/dune_rules/coq/coq_rules.mli +++ b/src/dune_rules/coq/coq_rules.mli @@ -5,14 +5,15 @@ open Import (* (c) INRIA 2020 *) (* Written by: Emilio Jesús Gallego Arias *) -(** [deps_of ~dir ~use_stdlib ~wrapper_name m] produces an action builder that - can be run to build all dependencies of the Coq module [m]. *) -val deps_of : +module Dep_map : Map.S with type key := Path.t + +(** [get_dep_map] produces a dep map for a theory *) +val get_dep_map : dir:Path.Build.t -> use_stdlib:bool -> wrapper_name:string -> Coq_module.t - -> unit Dune_engine.Action_builder.t + -> Path.t list Dep_map.t Dune_engine.Action_builder.t val coqdoc_directory_targets : dir:Path.Build.t -> Coq_stanza.Theory.t -> Loc.t Path.Build.Map.t diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t index 5c6449072cb..f142cea4912 100644 --- a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t @@ -8,7 +8,6 @@ dependencies. -> theory C in C -> theory A in A -> required by _build/default/A/A.theory.d - -> required by _build/default/A/a.v.d -> required by _build/default/A/a.vo -> required by _build/install/default/lib/coq/user-contrib/A/a.vo -> required by _build/default/A/A.install @@ -23,7 +22,6 @@ dependencies. -> theory A in A -> theory B in B -> required by _build/default/B/B.theory.d - -> 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/B/B.install @@ -38,7 +36,6 @@ dependencies. -> theory B in B -> theory C in C -> required by _build/default/C/C.theory.d - -> required by _build/default/C/c.v.d -> required by _build/default/C/c.vo -> required by _build/install/default/lib/coq/user-contrib/C/c.vo -> required by _build/default/C/C.install diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t index e5205c50118..390d8fce78a 100644 --- a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t @@ -9,7 +9,6 @@ dependency. -> required by theory B in B -> required by theory C in C -> required by _build/default/C/C.theory.d - -> required by _build/default/C/c.v.d -> required by _build/default/C/c.vo -> required by _build/install/default/lib/coq/user-contrib/C/c.vo -> required by _build/default/C/C.install diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t index 1edaac6b9df..b17a089ff93 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t @@ -7,7 +7,6 @@ Testing coqdoc when composed with a boot library A.theory.d a.glob a.v - a.v.d a.vo a.vok a.vos diff --git a/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t index a427fb7fe12..7e7c77da01e 100644 --- a/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t @@ -26,7 +26,6 @@ Note that this currently works due to a bug in @all detecting directory targets. META.base bar.glob bar.v - bar.v.d bar.vo bar.vok bar.vos @@ -35,7 +34,6 @@ Note that this currently works due to a bug in @all detecting directory targets. basic.theory.d foo.glob foo.v - foo.v.d foo.vo foo.vok foo.vos diff --git a/test/blackbox-tests/test-cases/coq/extract.t b/test/blackbox-tests/test-cases/coq/extract.t index 42405dd01d5..40f49461120 100644 --- a/test/blackbox-tests/test-cases/coq/extract.t +++ b/test/blackbox-tests/test-cases/coq/extract.t @@ -38,11 +38,11 @@ $ ls _build/default Datatypes.ml Datatypes.mli + DuneExtraction.theory.d extract.glob extract.ml extract.mli extract.v - extract.v.d extract.vo extract.vok extract.vos diff --git a/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t b/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t index 20097849b12..0609faa5632 100644 --- a/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t +++ b/test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t @@ -9,7 +9,7 @@ The META file for plugins is built before calling coqdep > (plugins bar.foo)) > EOF - $ dune build bar.v.d + $ dune build bar.theory.d $ ls _build/install/default/lib/bar META diff --git a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t index 78ac9a9e8b0..3ca04018313 100644 --- a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t +++ b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t @@ -6,7 +6,6 @@ You need to associate "private" to a package. -> required by theory public in public -> required by _build/default/public/public.theory.d - -> required by _build/default/public/b.v.d -> required by _build/default/public/b.vo -> required by _build/install/default/lib/coq/user-contrib/public/b.vo -> required by _build/default/public.install From d2d5e2e7129308b31451a0a39856cad546186968 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 13 Feb 2023 21:56:43 +0100 Subject: [PATCH 3/3] add changelog Signed-off-by: Ali Caglayan --- CHANGES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index cf3c9303c79..b1289c5c705 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,8 @@ Unreleased ---------- +- coqdep is now called once per theory (#7048, @Alizter) + - Add map_workspace_root dune-project stanza to allow disabling of mapping of workspace root to /workspace_root. (#6988, fixes #6929, @richardlford)