dune coq top: add --no-build option to avoid building dependencies

CHANGES.md

@@ -23,6 +23,9 @@ Unreleased
   longer supported (due to being buggy) (#7357, fixes #7344, @rlepigre and
   @Alizter)
 
+- Added a `--no-build` option to `dune coq top` for avoiding rebuilds (#7380,
+  fixes #7355, @Alizter)
+
 - RPC: Ignore SIGPIPE when clients suddenly disconnect (#7299, #7319, fixes
   #6879, @rgrinberg)
 

bin/coq/coqtop.ml

@@ -29,6 +29,10 @@ let term =
     Arg.(required & pos 0 (some string) None (Arg.info [] ~docv:"COQFILE"))
   and+ extra_args =
     Arg.(value & pos_right 0 string [] (Arg.info [] ~docv:"ARGS"))
+  and+ no_rebuild =
+    Arg.(
+      value & flag
+      & info [ "no-build" ] ~doc:"Don't rebuild dependencies before executing.")
   in
   let config = Common.init common in
   let coq_file_arg =
@@ -103,24 +107,26 @@ let term =
               , "DuneExtraction"
               , extr.buildable.mode )
           in
+          (* Run coqdep *)
           let* (_ : unit * Dep.Fact.t Dep.Map.t) =
             let deps_of =
-              let mode =
-                match mode with
-                | None -> Dune_rules.Coq_mode.VoOnly
-                | Some mode -> mode
-              in
-              Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name ~mode
-                ~coq_lang_version coq_module
+              if no_rebuild then Action_builder.return ()
+              else
+                let mode =
+                  match mode with
+                  | None -> Dune_rules.Coq_mode.VoOnly
+                  | Some mode -> mode
+                in
+                Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name
+                  ~mode ~coq_lang_version coq_module
             in
             Action_builder.(run deps_of) Eager
           in
+          (* Get args *)
           let* (args, _) : string list * Dep.Fact.t Dep.Map.t =
-            let* args =
-              let dir = Path.external_ Path.External.initial_cwd in
-              let+ args = args in
-              Dune_rules.Command.expand ~dir (S args)
-            in
+            let* args = args in
+            let dir = Path.external_ Path.External.initial_cwd in
+            let args = Dune_rules.Command.expand ~dir (S args) in
             Action_builder.run args.build Eager
           in
           let* prog =

doc/coq.rst

@@ -660,6 +660,11 @@ actually passed to the toplevel. These options are computed based on the options
 that would be passed to the Coq compiler if it was invoked on the Coq file
 ``<file>``.
 
+In certain situations, it is desirable to not rebuild dependencies for a ``.v``
+files but still pass the correct flags to the toplevel. For this reason, a
+``--no-build`` flag can be passed to ``dune coq top`` which will skip any
+building of dependencies.
+
 Limitations
 ~~~~~~~~~~~
 

test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t

@@ -0,0 +1,38 @@
+Testing the -no-build opion of dune coq top:
+
+  $ mkdir dir
+  $ cat >dir/bar.v <<EOF
+  > From basic Require Import foo.
+  > Definition mynum (i : mynat) := 3.
+  > EOF
+  $ cat >dir/foo.v <<EOF
+  > Definition mynat := nat.
+  > EOF
+  $ cat >dir/dune <<EOF
+  > (coq.theory
+  >  (name basic))
+  > EOF
+  $ cat >dune-project <<EOF
+  > (lang dune 3.8)
+  > (using coq 0.8)
+  > EOF
+
+On a fresh build, this should do nothing but should pass the correct flags:
+
+  $ dune coq top --no-build --display short --toplevel echo dir/bar.v | ../scrub_coq_args.sh
+  -topfile $TESTCASE_ROOT/_build/default/dir/bar.v
+  -w -deprecated-native-compiler-option -native-output-dir . -native-compiler on
+  -I coq-core/kernel
+  -nI $TESTCASE_ROOT/_build/default/dir
+  -R coqtop/_build/default/dir basic
+
+And for comparison normally a build would happen:
+
+  $ dune coq top --display short --toplevel echo dir/bar.v | ../scrub_coq_args.sh
+        coqdep dir/.basic.theory.d
+          coqc dir/Nbasic_foo.{cmi,cmxs},dir/foo.{glob,vo}
+  -topfile $TESTCASE_ROOT/_build/default/dir/bar.v
+  -w -deprecated-native-compiler-option -native-output-dir . -native-compiler on
+  -I coq-core/kernel
+  -nI $TESTCASE_ROOT/_build/default/dir
+  -R coqtop/_build/default/dir basic