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

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)
 

src/dune_rules/coq/coq_rules.ml

@@ -347,7 +347,23 @@ 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 coq_flags = coq_flags ~expander ~dir ~stanza_flags ~sctx in
+      (* By default we have the -q flag. We don't want to pass this to coqtop to
+         allow users to load their .coqrc files for interactive development.
+         Therefore we manually scrub the -q setting when passing arguments to
+         coqtop. *)
+      match coq_prog with
+      | `Coqtop ->
+        let rec remove_q = function
+          | "-q" :: l -> remove_q l
+          | x :: l -> x :: remove_q l
+          | [] -> []
+        in
+        let open Action_builder.O in
+        coq_flags >>| remove_q
+      | _ -> coq_flags
+    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.