From 8c7e62e468b5f5be0feb57a306c7f74a86ccb19b Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Wed, 22 Mar 2023 19:22:32 +0100
Subject: [PATCH] dune coq top: add --no-build option to avoid building
 dependencies

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 CHANGES.md                                    |  3 ++
 bin/coq/coqtop.ml                             | 20 ++++++----
 .../test-cases/coq/coqtop/coqtop-no-build.t   | 38 +++++++++++++++++++
 3 files changed, 54 insertions(+), 7 deletions(-)
 create mode 100644 test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t

diff --git a/CHANGES.md b/CHANGES.md
index 1d4e1a7b676e..882ffddada63 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -15,6 +15,9 @@ Unreleased
   longer supported (due to being buggy) (#7357, fixes #7344, @rlepigre and
   @Alizter)
 
+- Added `-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)
 
diff --git a/bin/coq/coqtop.ml b/bin/coq/coqtop.ml
index 525f9c5e8757..67e0495f01aa 100644
--- a/bin/coq/coqtop.ml
+++ b/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 =
@@ -101,19 +105,21 @@ let term =
               , extr.buildable.coq_lang_version
               , "DuneExtraction" )
           in
+          (* Run coqdep *)
           let* (_ : unit * Dep.Fact.t Dep.Map.t) =
             let deps_of =
-              Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name
-                ~coq_lang_version coq_module
+              if no_rebuild then Action_builder.return ()
+              else
+                Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name
+                  ~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 =
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t
new file mode 100644
index 000000000000..2181468a8be8
--- /dev/null
+++ b/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