Add support for coqdep flags.

This includes the following: - A [coqdep_flags] field in the [env] stanza (under [coq]). - A [coqdep_flags] field in the [coq.theory] stanza. Signed-off-by: Rodolphe Lepigre <[email protected]>
ocaml · Nov 4, 2024 · 7e7ed7d · 7e7ed7d
1 parent b409963
commit 7e7ed7d
Show file tree

Hide file tree

Showing 15 changed files with 139 additions and 7 deletions.
diff --git a/doc/coq.rst b/doc/coq.rst
@@ -67,6 +67,7 @@ The Coq theory stanza is very similar in form to the OCaml
      (plugins <ocaml_plugins>)
      (flags <coq_flags>)
      (modules_flags <flags_map>)
+     (coqdep_flags <coqdep_flags>)
      (coqdoc_flags <coqdoc_flags>)
      (stdlib <stdlib_included>)
      (mode <coq_native_mode>)
@@ -134,6 +135,11 @@ The semantics of the fields are:
   ...)`` as to propagate the default flags. (Appeared in :ref:`Coq
   lang 0.9<coq-lang>`)
 
+- ``<coqdep_flags>`` are extra user-configurable flags passed to ``coqdep``. The
+  default value for ``:standard`` is empty. (Appeared in :ref:`Coq
+  lang 0.10<coq-lang>`)
+
+
 - ``<coqdoc_flags>`` are extra user-configurable flags passed to ``coqdoc``. The
   default value for ``:standard`` is ``--toc``. The ``--html`` or ``--latex``
   flags are passed separately depending on which mode is target. See the section
@@ -833,6 +839,9 @@ with the following values for ``<coq_fields>``:
 - ``(flags <flags>)``: The default flags passed to ``coqc``. The default value
   is ``-q``. Values set here become the ``:standard`` value in the
   ``(coq.theory (flags <flags>))`` field. 
+- ``(coqdep_flags <flags>)``: The default flags passed to ``coqdep``. The default
+  value is empty. Values set here become the ``:standard`` value in the
+  ``(coq.theory (coqdep_flags <flags>))`` field.
 - ``(coqdoc_flags <flags>)``: The default flags passed to ``coqdoc``. The default
   value is ``--toc``. Values set here become the ``:standard`` value in the
   ``(coq.theory (coqdoc_flags <flags>))`` field.
diff --git a/src/dune_rules/coq/coq_env.ml b/src/dune_rules/coq/coq_env.ml
@@ -3,16 +3,19 @@ open Dune_lang.Decoder
 
 type t =
   { flags : Ordered_set_lang.Unexpanded.t
+  ; coqdep_flags : Ordered_set_lang.Unexpanded.t
   ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
   }
 
 let default =
   { flags = Ordered_set_lang.Unexpanded.standard
+  ; coqdep_flags = Ordered_set_lang.Unexpanded.standard
   ; coqdoc_flags = Ordered_set_lang.Unexpanded.standard
   }
 ;;
 
 let flags t = t.flags
+let coqdep_flags t = t.coqdep_flags
 let coqdoc_flags t = t.coqdoc_flags
 
 let decode =
@@ -24,15 +27,20 @@ let decode =
           Ordered_set_lang.Unexpanded.field
             "flags"
             ~check:(Dune_lang.Syntax.since Stanza.syntax (2, 7))
+        and+ coqdep_flags =
+          Ordered_set_lang.Unexpanded.field
+            "coqdep_flags"
+            ~check:(Dune_lang.Syntax.since Stanza.syntax (3, 17))
         and+ coqdoc_flags =
           Ordered_set_lang.Unexpanded.field
             "coqdoc_flags"
             ~check:(Dune_lang.Syntax.since Stanza.syntax (3, 13))
         in
-        { flags; coqdoc_flags }))
+        { flags; coqdep_flags; coqdoc_flags }))
 ;;
 
-let equal { flags; coqdoc_flags } t =
+let equal { flags; coqdep_flags; coqdoc_flags } t =
   Ordered_set_lang.Unexpanded.equal flags t.flags
+  && Ordered_set_lang.Unexpanded.equal coqdep_flags t.coqdep_flags
   && Ordered_set_lang.Unexpanded.equal coqdoc_flags t.coqdoc_flags
 ;;
diff --git a/src/dune_rules/coq/coq_env.mli b/src/dune_rules/coq/coq_env.mli
@@ -11,6 +11,9 @@ val default : t
 (** Flags for Coq binaries. *)
 val flags : t -> Ordered_set_lang.Unexpanded.t
 
