From 210d6d8226c2bd824f2e02013f4cc591578ded48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 9 Dec 2024 17:46:13 +0100 Subject: [PATCH] Add `rocq repl-with-drop` subcommand, put coqtop.byte back in coq-core --- topbin/coqtop_byte_bin.ml | 53 ++++++-------------------------- topbin/coqworker_with_drop.ml | 55 ++++++++++++++++++++++++++++++++++ topbin/coqworker_with_drop.mli | 0 topbin/dune | 14 ++++++--- topbin/rocq.ml | 10 +++++-- 5 files changed, 81 insertions(+), 51 deletions(-) create mode 100644 topbin/coqworker_with_drop.ml create mode 100644 topbin/coqworker_with_drop.mli diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml index 4a99268bb727..0cb7ffe449c3 100644 --- a/topbin/coqtop_byte_bin.ml +++ b/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 diff --git a/topbin/coqworker_with_drop.ml b/topbin/coqworker_with_drop.ml new file mode 100644 index 000000000000..38474229fd37 --- /dev/null +++ b/topbin/coqworker_with_drop.ml @@ -0,0 +1,55 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + 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))) diff --git a/topbin/coqworker_with_drop.mli b/topbin/coqworker_with_drop.mli new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/topbin/dune b/topbin/dune index 9c6861c6522d..83845cc5c10f 100644 --- a/topbin/dune +++ b/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))) diff --git a/topbin/rocq.ml b/topbin/rocq.ml index 752cea13d17c..b12849f1798e 100644 --- a/topbin/rocq.ml +++ b/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