Merge branch 'main' into ps/rr/fix_install___respect_display_options

Signed-off-by: Emilio Jesús Gallego Arias <e+git@x80.org>

CHANGES.md

@@ -1,7 +1,9 @@
 Unreleased
 ----------
 
-- dune install now respects --display=quiet mode (#7116, fixes #4573, fixes #7106,
+- Fix preludes not being recorded as dependencies in the `(mdx)` stanza (#7109,
+  fixes #7077, @emillon).
+  - dune install now respects --display=quiet mode (#7116, fixes #4573, fixes #7106,
   @Alizter)
 
 3.7.0 (2023-02-17)

src/dune_engine/dialect.ml

@@ -1,5 +1,8 @@
 open Import
 module Action = Dune_lang.Action
+module Ml_kind = Ocaml.Ml_kind
+module Cm_kind = Ocaml.Cm_kind
+module Mode = Ocaml.Mode
 
 module File_kind = struct
   type t =

src/dune_engine/dialect.mli

@@ -1,4 +1,5 @@
 open Import
+open Ocaml
 
 (** Dialects
 

src/dune_engine/dune

@@ -12,7 +12,6 @@
   incremental_cycles
   dag
   memo
-  xdg
   ocaml
   dune_re
   threads.posix
@@ -21,7 +20,6 @@
   dune_cache
   dune_cache_storage
   dune_glob
-  ocaml_config
   chrome_trace
   dune_stats
   dune_action_plugin

src/dune_engine/import.ml

@@ -8,9 +8,6 @@ module Stringlike = Dune_util.Stringlike
 module Stringlike_intf = Dune_util.Stringlike_intf
 module Persistent = Dune_util.Persistent
 module Value = Dune_util.Value
-module Ml_kind = Ocaml.Ml_kind
-module Cm_kind = Ocaml.Cm_kind
-module Mode = Ocaml.Mode
 module Config = Dune_util.Config
 module Predicate_lang = Dune_lang.Predicate_lang
 module String_with_vars = Dune_lang.String_with_vars

src/dune_rules/coq/coq_rules.ml

@@ -269,7 +269,7 @@ let boot_type ~dir ~use_stdlib ~wrapper_name coq_module =
   else `Bootstrap_prelude
 
 let dep_theory_file ~dir ~wrapper_name =
-  Path.Build.relative 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

src/dune_rules/mdx.ml

@@ -145,13 +145,20 @@ module Prelude = struct
     in
     enter decode_env <|> decode_default
 
+  (** Generated program will read some files when it runs. *)
+  let runtime_deps ~dir t : _ Command.Args.t =
+    match t with
+    | Default file | Env { env = _; file } ->
+      Hidden_deps
+        (Dep.Set.of_files [ Path.build (Path.Build.append_local dir file) ])
+
   let to_args ~dir t : _ Command.Args.t list =
-    let bpath p = Path.build (Path.Build.append_local dir p) in
     match t with
-    | Default file -> [ A "--prelude"; Dep (bpath file) ]
+    | Default file ->
+      [ A "--prelude"; Dep (Path.build (Path.Build.append_local dir file)) ]
     | Env { env; file } ->
       let arg = sprintf "%s:%s" env (Path.Local.to_string file) in
-      [ A "--prelude"; A arg; Hidden_deps (Dep.Set.of_files [ bpath file ]) ]
+      [ A "--prelude"; A arg; runtime_deps ~dir t ]
 end
 
 type t =
@@ -317,7 +324,11 @@ let gen_rules_for_single_file stanza ~sctx ~dir ~expander ~mdx_prog
            generated executable *)
         let open Command.Args in
         match mdx_prog_gen with
-        | Some prog -> (Ok (Path.build prog), [ Dep (Path.build files.src) ])
+        | Some prog ->
+          ( Ok (Path.build prog)
+          , [ Dep (Path.build files.src)
+            ; S (List.map ~f:(Prelude.runtime_deps ~dir) stanza.preludes)
+            ] )
         | None ->
           let prelude_args =
             List.concat_map stanza.preludes ~f:(Prelude.to_args ~dir)

test/blackbox-tests/test-cases/coq/base-unsound.t/run.t

@@ -1,4 +1,4 @@
   $ dune build --display short --profile unsound --debug-dependency-path @all
-        coqdep basic.theory.d
+        coqdep .basic.theory.d
           coqc foo.{glob,vo}
           coqc bar.{glob,vo}

test/blackbox-tests/test-cases/coq/base.t/run.t

@@ -1,5 +1,5 @@
   $ dune build --display short --debug-dependency-path @all
-        coqdep basic.theory.d
+        coqdep .basic.theory.d
           coqc foo.{glob,vo}
           coqc bar.{glob,vo}
 

test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t

@@ -4,7 +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.theory.d
+  -> required by _build/default/A/.A.theory.d
   -> required by alias A/all
   -> required by alias default
   [1]

test/blackbox-tests/test-cases/coq/compose-installed.t/run.t

@@ -12,7 +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.theory.d
+  -> required by _build/default/.A.theory.d
   -> required by alias all
   -> required by alias default
   [1]

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/thy1.theory.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/thy2.theory.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}

test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t

@@ -7,10 +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.vo
-  -> required by _build/install/default/lib/coq/user-contrib/A/a.vo
-  -> required by _build/default/A/A.install
+  -> required by _build/default/A/.A.theory.d
   -> required by alias A/all
   -> required by alias A/default
   [1]
@@ -21,10 +18,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.vo
-  -> required by _build/install/default/lib/coq/user-contrib/B/b.vo
-  -> required by _build/default/B/B.install
+  -> required by _build/default/B/.B.theory.d
   -> required by alias B/all
   -> required by alias B/default
   [1]
@@ -35,10 +29,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.vo
-  -> required by _build/install/default/lib/coq/user-contrib/C/c.vo
-  -> required by _build/default/C/C.install
+  -> required by _build/default/C/.C.theory.d
   -> required by alias C/all
   -> required by alias C/default
   [1]

test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t

@@ -8,10 +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.vo
-  -> required by _build/install/default/lib/coq/user-contrib/C/c.vo
-  -> required by _build/default/C/C.install
+  -> required by _build/default/C/.C.theory.d
   -> required by alias C/all
   -> required by alias C/default
   [1]

test/blackbox-tests/test-cases/coq/compose-self.t/run.t

@@ -2,7 +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.theory.d
+  -> required by _build/default/A/.A.theory.d
   -> required by alias A/all
   -> required by alias default
   [1]

test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t

@@ -14,8 +14,8 @@
   > Definition doo := a.foo.
   > EOF
   $ dune build --display short --debug-dependency-path
-        coqdep a/a.theory.d
-        coqdep b/b.theory.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}
@@ -25,5 +25,5 @@
   > Definition zoo := 4.
   > EOF
   $ dune build --display short --debug-dependency-path
-        coqdep b/b.theory.d
+        coqdep b/.b.theory.d
           coqc b/Nb_b.{cmi,cmxs},b/b.{glob,vo}

test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t

@@ -20,7 +20,6 @@ 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
@@ -53,7 +52,6 @@ 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

test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t

@@ -4,7 +4,6 @@ Testing coqdoc when composed with a boot library
 
   $ ls _build/default/A
   A.html
-  A.theory.d
   a.glob
   a.v
   a.vo

test/blackbox-tests/test-cases/coq/coqdoc.t/run.t

@@ -31,7 +31,6 @@ 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.vo

test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t

@@ -19,15 +19,15 @@ 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/basic.theory.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
   -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 clean
   $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v)
   Entering directory '..'
-        coqdep dir/basic.theory.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

test/blackbox-tests/test-cases/coq/extract.t

@@ -38,7 +38,6 @@
   $ ls _build/default
   Datatypes.ml
   Datatypes.mli
-  DuneExtraction.theory.d
   extract.glob
   extract.ml
   extract.mli

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/Plugin.theory.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}

test/blackbox-tests/test-cases/coq/native-compose.t/run.t

@@ -1,6 +1,6 @@
   $ dune build --profile=release --display short --debug-dependency-path @all
-        coqdep bar/bar.theory.d
-        coqdep foo/foo.theory.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}

test/blackbox-tests/test-cases/coq/native-single.t/run.t

@@ -1,5 +1,5 @@
   $ dune build --profile=release --display short --debug-dependency-path @all
-        coqdep basic.theory.d
+        coqdep .basic.theory.d
           coqc Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
           coqc Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
 

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 basic.theory.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:

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.theory.d
+  $ dune build .bar.theory.d
   $ ls _build/install/default/lib/bar
   META
 

test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t

@@ -5,7 +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/.public.theory.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

test/blackbox-tests/test-cases/coq/rec-module.t/run.t

@@ -1,5 +1,5 @@
   $ dune build --display short --debug-dependency-path @all
-        coqdep rec_module.theory.d
+        coqdep .rec_module.theory.d
           coqc b/foo.{glob,vo}
           coqc c/d/bar.{glob,vo}
           coqc c/ooo.{glob,vo}

test/blackbox-tests/test-cases/mdx-stanza/github7077.t

@@ -0,0 +1,39 @@
+When mdx is used to generate a program, the program will read the preludes at
+run time. This test makes sure that this is recorded as a dependency.
+
+  $ cat > dune << EOF
+  > (mdx (preludes prelude.ml))
+  > EOF
+
+  $ cat > dune-project << EOF
+  > (lang dune 3.6)
+  > (using mdx 0.3)
+  > EOF
+
+  $ cat > prelude.ml << EOF
+  > let foo () = 1
+  > EOF
+
+  $ cat > README.md << 'EOF'
+  > ```ocaml
+  > # foo ();;
+  > - : int = 1
+  > ```
+  > EOF
+
+  $ dune runtest
+
+  $ echo 'let foo () = 2' > prelude.ml
+
+  $ dune runtest --auto-promote
+  File "README.md", line 1, characters 0-0:
+  Error: Files _build/default/README.md and
+  _build/default/.mdx/README.md.corrected differ.
+  Promoting _build/default/.mdx/README.md.corrected to README.md.
+  [1]
+
+  $ cat README.md
+  ```ocaml
+  # foo ();;
+  - : int = 2
+  ```