[rocq] Remove need for coqc shims.

We remove the need for installing coqc shims, and adapt the test suite
accordingly.

There is one mayor caveat and one minor caveat:

- the major caveat is that in builds composed with Rocq, dune will
  only search for `rocq`, but we don't inject a dependency on
  `rocqworker` which is also needed, but a private binary. This means
  that users should ensure manually `rocqworker` is built when using
  composed builds. We hope to fix this soon, in a different PR.

- the minor caveat is that with `--display=short` we just now display
  the `rocq` name, not `rocq compile` or `rocq dep`. This can be also
  fixed in a different PR.

Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

Author: ejgallego

bin/rocq/rocqtop.ml

@@ -37,7 +37,7 @@ let term =
     Common.context_arg ~doc
   and+ rocqtop =
     let doc = Some "Run the given toplevel command instead of the default." in
-    Arg.(value & opt string "coqtop" & info [ "toplevel" ] ~docv:"CMD" ~doc)
+    Arg.(value & opt string "rocq" & info [ "toplevel" ] ~docv:"CMD" ~doc)
   and+ rocq_file_arg =
     Arg.(required & pos 0 (some string) None (Arg.info [] ~doc:None ~docv:"ROCQFILE"))
   and+ extra_args =
@@ -72,7 +72,7 @@ let term =
        | Some dir -> dir)
       |> Path.Build.append_local (Context.build_dir context)
     in
-    let* rocqtop, args, env =
+    let* rocqtop, rocq_arg, args, env =
       build_exn
       @@ fun () ->
       let open Memo.O in
@@ -145,22 +145,26 @@ let term =
         in
         Action_builder.evaluate_and_collect_facts deps_of
       in
+      let real_binary, rocq_arg =
+        if String.equal "rocq" rocqtop then "rocq", [ "top" ] else rocqtop, []
+      in
+      let* prog = Super_context.resolve_program_memo sctx ~dir ~loc:None real_binary in
+      let prog = Action.Prog.ok_exn prog in
+      let* () = Build_system.build_file prog in
       (* Get args *)
       let* (args, _) : string list * Dep.Fact.t Dep.Map.t =
         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.evaluate_and_collect_facts args.build
       in
-      let* prog = Super_context.resolve_program_memo sctx ~dir ~loc:None rocqtop in
-      let prog = Action.Prog.ok_exn prog in
-      let* () = Build_system.build_file prog in
       let+ env = Super_context.context_env sctx in
-      Path.to_string prog, args, env
+      Path.to_string prog, rocq_arg, args, env
     in
+    (* Careful about the first argument to "rocq" *)
     let args =
       let topfile = Path.to_absolute_filename (Path.build rocq_file_build) in
-      ("-topfile" :: topfile :: args) @ extra_args
+      rocq_arg @ ("-topfile" :: topfile :: args) @ extra_args
     in
     Fiber.return (rocqtop, args, env)
   in

src/dune_rules/rocq/rocq_config.ml

@@ -78,8 +78,8 @@ end = struct
   ;;
 end
 
-let get_output_from_config_or_version ~(coqc : Action.Prog.t) ~what memo =
-  match coqc with
+let get_output_from_config_or_version ~(rocq : Action.Prog.t) ~what memo =
+  match rocq with
   | Ok coqc_path ->
     let open Memo.O in
     let+ output, exit_code = Memo.exec memo coqc_path in
@@ -170,10 +170,10 @@ module Version = struct
 
   let version_memo = Memo.create "coq-and-ocaml-version" ~input:(module Path) impl_version
 
-  let make ~(coqc : Action.Prog.t) =
+  let make ~(rocq : Action.Prog.t) =
     let open Memo.O in
     let+ version_output =
-      get_output_from_config_or_version ~coqc ~what:"--print-version" version_memo
+      get_output_from_config_or_version ~rocq ~what:"--print-version" version_memo
     in
     let open Result.O in
     let* version_output = version_output in
@@ -227,23 +227,23 @@ let impl_config bin =
 
 let config_memo = Memo.create "rocq-config" ~input:(module Path) impl_config
 
-let make ~(coqc : Action.Prog.t) =
+let make ~(rocq : Action.Prog.t) =
   let open Memo.O in
   let+ config_output =
