feature(coq): omit -q flag during dune coq top

Signed-off-by: Ali Caglayan <[email protected]>
ocaml · Jan 21, 2023 · febe2aa · febe2aa
1 parent fc0769e
commit febe2aa
Show file tree

Hide file tree

Showing 6 changed files with 24 additions and 11 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -65,6 +65,9 @@ Unreleased
 - Remove "Entering Directory" messages for `$ dune install`. (#6513,
   @rgrinberg)
 
+- Stop passing `-q` flag in `dune coq top`, which allows for `.coqrc` to be
+  loaded. (#6848, fixes #6847, @Alizter)
+
 - Fix missing dependencies when detecting the kind of C compiler we're using
   (#6610, fixes #6415, @emillon)
 

diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml
@@ -46,9 +46,13 @@ let rec resolve_first lib_db = function
     | Some l -> Resolve.Memo.lift l
     | None -> resolve_first lib_db l)
 
-let coq_flags ~dir ~stanza_flags ~expander ~sctx =
+let coq_flags ~dir ~stanza_flags ~expander ~sctx ~default =
   let open Action_builder.O in
-  let* standard = Action_builder.of_memo @@ Super_context.coq ~dir sctx in
+  let* env_flags = Action_builder.of_memo @@ Super_context.coq ~dir sctx in
+  let standard =
+    let+ env_flags = env_flags in
+    env_flags @ default
+  in
   Expander.expand_and_eval_set expander stanza_flags ~standard
 
 let theories_flags ~theories_deps =
@@ -345,10 +349,16 @@ let deps_of ~dir ~use_stdlib ~wrapper_name coq_module =
 
 let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog
     ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs coq_module =
+  (* stanza flags together with env and default (-q)*)
   let+ coq_stanza_flags =
     let+ expander = Super_context.expander sctx ~dir in
     let coq_flags = coq_flags ~expander ~dir ~stanza_flags ~sctx in
-    Command.Args.dyn coq_flags (* stanza flags *)
+    let default =
+      match coq_prog with
+      | `Coqtop -> []
+      | _ -> [ "-q" ]
+    in
+    Command.Args.dyn (coq_flags ~default)
   in
   let coq_native_flags =
     coqc_native_flags ~sctx ~dir ~theories_deps ~theory_dirs ~mode

diff --git a/src/dune_rules/env_node.ml b/src/dune_rules/env_node.ml
@@ -202,7 +202,7 @@ let make ~dir ~inherit_from ~scope ~config_stanza ~profile ~expander
         Memo.return
           { warnings = Option.value config.odoc.warnings ~default:warnings })
   in
-  let default_coq_flags = Action_builder.return [ "-q" ] in
+  let default_coq_flags = Action_builder.return [] in
   let coq : Coq.t Action_builder.t Memo.Lazy.t =
     inherited ~field:coq ~root:default_coq_flags (fun flags ->
         let+ expander = Memo.Lazy.force expander in

diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t
@@ -3,6 +3,6 @@ Checking that we compute the directory and file for dune coq top correctly
   $ dune build theories/c.vo
   $ dune build theories/b/b.vo
   $ dune coq top --toplevel=echo theories/c.v
-  -topfile $TESTCASE_ROOT/_build/default/theories/c.v -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/theories foo
+  -topfile $TESTCASE_ROOT/_build/default/theories/c.v -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/theories foo
   $ dune coq top --toplevel=echo theories/b/b.v
-  -topfile $TESTCASE_ROOT/_build/default/theories/b/b.v -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/theories foo
+  -topfile $TESTCASE_ROOT/_build/default/theories/b/b.v -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/theories foo
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t
@@ -22,19 +22,19 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
         coqdep dir/bar.v.d
         coqdep dir/foo.v.d
           coqc dir/foo.{glob,vo}
-  -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic
+  -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 -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic
+  -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/bar.v.d
         coqdep dir/foo.v.d
           coqc dir/foo.{glob,vo}
   Leaving directory '..'
-  -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic
+  -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
   $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v)
   Entering directory '..'
   Leaving directory '..'
-  -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic
+  -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
 
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t
@@ -1,7 +1,7 @@
 All dune commands work when you run them in sub-directories, so this should be no exception.
 
   $ dune coq top --toplevel=echo -- theories/foo.v
-  -topfile $TESTCASE_ROOT/_build/default/theories/foo.v -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/theories foo
+  -topfile $TESTCASE_ROOT/_build/default/theories/foo.v -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/theories foo
   $ cd theories
 
 This test is currently broken due to the workspace resolution being faulty #5899.