Merge pull request #11094 from rlepigre/coqdep-flags

Add support for `coqdep` flags.

doc/changes/11094.md

@@ -0,0 +1,2 @@
+- Add a `coqdep_flags` field to the `coq` field of the `env` stanza, and to the `coq.theory` stanza, allowing to configure `coqdep` flags.
+  (#11094, @rlepigre)

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,12 @@ 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. This field exists for transient
+  use-cases, in particular disabling ``coqdep`` warnings, but it should not be
+  used in normal operations. (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
@@ -347,6 +354,7 @@ The Coq lang can be modified by adding the following to a
 
 The supported Coq language versions (not the version of Coq) are:
 
+- ``0.10``: Support for the ``(coqdep_flags ...)`` field.
 - ``0.9``: Support for per-module flags with the ``(module_flags ...)``` field.
 - ``0.8``: Support for composition with installed Coq theories;
   support for ``vos`` builds.
@@ -833,6 +841,11 @@ 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. As noted in the documentation
+  of the ``(coq.theory (coqdep_flags <flags>))`` field, changing the ``coqdep``
+  flags is discouraged.
 - ``(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.

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
 ;;

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
 

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 ]
 ;;

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
   }
 

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,15 @@ 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
+    coqdep_flags ~dir ~stanza_coqdep_flags ~expander
+  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 +996,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 +1218,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

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
        })
   ;;

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
     }
 

test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.17)
+(using coq 0.10)

test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune.disabled

@@ -0,0 +1,4 @@
+(env
+ (_
+  (coq
+   (coqdep_flags (:standard --global-flag1 --global-flag2)))))

test/blackbox-tests/test-cases/coq/coqdep-flags.t/run.t

@@ -0,0 +1,29 @@
+By default the coqdep flags are empty.
+
+  $ cp theories/dune.noflags theories/dune
+  $ dune build theories/.basic.theory.d
+
+We use non-exising coqdep flags, so compilation fails.
+
+  $ mv dune.disabled dune
+  $ dune build theories/.basic.theory.d
+  *** Warning: unknown option --global-flag1
+  *** Warning: unknown option --global-flag2
+
+We then add more flags locally to the theory.
+
+  $ rm -f theories/dune
+  $ cp theories/dune.flags theories/dune
+  $ dune build theories/.basic.theory.d
+  *** Warning: unknown option --global-flag1
+  *** Warning: unknown option --global-flag2
+  *** Warning: unknown option --local-flag1
+  *** Warning: unknown option --local-flag2
+
+Finally we remove the toplevel dune file which sets some flags, but keep the
+theory-local flags only.
+
+  $ rm -f dune
+  $ dune build theories/.basic.theory.d
+  *** Warning: unknown option --local-flag1
+  *** Warning: unknown option --local-flag2

test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/bar.v

@@ -0,0 +1,3 @@
+From basic Require Import foo.
+
+Definition mynum (i : mynat) := 3.

test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.flags

@@ -0,0 +1,3 @@
+(coq.theory
+ (name basic)
+ (coqdep_flags (:standard --local-flag1 --local-flag2)))

test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.noflags

@@ -0,0 +1,2 @@
+(coq.theory
+ (name basic))

test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/foo.v

@@ -0,0 +1 @@
+Definition mynat := nat.

test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t

@@ -45,5 +45,5 @@ This test is currently broken due to the workspace resolution being faulty #5899
   1 | (coq.theory
   2 |  (name foo))
   Error: 'coq.theory' is available only when coq is enabled in the dune-project
-  file. You must enable it using (using coq 0.9) in your dune-project file.
+  file. You must enable it using (using coq 0.10) in your dune-project file.
   [1]

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

@@ -17,5 +17,5 @@ good when the coq extension is not enabled.
   1 | (coq.theory
   2 |  (name foo))
   Error: 'coq.theory' is available only when coq is enabled in the dune-project
-  file. You must enable it using (using coq 0.9) in your dune-project file.
+  file. You must enable it using (using coq 0.10) in your dune-project file.
   [1]

test/blackbox-tests/test-cases/workspaces/workspace-env.t/run.t

@@ -13,6 +13,7 @@ Workspaces also allow you to set the env for a context:
   (menhir_flags ())
   (menhir_explain ())
   (coq_flags (-q))
+  (coqdep_flags ())
   (coqdoc_flags (--toc))
   (js_of_ocaml_flags ())
   (js_of_ocaml_build_runtime_flags ())