Add .glob files as coqc targets as well

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
ocaml · Aug 21, 2020 · af82d8c · af82d8c
1 parent 8d30a98
commit af82d8c
Show file tree

Hide file tree

Showing 8 changed files with 19 additions and 11 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,7 +1,8 @@
 Unreleased
 ----------
 
-- Add missing `.aux` targets to coq rules (3721, fixes #3437, @rgrinberg)
+- Add missing `.aux` & `.glob` targets to coq rules (3721, fixes #3437,
+  @rgrinberg)
 
 2.7.0 (13/08/2020)
 ------------------

diff --git a/src/dune/coq_module.ml b/src/dune/coq_module.ml
@@ -45,6 +45,10 @@ let aux_file x ~obj_dir =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir ("." ^ x.name ^ ".aux")
 
+let glob_file x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  Path.Build.relative vo_dir (x.name ^ ".glob")
+
 let obj_file x ~obj_dir =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir (x.name ^ ".vo")

diff --git a/src/dune/coq_module.mli b/src/dune/coq_module.mli
@@ -40,6 +40,8 @@ val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
 val aux_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
+val glob_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+
 val obj_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
 val to_dyn : t -> Dyn.t

diff --git a/src/dune/coq_rules.ml b/src/dune/coq_rules.ml
@@ -266,7 +266,8 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
   let file_flags =
     let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module in
     let aux = Coq_module.aux_file ~obj_dir:cctx.dir coq_module in
-    [ Command.Args.Hidden_targets [ object_to; aux ]
+    let glob = Coq_module.glob_file ~obj_dir:cctx.dir coq_module in
+    [ Command.Args.Hidden_targets [ object_to; aux; glob ]
     ; S file_flags
     ; Command.Args.Dep (Path.build source)
     ]

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
@@ -1,5 +1,5 @@
   $ dune build --display short --profile unsound --debug-dependency-path @all
         coqdep bar.v.d
         coqdep foo.v.d
-          coqc .foo.aux,foo.vo
-          coqc .bar.aux,bar.vo
+          coqc .foo.aux,foo.{glob,vo}
+          coqc .bar.aux,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
@@ -1,8 +1,8 @@
   $ dune build --display short --debug-dependency-path @all
         coqdep bar.v.d
         coqdep foo.v.d
-          coqc .foo.aux,foo.vo
-          coqc .bar.aux,bar.vo
+          coqc .foo.aux,foo.{glob,vo}
+          coqc .bar.aux,bar.{glob,vo}
 
   $ dune build --debug-dependency-path @default
   lib: [

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
@@ -22,4 +22,4 @@
       ocamlopt src_b/ml_plugin_b.{a,cmxa}
       ocamlopt src_a/ml_plugin_a.cmxs
       ocamlopt src_b/ml_plugin_b.cmxs
-          coqc theories/.a.aux,theories/a.vo
+          coqc theories/.a.aux,theories/a.{glob,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
@@ -3,10 +3,10 @@
         coqdep b/foo.v.d
         coqdep c/d/bar.v.d
         coqdep c/ooo.v.d
-          coqc b/.foo.aux,b/foo.vo
-          coqc c/d/.bar.aux,c/d/bar.vo
-          coqc c/.ooo.aux,c/ooo.vo
-          coqc a/.bar.aux,a/bar.vo
+          coqc b/.foo.aux,b/foo.{glob,vo}
+          coqc c/d/.bar.aux,c/d/bar.{glob,vo}
+          coqc c/.ooo.aux,c/ooo.{glob,vo}
+          coqc a/.bar.aux,a/bar.{glob,vo}
 
   $ dune build --debug-dependency-path @default
   lib: [