+(** Flags for coqdep *)
+val coqdep_flags : t -> Ordered_set_lang.Unexpanded.t
+
 (** Flags for coqdoc *)
 val coqdoc_flags : t -> Ordered_set_lang.Unexpanded.t
 

diff --git a/src/dune_rules/coq/coq_flags.ml b/src/dune_rules/coq/coq_flags.ml
@@ -2,13 +2,14 @@ open Import
 
 type t =
   { coq_flags : string list
+  ; coqdep_flags : string list
   ; coqdoc_flags : string list
   }
 
-let default = { coq_flags = [ "-q" ]; coqdoc_flags = [ "--toc" ] }
+let default = { coq_flags = [ "-q" ]; coqdep_flags = []; coqdoc_flags = [ "--toc" ] }
 
-let dump { coq_flags; coqdoc_flags } =
+let dump { coq_flags; coqdep_flags; coqdoc_flags } =
   List.map
     ~f:Dune_lang.Encoder.(pair string (list string))
-    [ "coq_flags", coq_flags; "coqdoc_flags", coqdoc_flags ]
+    [ "coq_flags", coq_flags; "coqdep_flags", coqdep_flags; "coqdoc_flags", coqdoc_flags ]
 ;;
diff --git a/src/dune_rules/coq/coq_flags.mli b/src/dune_rules/coq/coq_flags.mli
@@ -1,5 +1,6 @@
 type t =
   { coq_flags : string list
+  ; coqdep_flags : string list
   ; coqdoc_flags : string list
   }
 

diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml
@@ -141,6 +141,15 @@ let coq_env =
             x.coq_flags
           in
           Expander.expand_and_eval_set expander (Coq_env.flags config.coq) ~standard
+        and+ coqdep_flags =
+          let standard =
+            let+ x = Action_builder.of_memo_join parent in
+            x.coqdep_flags
+          in
+          Expander.expand_and_eval_set
+            expander
+            (Coq_env.coqdep_flags config.coq)
+            ~standard
         and+ coqdoc_flags =
           let standard =
             let+ x = Action_builder.of_memo_join parent in
@@ -151,7 +160,7 @@ let coq_env =
             (Coq_env.coqdoc_flags config.coq)
             ~standard
         in
-        { Coq_flags.coq_flags; coqdoc_flags })
+        { Coq_flags.coq_flags; coqdep_flags; coqdoc_flags })
   in
   fun ~dir ->
     (let* () = Memo.return () in
@@ -176,6 +185,16 @@ let coq_flags ~dir ~stanza_flags ~per_file_flags ~expander =
   Expander.expand_and_eval_set expander flags_to_expand ~standard
 ;;
 
+let coqdep_flags ~dir ~stanza_coqdep_flags ~expander =
+  Expander.expand_and_eval_set
+    expander
+    stanza_coqdep_flags
+    ~standard:
+      (Action_builder.map
+         ~f:(fun { Coq_flags.coqdep_flags; _ } -> coqdep_flags)
+         (coq_env ~dir))
+;;
+
 let coqdoc_flags ~dir ~stanza_coqdoc_flags ~expander =
   Expander.expand_and_eval_set
     expander
@@ -474,6 +493,7 @@ let setup_coqdep_for_theory_rule
   ~ml_flags
   ~mlpack_rule
   ~boot_flags
+  ~stanza_coqdep_flags
   coq_modules
   =
   (* coqdep needs the full source + plugin's mlpack to be present :( *)
@@ -484,7 +504,16 @@ let setup_coqdep_for_theory_rule
     ; Deps sources
     ]
   in
-  let coqdep_flags = Command.Args.Dyn boot_flags :: file_flags in
+  let extra_coqdep_flags =
+    (* Standard flags for coqdep *)
+    let open Action_builder.O in
+    let* expander = Action_builder.of_memo @@ Super_context.expander sctx ~dir in
+    let standard = coqdep_flags ~dir ~stanza_coqdep_flags ~expander in
+    Expander.expand_and_eval_set expander stanza_coqdep_flags ~standard
+  in
+  let coqdep_flags =
+    Command.Args.Dyn boot_flags :: Command.Args.dyn extra_coqdep_flags :: file_flags
+  in
   let stdout_to = dep_theory_file ~dir ~wrapper_name in
   let* coqdep =
     Super_context.resolve_program_memo
@@ -968,6 +997,7 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) =
     ~ml_flags
     ~mlpack_rule
     ~boot_flags
+    ~stanza_coqdep_flags:s.coqdep_flags
     coq_modules
   >>> Memo.parallel_iter
         coq_modules
@@ -1189,6 +1219,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Extraction.t
     ~ml_flags
     ~mlpack_rule
     ~boot_flags
