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

<!-- ps-id: 5a03ba95-9ec7-41fd-8f3f-db31c6742042 -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>

CHANGES.md

@@ -62,6 +62,9 @@ Unreleased
   @rgrinberg)
 
 - Fix configurator when using the MSVC compiler (#6538, fixes #6537, @nojb)
+
+- 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)

src/dune_rules/coq_rules.ml

@@ -46,11 +46,6 @@ 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 open Action_builder.O in
-  let* standard = Action_builder.of_memo @@ Super_context.coq ~dir sctx in
-  Expander.expand_and_eval_set expander stanza_flags ~standard
-
 let theories_flags ~theories_deps =
   let theory_coqc_flag lib =
     let dir = Coq_lib.src_root lib in
@@ -347,7 +342,17 @@ let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog
     ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs coq_module =
   let+ coq_stanza_flags =
     let+ expander = Super_context.expander sctx ~dir in
-    let coq_flags = coq_flags ~expander ~dir ~stanza_flags ~sctx in
+    let coq_flags =
+      let open Action_builder.O in
+      let* standard = Action_builder.of_memo @@ Super_context.coq ~dir sctx in
+      let standard =
+        (* For dune coq top, we don't want the -q flag *)
+        match coq_prog with
+        | `Coqtop -> Action_builder.return []
+        | _ -> standard
+      in
+      Expander.expand_and_eval_set expander stanza_flags ~standard
+    in
     Command.Args.dyn coq_flags (* stanza flags *)
   in
   let coq_native_flags =

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

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
 

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.