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

Signed-off-by: Ali Caglayan <alizter@gmail.com>
ocaml · Jan 22, 2023 · 09cd6a1 · 09cd6a1
1 parent fc0769e
commit 09cd6a1
Show file tree

Hide file tree

Showing 7 changed files with 29 additions and 13 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,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,20 @@ 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 stanza_flags : Ordered_set_lang.Unexpanded.t =
+      match coq_prog with
+      | `Coqtop ->
+        let open Ordered_set_lang.Unexpanded in
+        let pos = ("", 0, 0, 0) in
+        diff stanza_flags ~pos ~context:Univ_map.empty
+          (of_strings ~pos [ "-q" ])
+      | _ -> stanza_flags
+    in
+    let coq_flags =
+      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
+    in
     Command.Args.dyn coq_flags (* stanza flags *)
   in
   let coq_native_flags =

diff --git a/src/dune_rules/ordered_set_lang.ml b/src/dune_rules/ordered_set_lang.ml
@@ -256,6 +256,9 @@ module Unexpanded = struct
     ; context = Univ_map.empty
     }
 
+  let diff ~context ~pos t t' : t =
+    { ast = Ast.Diff (t.ast, t'.ast); loc = Some (Loc.of_pos pos); context }
+
   let include_single ~context ~pos f =
     { ast = Ast.Include (String_with_vars.virt_text pos f)
     ; loc = Some (Loc.of_pos pos)

diff --git a/src/dune_rules/ordered_set_lang.mli b/src/dune_rules/ordered_set_lang.mli
@@ -54,6 +54,8 @@ module Unexpanded : sig
 
   val standard : t
 
+  val diff : context:Univ_map.t -> pos:string * int * int * int -> t -> t -> t
+
   val of_strings : pos:string * int * int * int -> string list -> t
 
   val include_single :

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.