+    ~stanza_coqdep_flags:Ordered_set_lang.Unexpanded.standard
     [ coq_module ]
   >>> setup_coqc_rule
         ~scope

diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml
@@ -14,6 +14,7 @@ let coq_syntax =
     ; (0, 7), `Since (3, 7)
     ; (0, 8), `Since (3, 8)
     ; (0, 9), `Since (3, 16)
+    ; (0, 10), `Since (3, 17)
     ]
 ;;
 
@@ -169,6 +170,7 @@ module Theory = struct
     ; boot : bool
     ; enabled_if : Blang.t
     ; buildable : Buildable.t
+    ; coqdep_flags : Ordered_set_lang.Unexpanded.t
     ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
     }
 
@@ -249,6 +251,10 @@ module Theory = struct
            (Dune_lang.Syntax.since coq_syntax (0, 9) >>> Per_file.decode)
        and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None ()
        and+ buildable = Buildable.decode
+       and+ coqdep_flags =
+         Ordered_set_lang.Unexpanded.field
+           "coqdep_flags"
+           ~check:(Dune_lang.Syntax.since coq_syntax (0, 10))
        and+ coqdoc_flags =
          Ordered_set_lang.Unexpanded.field
            "coqdoc_flags"
@@ -266,6 +272,7 @@ module Theory = struct
        ; boot
        ; buildable
        ; enabled_if
+       ; coqdep_flags
        ; coqdoc_flags
        })
   ;;

diff --git a/src/dune_rules/coq/coq_stanza.mli b/src/dune_rules/coq/coq_stanza.mli
@@ -35,6 +35,7 @@ module Theory : sig
     ; boot : bool
     ; enabled_if : Blang.t
     ; buildable : Buildable.t
+    ; coqdep_flags : Ordered_set_lang.Unexpanded.t
     ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
     }
 

diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune-project b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.17)
+(using coq 0.10)
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune.disabled b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune.disabled
@@ -0,0 +1,4 @@
+(env
+ (_
+  (coq
+   (coqdep_flags (:standard -w +all)))))
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/run.t b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/run.t
@@ -0,0 +1,55 @@
+By default the coqdep flags are empty, and missing files only lead to a simple
+warning.
+
+  $ cp theories/dune.noflags theories/dune
+  $ dune build theories/.basic.theory.d
+  Warning: in file bar.v, library baz is required
+           from root basic and has not been found in the loadpath!
+           [module-not-found,filesystem,default]
+
+We define coqdep flags that turn all warnings into errors, which leads to the
+above warning being turned into an error.
+
+  $ mv dune.disabled dune
+  $ dune build theories/.basic.theory.d
+  File "theories/dune", lines 1-2, characters 0-26:
+  1 | (coq.theory
+  2 |  (name basic))
+  *** Error: in file bar.v, library baz is required
+             from root basic and has not been found in the loadpath!
+             [module-not-found,filesystem,default]
+  [1]
+
+We then add the same flag (now duplicated) to the theory, which should not
+change anything.
+
+  $ rm -f theories/dune
+  $ cp theories/dune.flags theories/dune
+  $ dune build theories/.basic.theory.d
+  File "theories/dune", lines 1-3, characters 0-62:
+  1 | (coq.theory
+  2 |  (name basic)
+  3 |  (coqdep_flags (:standard -w +all)))
+  *** Error: in file bar.v, library baz is required
+             from root basic and has not been found in the loadpath!
+             [module-not-found,filesystem,default]
+  [1]
+
+Finally we remove the toplevel dune file which sets the flags globally, but
+keep the theory-local flags, so the behavior does not change.
+
+  $ rm -f dune
+  $ dune build theories/.basic.theory.d
+  File "theories/dune", lines 1-3, characters 0-62:
+  1 | (coq.theory
+  2 |  (name basic)
+  3 |  (coqdep_flags (:standard -w +all)))
+  *** Error: in file bar.v, library baz is required
+             from root basic and has not been found in the loadpath!
+             [module-not-found,filesystem,default]
+  [1]
+
+Creating the missing file fixes the error.
+
+  $ touch theories/baz.v
+  $ dune build theories/.basic.theory.d
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/bar.v b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/bar.v
@@ -0,0 +1,4 @@
+From basic Require Import foo.
+From basic Require Import baz.
+
+Definition mynum (i : mynat) := 3.
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.flags b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.flags
@@ -0,0 +1,3 @@
+(coq.theory
+ (name basic)
+ (coqdep_flags (:standard -w +all)))
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.noflags b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.noflags
@@ -0,0 +1,2 @@
+(coq.theory
+ (name basic))
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/foo.v b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/foo.v
@@ -0,0 +1 @@
+Definition mynat := nat.