[coq] Add "-q" to default flags.

Fixes #3924 , and a bug where `:standard` was not properly set in theory flags, as they should be inherited from the ones set in the profile; thanks Rudi Gringerb. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ocaml · Nov 25, 2020 · 307b0e4 · 307b0e4
1 parent 555fd33
commit 307b0e4
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 9 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -86,6 +86,11 @@ Unreleased
 - Allow (formatting ...) field in (env ...) stanza to set per-directory
   formatting specification. (#3942, @nojb)
 
+- [coq] In `coq.theory`, `:standard` for the `flags` field now uses the
+  flags set in `env` profile flags (#3931 , @ejgallego @rgrinberg)
+
+- [coq] Add `-q` flag to `:standard` `coqc` flags , fixes #3924, (#3931 , @ejgallego)
+
 2.7.1 (2/09/2020)
 -----------------
 

diff --git a/doc/dune-files.rst b/doc/dune-files.rst
@@ -1653,7 +1653,9 @@ The stanza will build all ``.v`` files on the given directory. The semantics of
   customary in the make-based Coq package ecosystem. For
   compatibility, we also install under the ``user-contrib`` prefix the
   ``.cmxs`` files appearing in ``<ocaml_libraries>``,
-- ``<coq_flags>`` will be passed to ``coqc`` as command-line options,
+- ``<coq_flags>`` will be passed to ``coqc`` as command-line
+  options. ``:standard`` is taken from the value set in the ``(coq (flags <flags>))``
+  field in ``env`` profile. See :ref:`_dune-env` for more information.
 - the path to installed locations of ``<ocaml_libraries>`` will be passed to
   ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq
   theory to depend on a ML plugin,

diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
@@ -101,15 +101,14 @@ module Context = struct
     let dir = Path.build (snd t.coqc) in
     Command.run ~dir ?stdout_to (fst t.coqc) args
 
+  let standard_coq_flags = Build.return [ "-q" ]
+
   let coq_flags t =
-    Build.(
-      map ~f:List.concat
-        (all
-           [ Expander.expand_and_eval_set t.expander t.profile_flags
-               ~standard:(Build.return [])
-           ; Expander.expand_and_eval_set t.expander t.buildable.flags
-               ~standard:(Build.return [])
-           ]))
+    let standard = standard_coq_flags in
+    let standard =
+      Expander.expand_and_eval_set t.expander t.profile_flags ~standard
+    in
+    Expander.expand_and_eval_set t.expander t.buildable.flags ~standard
 
   let theories_flags =
     let setup_theory_flag lib =