Add rocq repl-with-drop subcommand, put coqtop.byte back in coq-core

topbin/coqtop_byte_bin.ml

@@ -8,48 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* We register this handler for lower-level toplevel loading code *)
-let () = CErrors.register_handler (function
-    | Symtable.Error e ->
-      Some (Pp.str (Format.asprintf "%a" Symtable.report_error e))
-    | _ ->
-      None
-  )
+open Rocqshim
 
-(* Another bit of text is printed in the [include_utilities] file, so the default one is not need *)
-let () = Clflags.noversion := true
-
-let load_module fmt name =
-  if not ((Topdirs.load_file [@ocaml.warning "-3"]) fmt name) then
-    CErrors.user_err Pp.(str ("Could not load plugin " ^ name))
-
-let load_plugin fmt ps =
-  let lib = Mltop.PluginSpec.to_package ps in
-  Topfind.load_deeply [lib]
-
-let ml_loop fmt ?init_file () =
-  let init_file = ref init_file in
-  Toploop.add_hook (fun event ->
-    if event = Toploop.After_setup then begin
-      match !init_file with
-      | None -> ()
-      | Some f ->
-        init_file := None; (* Run the initialization file only once *)
-        ignore (Coq_byte_config.toploop_use_silently fmt f)
-    end
-  );
-  Coq_byte_config.compenv_handle_exit_with_status_0 (fun () -> Toploop.loop fmt)
-
-let drop_setup () =
-  let ppf = Format.std_formatter in
-  Mltop.set_top
-    { load_plugin = load_plugin ppf
-    ; load_module = load_module ppf
-    ; add_dir = Topdirs.dir_directory
-    ; ml_loop = ml_loop ppf
-    }
-
-(* Main coqtop initialization *)
-let _ =
-  drop_setup ();
-  Coqtop.(start_coq coqtop_toplevel (List.tl (Array.to_list Sys.argv)))
+let () =
+  let args = List.tl (Array.to_list Sys.argv) in
+  let opts, args = Rocqshim.parse_opts args in
+  let () = Rocqshim.init opts args in
+  let prog = get_worker_path { package = "rocq-runtime"; basename = "coqworker_with_drop" } in
+  let () = if opts.debug_shim then Printf.eprintf "Using %s\n%!" prog in
+  let argv = Array.of_list (prog :: args) in
+  exec_or_create_process prog argv

topbin/coqworker_with_drop.ml

@@ -0,0 +1,55 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* We register this handler for lower-level toplevel loading code *)
+let () = CErrors.register_handler (function
+    | Symtable.Error e ->
+      Some (Pp.str (Format.asprintf "%a" Symtable.report_error e))
+    | _ ->
+      None
+  )
+
+(* Another bit of text is printed in the [include_utilities] file, so the default one is not need *)
+let () = Clflags.noversion := true
+
+let load_module fmt name =
+  if not ((Topdirs.load_file [@ocaml.warning "-3"]) fmt name) then
+    CErrors.user_err Pp.(str ("Could not load plugin " ^ name))
+
+let load_plugin fmt ps =
+  let lib = Mltop.PluginSpec.to_package ps in
+  Topfind.load_deeply [lib]
+
+let ml_loop fmt ?init_file () =
+  let init_file = ref init_file in
+  Toploop.add_hook (fun event ->
+    if event = Toploop.After_setup then begin
+      match !init_file with
+      | None -> ()
+      | Some f ->
+        init_file := None; (* Run the initialization file only once *)
+        ignore (Coq_byte_config.toploop_use_silently fmt f)
+    end
+  );
+  Coq_byte_config.compenv_handle_exit_with_status_0 (fun () -> Toploop.loop fmt)
+
+let drop_setup () =
+  let ppf = Format.std_formatter in
+  Mltop.set_top
+    { load_plugin = load_plugin ppf
+    ; load_module = load_module ppf
+    ; add_dir = Topdirs.dir_directory
+    ; ml_loop = ml_loop ppf
+    }
+
+(* Main coqtop initialization *)
+let () =
+  drop_setup ();
+  Coqtop.(start_coq coqtop_toplevel (List.tl (Array.to_list Sys.argv)))

topbin/dune

@@ -29,10 +29,9 @@
 (executable
  (name coqtop_byte_bin)
  (public_name coqtop.byte)
- (package rocq-runtime)
+ (package coq-core)
  (modules coqtop_byte_bin)
- (libraries compiler-libs.toplevel rocq-runtime.config.byte rocq-runtime.toplevel rocq-runtime.dev findlib.top)
- (modes byte))
+ (libraries rocqshim))
 
 (executable
  (name coqc_bin)
@@ -59,9 +58,16 @@
  ; Adding -ccopt -flto to links options could be interesting, however,
  ; it doesn't work on Windows
 
+(executable
+ (name coqworker_with_drop)
+ (modules coqworker_with_drop)
+ (modes byte)
+ (libraries compiler-libs.toplevel rocq-runtime.config.byte rocq-runtime.toplevel rocq-runtime.dev findlib.top))
+
 (install
  (section libexec)
  (package rocq-runtime)
  (files
   (coqworker.exe as coqworker)
-  (coqworker.bc as coqworker.byte)))
+  (coqworker.bc as coqworker.byte)
+  (coqworker_with_drop.bc as coqworker_with_drop)))

topbin/rocq.ml

@@ -13,13 +13,16 @@ let fatal_error fmt = Printf.kfprintf (fun _ -> exit 1) stderr (fmt^^"\n")
 let error_usage () =
   fatal_error "Usage: rocq [-debug-shim] {-v|--version|NAME} [ARGUMENTS...]"
 
-let with_worker opts kind args =
+let with_worker_gen opts basename args =
   Rocqshim.init opts args;
-  let prog = Rocqshim.get_worker_path { package = "rocq-runtime"; basename = "coqworker" } in
+  let prog = Rocqshim.get_worker_path { package = "rocq-runtime"; basename } in
   let () = if opts.debug_shim then Printf.eprintf "Using %s\n%!" prog in
-  let argv = Array.of_list (prog :: ("--kind="^kind) :: args) in
+  let argv = Array.of_list (prog :: args) in
   Rocqshim.exec_or_create_process prog argv
 
+let with_worker opts kind args =
+  with_worker_gen opts "coqworker" (("--kind="^kind) :: args)
+
 let () =
   if Array.length Sys.argv < 2 then error_usage ();
 
@@ -29,6 +32,7 @@ let () =
   | "-v" :: _ | "--version" :: _ -> Boot.Usage.version ()
   | ("c" | "compile") :: args -> with_worker opts "compile" args
   | ("top"|"repl") :: args -> with_worker opts "repl" args
+  | ("top-with-drop"|"repl-with-drop") :: args -> with_worker_gen opts "coqworker_with_drop" args
   | ("preprocess-mlg"|"pp-mlg") :: args -> Coqpp_main.main args
   | "dep" :: args -> Coqdeplib.Rocqdep_main.main args
   | "doc" :: args -> Coqdoclib.Rocqdoc_main.main ~prog:(Sys.argv.(0) ^ " doc") args