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

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

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,20 +105,24 @@ 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
             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
-            Action_builder.run args.build Eager
+            let* args = args in
+            let dir = Path.external_ Path.External.initial_cwd in
+            if no_rebuild then
+              Memo.map ~f:(fun x -> (x, Dep.Map.empty))
+              @@ Dune_rules.Command.Expert.expand ~dir (S args)
+            else
+              let args = Dune_rules.Command.expand ~dir (S args) in
+              Action_builder.run args.build Eager
           in
           let* prog =
             Super_context.resolve_program sctx ~dir ~loc:None coqtop

src/dune_rules/command.ml

@@ -143,3 +143,26 @@ module Ml_kind = struct
   let ppx_driver_flag t =
     Ml_kind.choose ~impl:(Args.A "--impl") ~intf:(A "--intf") t
 end
+
+module Expert = struct
+  let rec expand : type a. dir:Path.t -> a t -> string list Memo.t =
+   fun ~dir t ->
+    match t with
+    | A s -> Memo.return [ s ]
+    | As l -> Memo.return l
+    | Dep fn | Path fn -> Memo.return [ Path.reach fn ~from:dir ]
+    | Deps fns | Paths fns ->
+      Memo.return @@ List.map fns ~f:(Path.reach ~from:dir)
+    | S ts -> Memo.map ~f:List.concat (Memo.List.map ts ~f:(expand ~dir))
+    | Concat (sep, ts) ->
+      Memo.all [ Memo.map ~f:(String.concat ~sep) (expand ~dir (S ts)) ]
+    | Target fn -> Memo.return [ Path.reach (Path.build fn) ~from:dir ]
+    | Dyn dyn ->
+      Action_builder.run
+        (Action_builder.bind dyn ~f:(fun t -> expand_no_targets ~dir t))
+        Eager
+      |> Memo.map ~f:fst
+    | Fail _ -> Code_error.raise "Command.Expert.expand: Fail encountred" []
+    | Hidden_deps _ | Hidden_targets _ -> Memo.return []
+    | Expand _ -> Code_error.raise "Command.Expert.expand: Expand encountred" []
+end

src/dune_rules/command.mli

@@ -114,3 +114,14 @@ val expand :
     run a command in directory [dir]. *)
 val expand_no_targets :
   dir:Path.t -> Args.without_targets Args.t -> string list Action_builder.t
+
+module Expert : sig
+  (** [Expert.expand ~dir args] interprets the command line arguments [args] to
+      produce corresponding strings, assuming they will be used as arguments to
+      run a command in directory [dir].
+
+      This should not be used often as it is a back door for retrieving the
+      underlying values of [Command.Args.t] forgetting all the dependency and
+      target information. *)
+  val expand : dir:Path.t -> 'a Args.t -> string list Memo.t
+end