-    get_output_from_config_or_version ~coqc ~what:"--config" config_memo
+    get_output_from_config_or_version ~rocq ~what:"--config" config_memo
   in
   let open Result.O in
   let* config_output = config_output in
   match Vars.of_lines config_output with
   | Ok vars ->
     (* EJGA: Note, this is still COQLIB and
-       COQ_NATIVE_COMPILER_DEFAULT in both [coqc --config] and [rocq c
+       COQ_NATIVE_COMPILER_DEFAULT in both [rocq --config] and [rocq c
        --config] ; so BEWARE ! *)
     let rocqlib = Vars.get_path vars "COQLIB" in
     let rocq_native_compiler_default = Vars.get_opt vars "COQ_NATIVE_COMPILER_DEFAULT" in
     Ok { rocqlib; rocq_native_compiler_default }
   | Error msg ->
-    User_error.raise Pp.[ textf "Cannot parse output of coqc --config:"; msg ]
+    User_error.raise Pp.[ textf "Cannot parse output of rocq --config:"; msg ]
 ;;
 
 let by_name { rocqlib; rocq_native_compiler_default } name =
@@ -260,14 +260,14 @@ let by_name { rocqlib; rocq_native_compiler_default } name =
 let expand source macro artifacts_host =
   let s = Pform.Macro_invocation.Args.whole macro in
   let open Memo.O in
-  let* coqc = Artifacts.binary artifacts_host ~where:Original_path ~loc:None "coqc" in
+  let* rocq = Artifacts.binary artifacts_host ~where:Original_path ~loc:None "rocq" in
   let expand m k s =
-    let+ t = m ~coqc in
+    let+ t = m ~rocq in
     match t with
     | Error msg ->
       User_error.raise
         ~loc:(Dune_lang.Template.Pform.loc source)
-        [ Pp.textf "Could not expand %%{rocq:%s} as running coqc failed." s; msg ]
+        [ Pp.textf "Could not expand %%{rocq:%s} as running rocq failed." s; msg ]
     | Ok t ->
       (match k t s with
        | None ->

src/dune_rules/rocq/rocq_config.mli

@@ -29,14 +29,14 @@ module Version : sig
   (** Data of a Rocq version. *)
   type t
 
-  (** [make ~coqc] runs coqc --print-version and returns the version of Rocq
+  (** [make ~rocq] runs rocq --print-version and returns the version of Rocq
       and the version of OCaml used to build Rocq.
       Exceptionally, one of the following will happen:
 
-      - Return [Error message] if coqc --print-version exits with a non-zero code.
-      - Throw a user error if coqc --print-version is not parsable.
-      - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *)
-  val make : coqc:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
+      - Return [Error message] if rocq --print-version exits with a non-zero code.
+      - Throw a user error if rocq --print-version is not parsable.
+      - Throw an [Action.Prog.Not_found] exception if the rocq binary is not found. *)
+  val make : rocq:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
 
   (** [by_name t name] returns the value of the field [name] in the Rocq
       version [t]. If the value is not available then [None] is returned.
@@ -56,13 +56,13 @@ end
 (** Data of a Rocq configuration. *)
 type t
 
-(** [make ~coqc] runs coqc --config and returns the configuration data. Exceptionally, one
+(** [make ~rocq] runs rocq --config and returns the configuration data. Exceptionally, one
     of the following will happen:
 
-    - Return [Error message] if coqc --config exits with a non-zero code.
-    - Throw a user error if coqc --config is not parsable.
-    - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *)
-val make : coqc:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
+    - Return [Error message] if rocq --config exits with a non-zero code.
+    - Throw a user error if rocq --config is not parsable.
+    - Throw an [Action.Prog.Not_found] exception if the rocq binary is not found. *)
+val make : rocq:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
 
 (** [by_name t name] returns the value of the option [name] in the Rocq
     configuration [t]. If the value is not available then [None] is returned.

src/dune_rules/rocq/rocq_path.ml

@@ -36,11 +36,11 @@ let config_path_exn rocq_config key =
        (* This should never happen *)
        Code_error.raise "key is not a path" [ key, Rocq_config.Value.to_dyn path ])
   | None ->
-    (* This happens if the output of coqc --config doesn't include the key *)
+    (* This happens if the output of rocq --config doesn't include the key *)
     User_error.raise
       [ Pp.concat
           ~sep:Pp.space
-          [ Pp.text "key not found from"; User_message.command "coqc --config" ]
+          [ Pp.text "key not found from"; User_message.command "rocq --config" ]
         |> Pp.hovbox
       ; Pp.text key
       ]
@@ -135,16 +135,16 @@ let scan_vo root_path =
   scan_path ~f ~acc ~prefix:() root_path
 ;;
 
-let of_rocq_install coqc =
+let of_rocq_install rocq =
   let open Memo.O in
-  let* rocq_config = Rocq_config.make ~coqc:(Ok coqc) in
+  let* rocq_config = Rocq_config.make ~rocq:(Ok rocq) in
   match rocq_config with
   | Error msg ->
     User_warning.emit
       [ Pp.concat
           ~sep:Pp.space
           [ Pp.text "Skipping installed theories due to"
-          ; User_message.command "coqc --config"
+          ; User_message.command "rocq --config"
           ; Pp.text "failure:"
           ]
         |> Pp.hovbox
@@ -154,7 +154,7 @@ let of_rocq_install coqc =
         [ Pp.concat
             ~sep:Pp.space
             [ Pp.text "Try running"
-            ; User_message.command "coqc --config"
+            ; User_message.command "rocq --config"
             ; Pp.text "manually to see the error."
             ]
           |> Pp.hovbox
@@ -178,18 +178,18 @@ let of_rocq_install coqc =
     Memo.return (corelib :: user_contrib)
 ;;
 
-let of_rocq_install coqc =
-  (* If coqc was found in the _build directory then we must be composing
-     with Coq and therefore cannot have any installed libs *)
-  if Path.is_in_build_dir coqc then Memo.return [] else of_rocq_install coqc
+let of_rocq_install rocq =
+  (* If rocq was found in the _build directory then we must be composing
+     with Rocq and therefore cannot have any installed libs *)
+  if Path.is_in_build_dir rocq then Memo.return [] else of_rocq_install rocq
 ;;
 
 let of_rocq_install context =
   let open Memo.O in
-  let* coqc = Context.which context "coqc" in
-  match coqc with
+  let* rocq = Context.which context "rocq" in
+  match rocq with
   | None -> Memo.return []
-  | Some coqc -> of_rocq_install coqc
+  | Some rocq -> of_rocq_install rocq
 ;;
 
 let of_env env =

src/dune_rules/rocq/rocq_rules.ml

@@ -64,22 +64,22 @@ end = struct
   ;;
 end
 
-let coqc ~loc ~dir ~sctx =
+let rocq ~loc ~dir ~sctx =
   Super_context.resolve_program_memo
     sctx
-    "coqc"
+    "rocq"
     ~where:Original_path
     ~dir
     ~loc:(Some loc)
-    ~hint:"opam install coq"
+    ~hint:"opam install rocq-runtime"
 ;;
 
 let select_native_mode ~sctx ~dir (buildable : Rocq_stanza.Buildable.t) =
   match buildable.mode with
   | Some x -> Memo.return x
   | None ->
-    let* coqc = coqc ~sctx ~dir ~loc:buildable.loc in
-    let+ config = Rocq_config.make ~coqc in
+    let* rocq = rocq ~sctx ~dir ~loc:buildable.loc in
+    let+ config = Rocq_config.make ~rocq in
     (match config with
      | Error _ -> Rocq_mode.VoOnly
      | Ok config ->
@@ -443,18 +443,13 @@ let setup_rocqdep_for_theory_rule
     rocqdep_flags ~dir ~stanza_rocqdep_flags ~expander
   in
   let rocqdep_flags =
-    Command.Args.Dyn boot_flags :: Command.Args.dyn extra_rocqdep_flags :: file_flags
+    Command.Args.A "dep"
+    :: Command.Args.Dyn boot_flags
+    :: Command.Args.dyn extra_rocqdep_flags
+    :: file_flags
   in
   let stdout_to = dep_theory_file ~dir ~wrapper_name in
-  let* coqdep =
-    Super_context.resolve_program_memo
-      sctx
-      "coqdep"
-      ~dir
-      ~where:Original_path
-      ~loc:(Some loc)
-      ~hint:"opam install coq"
-  in
+  let* rocq = rocq ~loc ~sctx ~dir in
   (* Rocqdep has to be called in the stanza's directory *)
   Super_context.add_rule
     ~loc
@@ -463,7 +458,7 @@ let setup_rocqdep_for_theory_rule
     (let open Action_builder.With_targets.O in
      Action_builder.with_no_targets mlpack_rule
      >>> Action_builder.(with_no_targets (goal source_rule))
-     >>> Command.run ~dir:(Path.build dir) ~stdout_to coqdep rocqdep_flags)
+     >>> Command.run ~dir:(Path.build dir) ~stdout_to rocq rocqdep_flags)
 ;;
 
 module Dep_map = Stdune.Map.Make (Path)
@@ -663,7 +658,7 @@ let setup_rocqc_rule
   let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in
   (* TODO: merge with boot_type *)
   let per_file_flags = Per_file.match_ modules_flags rocq_module in
-  let* coqc = coqc ~loc ~dir ~sctx in
+  let* rocq = rocq ~loc ~dir ~sctx in
   let obj_files =
     Rocq_module.obj_files
       ~wrapper_name
@@ -690,14 +685,18 @@ let setup_rocqc_rule
       rocq_module
   in
   let deps_of = deps_of ~dir ~boot_type ~wrapper_name ~mode rocq_module in
+  let cflag = Command.Args.A "compile" in
   let open Action_builder.With_targets.O in
   Super_context.add_rule
     ~loc
     ~dir
     sctx
     (Action_builder.with_no_targets deps_of
      >>> Action_builder.With_targets.add ~file_targets
-         @@ Command.run ~dir:(Path.build rocqc_dir) coqc (target_obj_files :: args)
+         @@ Command.run
+              ~dir:(Path.build rocqc_dir)
+              rocq
+              (cflag :: target_obj_files :: args)
      (* The way we handle the transitive dependencies of .vo files is not safe for
         sandboxing *)
      >>| Action.Full.add_sandbox Sandbox_config.no_sandboxing)
@@ -739,15 +738,7 @@ let setup_rocqdoc_rules ~sctx ~dir ~theories_deps (s : Rocq_stanza.Theory.t) roc
     in
     fun mode ->
       let* () =
-        let* rocqdoc =
-          Super_context.resolve_program_memo
-            sctx
-            "coqdoc"
-            ~dir
-            ~where:Original_path
-            ~loc:(Some loc)
-            ~hint:"opam install coq"
-        in
+        let* rocq = rocq ~loc ~sctx ~dir in
         (let doc_dir = Rocq_doc.rocqdoc_directory ~mode ~obj_dir:dir ~name in
          let file_flags =
            let globs =
@@ -781,7 +772,8 @@ let setup_rocqdoc_rules ~sctx ~dir ~theories_deps (s : Rocq_stanza.Theory.t) roc
              in
              Expander.expand_and_eval_set expander s.rocqdoc_flags ~standard
            in
-           [ Command.Args.S file_flags
+           [ Command.Args.A "doc"
+           ; Command.Args.S file_flags
            ; Command.Args.dyn extra_rocqdoc_flags
            ; A mode_flag
            ; A "-d"
@@ -797,7 +789,7 @@ let setup_rocqdoc_rules ~sctx ~dir ~theories_deps (s : Rocq_stanza.Theory.t) roc
          Command.run
            ~sandbox:Sandbox_config.needs_sandboxing
            ~dir:(Path.build dir)
-           rocqdoc
+           rocq
            file_flags
          |> Action_builder.With_targets.map
               ~f:
@@ -1032,21 +1024,14 @@ let install_rules ~sctx ~dir s =
 ;;
 
 let setup_rocqpp_rules ~sctx ~dir ({ loc; modules } : Rocq_stanza.Rocqpp.t) =
-  let* coqpp =
-    Super_context.resolve_program_memo
-      sctx
-      "coqpp"
-      ~where:Original_path
-      ~dir
-      ~loc:(Some loc)
-      ~hint:"opam install coq"
+  let* rocq = rocq ~loc ~sctx ~dir
   and* mlg_files = Rocq_sources.mlg_files ~sctx ~dir ~modules in
   let mlg_rule m =
     let source = Path.build m in
     let target = Path.Build.set_extension m ~ext:".ml" in
-    let args = [ Command.Args.Dep source; Hidden_targets [ target ] ] in
+    let args = [ Command.Args.A "pp-mlg"; Dep source; Hidden_targets [ target ] ] in
     let build_dir = Super_context.context sctx |> Context.build_dir in
-    Command.run ~dir:(Path.build build_dir) coqpp args
+    Command.run ~dir:(Path.build build_dir) rocq args
   in
   List.rev_map ~f:mlg_rule mlg_files |> Super_context.add_rules ~loc ~dir sctx
 ;;

test/blackbox-tests/test-cases/rocq-native/base-unsound.t/run.t

@@ -1,4 +1,4 @@
   $ dune build --display short --profile unsound --debug-dependency-path @all
-        coqdep .basic.theory.d
-          coqc Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
-          coqc Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
+          rocq .basic.theory.d
+          rocq Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
+          rocq Nbasic_bar.{cmi,cmxs},bar.{glob,vo}

test/blackbox-tests/test-cases/rocq-native/base.t/run.t

@@ -1,7 +1,7 @@
   $ dune build --display short --debug-dependency-path @all --always-show-command-line
-        coqdep .basic.theory.d
-          coqc Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
-          coqc Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
+          rocq .basic.theory.d
+          rocq Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
+          rocq Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
 
   $ dune build --debug-dependency-path @default
   lib: [