aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/ccompile.ml19
-rw-r--r--toplevel/ccompile.mli2
-rw-r--r--toplevel/coqargs.ml580
-rw-r--r--toplevel/coqargs.mli81
-rw-r--r--toplevel/coqc.ml11
-rw-r--r--toplevel/coqinit.ml111
-rw-r--r--toplevel/coqrc.ml45
-rw-r--r--toplevel/coqrc.mli (renamed from toplevel/coqinit.mli)11
-rw-r--r--toplevel/coqtop.ml21
-rw-r--r--toplevel/coqtop.mli6
-rw-r--r--toplevel/toplevel.mllib4
-rw-r--r--toplevel/usage.ml113
-rw-r--r--toplevel/usage.mli29
-rw-r--r--toplevel/workerLoop.ml7
14 files changed, 79 insertions, 961 deletions
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index b75a4199ea..4747abceb5 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -24,7 +24,7 @@ let fatal_error msg =
let load_init_file opts ~state =
if opts.pre.load_rcfile then
Topfmt.(in_phase ~phase:LoadingRcFile) (fun () ->
- Coqinit.load_rcfile ~rcfile:opts.config.rcfile ~state) ()
+ Coqrc.load_rcfile ~rcfile:opts.config.rcfile ~state) ()
else begin
Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
state
@@ -93,7 +93,7 @@ let create_empty_file filename =
close_out f
(* Compile a vernac file *)
-let compile opts copts ~echo ~f_in ~f_out =
+let compile opts stm_options copts ~echo ~f_in ~f_out =
let open Vernac.State in
let check_pending_proofs () =
let pfs = Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"] in
@@ -106,7 +106,6 @@ let compile opts copts ~echo ~f_in ~f_out =
in
let ml_load_path, vo_load_path = build_load_path opts in
let injections = injection_commands opts in
- let stm_options = opts.config.stm_flags in
let output_native_objects = match opts.config.native_compiler with
| NativeOff -> false | NativeOn {ondemand} -> not ondemand
in
@@ -209,22 +208,22 @@ let compile opts copts ~echo ~f_in ~f_out =
dump_empty_vos();
create_empty_file (long_f_dot_out ^ "k")
-let compile opts copts ~echo ~f_in ~f_out =
+let compile opts stm_opts copts ~echo ~f_in ~f_out =
ignore(CoqworkmgrApi.get 1);
- compile opts copts ~echo ~f_in ~f_out;
+ compile opts stm_opts copts ~echo ~f_in ~f_out;
CoqworkmgrApi.giveback 1
-let compile_file opts copts (f_in, echo) =
+let compile_file opts stm_opts copts (f_in, echo) =
let f_out = copts.compilation_output_name in
if !Flags.beautify then
Flags.with_option Flags.beautify_file
- (fun f_in -> compile opts copts ~echo ~f_in ~f_out) f_in
+ (fun f_in -> compile opts stm_opts copts ~echo ~f_in ~f_out) f_in
else
- compile opts copts ~echo ~f_in ~f_out
+ compile opts stm_opts copts ~echo ~f_in ~f_out
-let compile_files opts copts =
+let compile_files (opts, stm_opts) copts =
let compile_list = copts.compile_list in
- List.iter (compile_file opts copts) compile_list
+ List.iter (compile_file opts stm_opts copts) compile_list
(******************************************************************************)
(* VIO Dispatching *)
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index 8c154488d0..1b670a8edc 100644
--- a/toplevel/ccompile.mli
+++ b/toplevel/ccompile.mli
@@ -13,7 +13,7 @@
val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t
(** [compile_files opts] compile files specified in [opts] *)
-val compile_files : Coqargs.t -> Coqcargs.t -> unit
+val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> unit
(** [do_vio opts] process [.vio] files in [opts] *)
val do_vio : Coqargs.t -> Coqcargs.t -> unit
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
deleted file mode 100644
index c114c43e26..0000000000
--- a/toplevel/coqargs.ml
+++ /dev/null
@@ -1,580 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq 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) *)
-(************************************************************************)
-
-let fatal_error exn =
- Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
- let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
- exit exit_code
-
-let error_wrong_arg msg =
- prerr_endline msg; exit 1
-
-let error_missing_arg s =
- prerr_endline ("Error: extra argument expected after option "^s);
- prerr_endline "See -help for the syntax of supported options";
- exit 1
-
-(******************************************************************************)
-(* Imperative effects! This must be fixed at some point. *)
-(******************************************************************************)
-let set_worker_id opt s =
- assert (s <> "master");
- Flags.async_proofs_worker_id := s
-
-let set_type_in_type () =
- let typing_flags = Environ.typing_flags (Global.env ()) in
- Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
-
-(******************************************************************************)
-
-type color = [`ON | `AUTO | `EMACS | `OFF]
-
-type native_compiler = Coq_config.native_compiler =
- NativeOff | NativeOn of { ondemand : bool }
-
-type coqargs_logic_config = {
- impredicative_set : Declarations.set_predicativity;
- indices_matter : bool;
- toplevel_name : Stm.interactive_top;
-}
-
-type coqargs_config = {
- logic : coqargs_logic_config;
- rcfile : string option;
- coqlib : string option;
- color : color;
- enable_VM : bool;
- native_compiler : native_compiler;
- native_output_dir : CUnix.physical_path;
- native_include_dirs : CUnix.physical_path list;
- stm_flags : Stm.AsyncOpts.stm_opt;
- debug : bool;
- time : bool;
- print_emacs : bool;
-}
-
-type coqargs_pre = {
- boot : bool;
- load_init : bool;
- load_rcfile : bool;
-
- ml_includes : string list;
- vo_includes : Loadpath.vo_path list;
-
- load_vernacular_list : (string * bool) list;
- injections : Stm.injection_command list;
-
- inputstate : string option;
-}
-
-type coqargs_query =
- | PrintTags | PrintWhere | PrintConfig
- | PrintVersion | PrintMachineReadableVersion
- | PrintHelp of Usage.specific_usage
-
-type coqargs_main =
- | Queries of coqargs_query list
- | Run
-
-type coqargs_post = {
- memory_stat : bool;
- output_context : bool;
-}
-
-type t = {
- config : coqargs_config;
- pre : coqargs_pre;
- main : coqargs_main;
- post : coqargs_post;
-}
-
-let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
-
-let default_native = Coq_config.native_compiler
-
-let default_logic_config = {
- impredicative_set = Declarations.PredicativeSet;
- indices_matter = false;
- toplevel_name = Stm.TopLogical default_toplevel;
-}
-
-let default_config = {
- logic = default_logic_config;
- rcfile = None;
- coqlib = None;
- color = `AUTO;
- enable_VM = true;
- native_compiler = default_native;
- native_output_dir = ".coq-native";
- native_include_dirs = [];
- stm_flags = Stm.AsyncOpts.default_opts;
- debug = false;
- time = false;
- print_emacs = false;
-
- (* Quiet / verbosity options should be here *)
-}
-
-let default_pre = {
- boot = false;
- load_init = true;
- load_rcfile = true;
- ml_includes = [];
- vo_includes = [];
- load_vernacular_list = [];
- injections = [];
- inputstate = None;
-}
-
-let default_queries = []
-
-let default_post = {
- memory_stat = false;
- output_context = false;
-}
-
-let default = {
- config = default_config;
- pre = default_pre;
- main = Run;
- post = default_post;
-}
-
-(******************************************************************************)
-(* Functional arguments *)
-(******************************************************************************)
-let add_ml_include opts s =
- { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }}
-
-let add_vo_include opts unix_path coq_path implicit =
- let open Loadpath in
- let coq_path = Libnames.dirpath_of_string coq_path in
- { opts with pre = { opts.pre with vo_includes = {
- unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
-
-let add_vo_require opts d p export =
- { opts with pre = { opts.pre with injections = Stm.RequireInjection (d, p, export) :: opts.pre.injections }}
-
-let add_load_vernacular opts verb s =
- { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
-
-let add_set_option opts opt_name value =
- { opts with pre = { opts.pre with injections = Stm.OptionInjection (opt_name, value) :: opts.pre.injections }}
-
-(** Options for proof general *)
-let set_emacs opts =
- Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true;
- { opts with config = { opts.config with color = `EMACS; print_emacs = true }}
-
-let set_logic f oval =
- { oval with config = { oval.config with logic = f oval.config.logic }}
-
-let set_color opts = function
- | "yes" | "on" -> { opts with config = { opts.config with color = `ON }}
- | "no" | "off" -> { opts with config = { opts.config with color = `OFF }}
- | "auto" -> { opts with config = { opts.config with color = `AUTO }}
- | _ ->
- error_wrong_arg ("Error: on/off/auto expected after option color")
-
-let set_query opts q =
- { opts with main = match opts.main with
- | Run -> Queries (default_queries@[q])
- | Queries queries -> Queries (queries@[q])
- }
-
-let warn_deprecated_sprop_cumul =
- CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
- (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
-
-let warn_deprecated_inputstate =
- CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
- (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
-
-let set_inputstate opts s =
- warn_deprecated_inputstate ();
- { opts with pre = { opts.pre with inputstate = Some s }}
-
-(******************************************************************************)
-(* Parsing helpers *)
-(******************************************************************************)
-let get_bool opt = function
- | "yes" | "on" -> true
- | "no" | "off" -> false
- | _ ->
- error_wrong_arg ("Error: yes/no expected after option "^opt)
-
-let get_int opt n =
- try int_of_string n
- with Failure _ ->
- error_wrong_arg ("Error: integer expected after option "^opt)
-
-let get_float opt n =
- try float_of_string n
- with Failure _ ->
- error_wrong_arg ("Error: float expected after option "^opt)
-
-let get_host_port opt s =
- match String.split_on_char ':' s with
- | [host; portr; portw] ->
- Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
- | ["stdfds"] -> Some Spawned.AnonPipe
- | _ ->
- error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt)
-
-let get_error_resilience opt = function
- | "on" | "all" | "yes" -> `All
- | "off" | "no" -> `None
- | s -> `Only (String.split_on_char ',' s)
-
-let get_priority opt s =
- try CoqworkmgrApi.priority_of_string s
- with Invalid_argument _ ->
- error_wrong_arg ("Error: low/high expected after "^opt)
-
-let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
- | "no" | "off" -> APoff
- | "yes" | "on" -> APon
- | "lazy" -> APonLazy
- | _ ->
- error_wrong_arg ("Error: on/off/lazy expected after "^opt)
-
-let get_cache opt = function
- | "force" -> Some Stm.AsyncOpts.Force
- | _ ->
- error_wrong_arg ("Error: force expected after "^opt)
-
-
-let get_native_name s =
- (* We ignore even critical errors because this mode has to be super silent *)
- try
- Filename.(List.fold_left concat (dirname s)
- [ !Nativelib.output_dir
- ; Library.native_name_from_filename s
- ])
- with _ -> ""
-
-let get_compat_file = function
- | "8.14" -> "Coq.Compat.Coq814"
- | "8.13" -> "Coq.Compat.Coq813"
- | "8.12" -> "Coq.Compat.Coq812"
- | "8.11" -> "Coq.Compat.Coq811"
- | ("8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
- CErrors.user_err ~hdr:"get_compat_file"
- Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
- | s ->
- CErrors.user_err ~hdr:"get_compat_file"
- Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
-
-let to_opt_key = Str.(split (regexp " +"))
-
-let parse_option_set opt =
- match String.index_opt opt '=' with
- | None -> to_opt_key opt, None
- | Some eqi ->
- let len = String.length opt in
- let v = String.sub opt (eqi+1) (len - eqi - 1) in
- to_opt_key (String.sub opt 0 eqi), Some v
-
-let warn_no_native_compiler =
- CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
- Pp.(fun s -> strbrk "Native compiler is disabled," ++
- strbrk " -native-compiler " ++ strbrk s ++
- strbrk " option ignored.")
-
-let get_native_compiler s =
- (* We use two boolean flags because the four states make sense, even if
- only three are accessible to the user at the moment. The selection of the
- produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by
- a separate flag, and the "ondemand" value removed. Once this is done, use
- [get_bool] here. *)
- let n = match s with
- | ("yes" | "on") -> NativeOn {ondemand=false}
- | "ondemand" -> NativeOn {ondemand=true}
- | ("no" | "off") -> NativeOff
- | _ ->
- error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in
- if Coq_config.native_compiler = NativeOff && n <> NativeOff then
- let () = warn_no_native_compiler s in
- NativeOff
- else
- n
-
-(* Main parsing routine *)
-(*s Parsing of the command line *)
-
-let parse_args ~help ~init arglist : t * string list =
- let args = ref arglist in
- let extras = ref [] in
- let rec parse oval = match !args with
- | [] ->
- (oval, List.rev !extras)
- | opt :: rem ->
- args := rem;
- let next () = match !args with
- | x::rem -> args := rem; x
- | [] -> error_missing_arg opt
- in
- let noval = begin match opt with
-
- (* Complex options with many args *)
- |"-I"|"-include" ->
- begin match rem with
- | d :: rem ->
- args := rem;
- add_ml_include oval d
- | [] -> error_missing_arg opt
- end
- |"-Q" ->
- begin match rem with
- | d :: p :: rem ->
- args := rem;
- add_vo_include oval d p false
- | _ -> error_missing_arg opt
- end
- |"-R" ->
- begin match rem with
- | d :: p :: rem ->
- args := rem;
- add_vo_include oval d p true
- | _ -> error_missing_arg opt
- end
-
- (* Options with one arg *)
- |"-coqlib" ->
- { oval with config = { oval.config with coqlib = Some (next ())
- }}
-
- |"-async-proofs" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
- }}}
- |"-async-proofs-j" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ()))
- }}}
- |"-async-proofs-cache" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
- }}}
-
- |"-async-proofs-tac-j" ->
- let j = get_int opt (next ()) in
- if j <= 0 then begin
- error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
- end;
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_n_tacworkers = j
- }}}
-
- |"-async-proofs-worker-priority" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
- }}}
-
- |"-async-proofs-private-flags" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
- }}}
-
- |"-async-proofs-tactic-error-resilience" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
- }}}
-
- |"-async-proofs-command-error-resilience" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ())
- }}}
-
- |"-async-proofs-delegation-threshold" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ())
- }}}
-
- |"-worker-id" -> set_worker_id opt (next ()); oval
-
- |"-compat" ->
- add_vo_require oval (get_compat_file (next ())) None (Some false)
-
- |"-exclude-dir" ->
- System.exclude_directory (next ()); oval
-
- |"-init-file" ->
- { oval with config = { oval.config with rcfile = Some (next ()); }}
-
- |"-inputstate"|"-is" ->
- set_inputstate oval (next ())
-
- |"-load-vernac-object" ->
- add_vo_require oval (next ()) None None
-
- |"-load-vernac-source"|"-l" ->
- add_load_vernacular oval false (next ())
-
- |"-load-vernac-source-verbose"|"-lv" ->
- add_load_vernacular oval true (next ())
-
- |"-mangle-names" ->
- Goptions.set_bool_option_value ["Mangle"; "Names"] true;
- Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ());
- oval
-
- |"-print-mod-uid" ->
- let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
-
- |"-profile-ltac-cutoff" ->
- Flags.profile_ltac := true;
- Flags.profile_ltac_cutoff := get_float opt (next ());
- oval
-
- |"-rfrom" ->
- let from = next () in add_vo_require oval (next ()) (Some from) None
-
- |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false)
-
- |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true)
-
- |"-require-import-from" | "-rifrom" ->
- let from = next () in add_vo_require oval (next ()) (Some from) (Some false)
-
- |"-require-export-from" | "-refrom" ->
- let from = next () in add_vo_require oval (next ()) (Some from) (Some true)
-
- |"-top" ->
- let topname = Libnames.dirpath_of_string (next ()) in
- if Names.DirPath.is_empty topname then
- CErrors.user_err Pp.(str "Need a non empty toplevel module name");
- { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopLogical topname }}}
-
- |"-topfile" ->
- { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopPhysical (next()) }}}
-
- |"-main-channel" ->
- Spawned.main_channel := get_host_port opt (next()); oval
-
- |"-control-channel" ->
- Spawned.control_channel := get_host_port opt (next()); oval
-
- |"-w" | "-W" ->
- let w = next () in
- if w = "none" then add_set_option oval ["Warnings"] (Stm.OptionSet(Some w))
- else add_set_option oval ["Warnings"] (Stm.OptionAppend w)
-
- |"-bytecode-compiler" ->
- { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }}
-
- |"-native-compiler" ->
- let native_compiler = get_native_compiler (next ()) in
- { oval with config = { oval.config with native_compiler }}
-
- | "-set" ->
- let opt, v = parse_option_set @@ next() in
- add_set_option oval opt (Stm.OptionSet v)
-
- | "-unset" ->
- add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset
-
- |"-native-output-dir" ->
- let native_output_dir = next () in
- { oval with config = { oval.config with native_output_dir } }
-
- |"-nI" ->
- let include_dir = next () in
- { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } }
-
- (* Options with zero arg *)
- |"-async-queries-always-delegate"
- |"-async-proofs-always-delegate"
- |"-async-proofs-never-reopen-branch" ->
- { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
- Stm.AsyncOpts.async_proofs_never_reopen_branch = true
- }}}
- |"-test-mode" -> Vernacinterp.test_mode := true; oval
- |"-beautify" -> Flags.beautify := true; oval
- |"-bt" -> Exninfo.record_backtrace true; oval
- |"-color" -> set_color oval (next ())
- |"-config"|"--config" -> set_query oval PrintConfig
- |"-debug" -> Coqinit.set_debug (); oval
- |"-xml-debug" -> Flags.xml_debug := true; Coqinit.set_debug (); oval
- |"-diffs" ->
- add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ()))
- |"-stm-debug" -> Stm.stm_debug := true; oval
- |"-emacs" -> set_emacs oval
- |"-impredicative-set" ->
- set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval
- |"-allow-sprop" ->
- add_set_option oval Vernacentries.allow_sprop_opt_name (Stm.OptionSet None)
- |"-disallow-sprop" ->
- add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset
- |"-sprop-cumulative" ->
- warn_deprecated_sprop_cumul();
- add_set_option oval Vernacentries.cumul_sprop_opt_name (Stm.OptionSet None)
- |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
- |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
- |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
- |"-boot" -> { oval with pre = { oval.pre with boot = true }}
- |"-output-context" -> { oval with post = { oval.post with output_context = true }}
- |"-profile-ltac" -> Flags.profile_ltac := true; oval
- |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }}
- |"-quiet"|"-silent" ->
- Flags.quiet := true;
- Flags.make_warn false;
- oval
- |"-list-tags" -> set_query oval PrintTags
- |"-time" -> { oval with config = { oval.config with time = true }}
- |"-type-in-type" -> set_type_in_type (); oval
- |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
- |"-where" -> set_query oval PrintWhere
- |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help)
- |"-v"|"--version" -> set_query oval PrintVersion
- |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
-
- (* Unknown option *)
- | s ->
- extras := s :: !extras;
- oval
- end in
- parse noval
- in
- try
- parse init
- with any -> fatal_error any
-
-(* We need to reverse a few lists *)
-let parse_args ~help ~init args =
- let opts, extra = parse_args ~help ~init args in
- let opts =
- { opts with
- pre = { opts.pre with
- ml_includes = List.rev opts.pre.ml_includes
- ; vo_includes = List.rev opts.pre.vo_includes
- ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
- ; injections = List.rev opts.pre.injections
- }
- } in
- opts, extra
-
-(******************************************************************************)
-(* Startup LoadPath and Modules *)
-(******************************************************************************)
-(* prelude_data == From Coq Require Import Prelude. *)
-let prelude_data = "Prelude", Some "Coq", Some false
-
-let injection_commands opts =
- if opts.pre.load_init then Stm.RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections
-
-let build_load_path opts =
- let ml_path, vo_path =
- if opts.pre.boot then [],[]
- else
- let coqlib = Envars.coqlib () in
- Coqinit.libs_init_load_path ~coqlib in
- ml_path @ opts.pre.ml_includes ,
- vo_path @ opts.pre.vo_includes
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
deleted file mode 100644
index f6222e4ec4..0000000000
--- a/toplevel/coqargs.mli
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq 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) *)
-(************************************************************************)
-
-type color = [`ON | `AUTO | `EMACS | `OFF]
-
-val default_toplevel : Names.DirPath.t
-
-type native_compiler = Coq_config.native_compiler =
- NativeOff | NativeOn of { ondemand : bool }
-
-type coqargs_logic_config = {
- impredicative_set : Declarations.set_predicativity;
- indices_matter : bool;
- toplevel_name : Stm.interactive_top;
-}
-
-type coqargs_config = {
- logic : coqargs_logic_config;
- rcfile : string option;
- coqlib : string option;
- color : color;
- enable_VM : bool;
- native_compiler : native_compiler;
- native_output_dir : CUnix.physical_path;
- native_include_dirs : CUnix.physical_path list;
- stm_flags : Stm.AsyncOpts.stm_opt;
- debug : bool;
- time : bool;
- print_emacs : bool;
-}
-
-type coqargs_pre = {
- boot : bool;
- load_init : bool;
- load_rcfile : bool;
-
- ml_includes : CUnix.physical_path list;
- vo_includes : Loadpath.vo_path list;
-
- load_vernacular_list : (string * bool) list;
- injections : Stm.injection_command list;
-
- inputstate : string option;
-}
-
-type coqargs_query =
- | PrintTags | PrintWhere | PrintConfig
- | PrintVersion | PrintMachineReadableVersion
- | PrintHelp of Usage.specific_usage
-
-type coqargs_main =
- | Queries of coqargs_query list
- | Run
-
-type coqargs_post = {
- memory_stat : bool;
- output_context : bool;
-}
-
-type t = {
- config : coqargs_config;
- pre : coqargs_pre;
- main : coqargs_main;
- post : coqargs_post;
-}
-
-(* Default options *)
-val default : t
-
-val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
-val error_wrong_arg : string -> unit
-
-val injection_commands : t -> Stm.injection_command list
-val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 03c53d6991..0c23c9f4e9 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -41,9 +41,9 @@ coqc specific options:\
\n"
}
-let coqc_main copts ~opts =
+let coqc_main (copts,stm_opts) ~opts =
Topfmt.(in_phase ~phase:CompilationPhase)
- Ccompile.compile_files opts copts;
+ Ccompile.compile_files (opts,stm_opts) copts;
(* Careful this will modify the load-path and state so after this
point some stuff may not be safe anymore. *)
@@ -73,8 +73,11 @@ let coqc_run copts ~opts () =
let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
exit exit_code
-let custom_coqc = Coqtop.{
- parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []);
+let custom_coqc : (Coqcargs.t * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel
+ = Coqtop.{
+ parse_extra = (fun ~opts extras ->
+ let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
+ (Coqcargs.parse extras, stm_opts), []);
help = coqc_specific_usage;
init = coqc_init;
run = coqc_run;
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
deleted file mode 100644
index 501047c520..0000000000
--- a/toplevel/coqinit.ml
+++ /dev/null
@@ -1,111 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq 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) *)
-(************************************************************************)
-
-open Util
-open Pp
-
-let ( / ) s1 s2 = Filename.concat s1 s2
-
-let set_debug () =
- let () = Exninfo.record_backtrace true in
- Flags.debug := true
-
-(* Loading of the resource file.
- rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one
- does not exist. *)
-
-let rcdefaultname = "coqrc"
-
-let load_rcfile ~rcfile ~state =
- try
- match rcfile with
- | Some rcfile ->
- if CUnix.file_readable_p rcfile then
- Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile
- else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
- | None ->
- try
- let warn x = Feedback.msg_warning (str x) in
- let inferedrc = List.find CUnix.file_readable_p [
- Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
- Envars.xdg_config_home warn / rcdefaultname;
- Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
- Envars.home ~warn / "."^rcdefaultname
- ] in
- Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc
- with Not_found -> state
- (*
- Flags.if_verbose
- mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
- " found. Skipping rcfile loading."))
- *)
- with reraise ->
- let reraise = Exninfo.capture reraise in
- let () = Feedback.msg_info (str"Load of rcfile failed.") in
- Exninfo.iraise reraise
-
-(* Recursively puts `.v` files in the LoadPath *)
-let build_stdlib_vo_path ~unix_path ~coq_path =
- let open Loadpath in
- { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true }
-
-(* Note we don't use has_ml=true due to #12771 , we need to see if we
- should just remove that option *)
-let build_userlib_path ~unix_path =
- let open Loadpath in
- if Sys.file_exists unix_path then
- let ml_path = System.all_subdirs ~unix_path |> List.map fst in
- let vo_path =
- { unix_path
- ; coq_path = Libnames.default_root_prefix
- ; has_ml = false
- ; implicit = false
- ; recursive = true
- } in
- ml_path, [vo_path]
- else [], []
-
-(* LoadPath for Coq user libraries *)
-let libs_init_load_path ~coqlib =
-
- let open Loadpath in
- let user_contrib = coqlib/"user-contrib" in
- let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
- let coqpath = Envars.coqpath in
- let coq_path = Names.DirPath.make [Libnames.coq_root] in
-
- (* ML includes *)
- let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in
-
- let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in
-
- let misc_ml, misc_vo =
- List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in
-
- let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in
- let vo_loadpath =
- (* current directory (not recursively!) *)
- [ { unix_path = "."
- ; coq_path = Libnames.default_root_prefix
- ; implicit = false
- ; has_ml = true
- ; recursive = false
- } ] @
-
- (* then standard library *)
- [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
-
- (* then user-contrib *)
- contrib_vo @
-
- (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
- List.concat misc_vo
- in
- ml_loadpath, vo_loadpath
diff --git a/toplevel/coqrc.ml b/toplevel/coqrc.ml
new file mode 100644
index 0000000000..e074e621da
--- /dev/null
+++ b/toplevel/coqrc.ml
@@ -0,0 +1,45 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq 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) *)
+(************************************************************************)
+
+let ( / ) s1 s2 = Filename.concat s1 s2
+
+(* Loading of the resource file.
+ rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one
+ does not exist. *)
+
+let rcdefaultname = "coqrc"
+
+let load_rcfile ~rcfile ~state =
+ try
+ match rcfile with
+ | Some rcfile ->
+ if CUnix.file_readable_p rcfile then
+ Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile
+ else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
+ | None ->
+ try
+ let warn x = Feedback.msg_warning (Pp.str x) in
+ let inferedrc = List.find CUnix.file_readable_p [
+ Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
+ Envars.xdg_config_home warn / rcdefaultname;
+ Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
+ Envars.home ~warn / "."^rcdefaultname
+ ] in
+ Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc
+ with Not_found -> state
+ (*
+ Flags.if_verbose
+ mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
+ " found. Skipping rcfile loading."))
+ *)
+ with reraise ->
+ let reraise = Exninfo.capture reraise in
+ let () = Feedback.msg_info (Pp.str"Load of rcfile failed.") in
+ Exninfo.iraise reraise
diff --git a/toplevel/coqinit.mli b/toplevel/coqrc.mli
index b96a0ef162..3b8a31b2a5 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqrc.mli
@@ -8,15 +8,4 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(** Initialization. *)
-
-val set_debug : unit -> unit
-
val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t
-
-(** Standard LoadPath for Coq user libraries; in particular it
- includes (in-order) Coq's standard library, Coq's [user-contrib]
- folder, and directories specified in [COQPATH] and [XDG_DIRS] *)
-val libs_init_load_path
- : coqlib:CUnix.physical_path
- -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d0d50aee70..7596df788b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -198,11 +198,7 @@ let init_parse parse_extra help init_opts =
(** Coq's init process, phase 2: Basic Coq environment, plugins. *)
let init_execution opts custom_init =
- (* If we have been spawned by the Spawn module, this has to be done
- * early since the master waits us to connect back *)
- Spawned.init_channels ();
if opts.post.memory_stat then at_exit print_memory_stat;
- CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
Mltop.init_known_plugins ();
(* Configuration *)
Global.set_engagement opts.config.logic.impredicative_set;
@@ -241,10 +237,11 @@ let init_toplevel custom =
| Queries q -> List.iter (print_query opts) q; exit 0
| Run ->
let () = init_coqlib opts in
+ Stm.init_process (snd customopts);
let customstate = init_execution opts (custom.init customopts) in
opts, customopts, customstate
-let init_document opts =
+let init_document opts stm_options =
(* Coq init process, phase 3: Stm initialization, backtracking state.
It is essential that the module system is in a consistent
@@ -255,7 +252,6 @@ let init_document opts =
Flags.load_vos_libraries := true;
let ml_load_path, vo_load_path = build_load_path opts in
let injections = injection_commands opts in
- let stm_options = opts.config.stm_flags in
let open Vernac.State in
let doc, sid =
Stm.(new_doc
@@ -281,16 +277,16 @@ let start_coq custom =
type run_mode = Interactive | Batch
-let init_toploop opts =
- let state = init_document opts in
+let init_toploop opts stm_opts =
+ let state = init_document opts stm_opts in
let state = Ccompile.load_init_vernaculars opts ~state in
state
-let coqtop_init run_mode ~opts =
+let coqtop_init (run_mode,stm_opts) ~opts =
if run_mode = Batch then Flags.quiet := true;
init_color opts.config;
Flags.if_verbose print_header ();
- init_toploop opts
+ init_toploop opts stm_opts
let coqtop_parse_extra ~opts extras =
let rec parse_extra run_mode = function
@@ -299,9 +295,10 @@ let coqtop_parse_extra ~opts extras =
let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest
| [] -> run_mode, [] in
let run_mode, extras = parse_extra Interactive extras in
- run_mode, extras
+ let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
+ (run_mode, stm_opts), extras
-let coqtop_run run_mode ~opts state =
+let coqtop_run (run_mode,_) ~opts state =
match run_mode with
| Interactive -> Coqloop.loop ~opts ~state;
| Batch -> exit 0
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index e535c19252..9ae0d86cf1 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -28,7 +28,7 @@ type ('a,'b) custom_toplevel =
load the files given on the command line, load the resource file,
produce the output state if any, and finally will launch
[custom.run]. *)
-val start_coq : ('a,'b) custom_toplevel -> unit
+val start_coq : ('a * Stm.AsyncOpts.stm_opt,'b) custom_toplevel -> unit
(** Initializer color for output *)
@@ -36,10 +36,10 @@ val init_color : Coqargs.coqargs_config -> unit
(** Prepare state for interactive loop *)
-val init_toploop : Coqargs.t -> Vernac.State.t
+val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Vernac.State.t
(** The specific characterization of the coqtop_toplevel *)
type run_mode = Interactive | Batch
-val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel
+val coqtop_toplevel : (run_mode * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index ddd11fd160..90f8fb9686 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,7 +1,5 @@
Vernac
-Usage
-Coqinit
-Coqargs
+Coqrc
Coqcargs
G_toplevel
Coqloop
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
deleted file mode 100644
index 6fb5f821ee..0000000000
--- a/toplevel/usage.ml
+++ /dev/null
@@ -1,113 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq 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) *)
-(************************************************************************)
-
-let version () =
- Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
- Coq_config.version Coq_config.date;
- Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version
-
-let machine_readable_version () =
- Printf.printf "%s %s\n"
- Coq_config.version Coq_config.caml_version
-
-(* print the usage of coqtop (or coqc) on channel co *)
-
-let print_usage_common co command =
- output_string co command;
- output_string co "Coq options are:\n";
- output_string co
-" -I dir look for ML files in dir\
-\n -include dir (idem)\
-\n -R dir coqdir recursively map physical dir to logical coqdir\
-\n -Q dir coqdir map physical dir to logical coqdir\
-\n -top coqdir set the toplevel name to be coqdir instead of Top\
-\n -topfile f set the toplevel name as though compiling f\
-\n -coqlib dir set the coq standard library directory\
-\n -exclude-dir f exclude subdirectories named f for option -R\
-\n\
-\n -boot don't bind the `Coq.` prefix to the default -coqlib dir\
-\n -noinit don't load Coq.Init.Prelude on start \
-\n -nois (idem)\
-\n -compat X.Y provides compatibility support for Coq version X.Y\
-\n\
-\n -load-vernac-source f load Coq file f.v (Load \"f\".)\
-\n -l f (idem)\
-\n -load-vernac-source-verbose f load Coq file f.v (Load Verbose \"f\".)\
-\n -lv f (idem)\
-\n -load-vernac-object lib\
-\n load Coq library lib (Require lib)\
-\n -rfrom root lib load Coq library lib (From root Require lib.)\
-\n -require-import lib, -ri lib\
-\n load and import Coq library lib\
-\n (equivalent to Require Import lib.)\
-\n -require-export lib, -re lib\
-\n load and transitively import Coq library lib\
-\n (equivalent to Require Export lib.)\
-\n -require-import-from root lib, -rifrom root lib\
-\n load and import Coq library lib\
-\n (equivalent to From root Require Import lib.)\
-\n -require-export-from root lib, -refrom root lib\
-\n load and transitively import Coq library lib\
-\n (equivalent to From root Require Export lib.)\
-\n\
-\n -where print Coq's standard library location and exit\
-\n -config, --config print Coq's configuration information and exit\
-\n -v, --version print Coq version and exit\
-\n -print-version print Coq version in easy to parse format and exit\
-\n -list-tags print highlight color tags known by Coq and exit\
-\n\
-\n -quiet unset display of extra information (implies -w \"-all\")\
-\n -w (w1,..,wn) configure display of warnings\
-\n -color (yes|no|auto) configure color output\
-\n -emacs tells Coq it is executed under Emacs\
-\n\
-\n -q skip loading of rcfile\
-\n -init-file f set the rcfile to f\
-\n -bt print backtraces (requires configure debug flag)\
-\n -debug debug mode (implies -bt)\
-\n -xml-debug debug mode and print XML messages to/from coqide\
-\n -diffs (on|off|removed) highlight differences between proof steps\
-\n -stm-debug STM debug mode (will trace every transaction)\
-\n -noglob do not dump globalizations\
-\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\
-\n -impredicative-set set sort Set impredicative\
-\n -allow-sprop allow using the proof irrelevant SProp sort\
-\n -disallow-sprop forbid using the proof irrelevant SProp sort\
-\n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\
-\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
-\n -type-in-type disable universe consistency checking\
-\n -mangle-names x mangle auto-generated names using prefix x\
-\n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\
-\n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\
-\n -unset \"Foo Bar\" disable Foo Bar (as Unset Foo Bar. in a file)\
-\n -time display the time taken by each command\
-\n -profile-ltac display the time taken by each (sub)tactic\
-\n -m, --memory display total heap size at program exit\
-\n (use environment variable\
-\n OCAML_GC_STATS=\"/tmp/gclog.txt\"\
-\n for full Gc stats dump)\
-\n -bytecode-compiler (yes|no) enable the vm_compute reduction machine\
-\n -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
-\n -native-output-dir <directory> set the output directory for native objects\
-\n -nI dir OCaml include directories for the native compiler (default if not set) \
-\n -h, -help, --help print this list of options\
-\n"
-
-(* print the usage *)
-
-type specific_usage = {
- executable_name : string;
- extra_args : string;
- extra_options : string;
-}
-
-let print_usage co { executable_name; extra_args; extra_options } =
- print_usage_common co ("Usage: " ^ executable_name ^ " <options> " ^ extra_args ^ "\n\n");
- output_string co extra_options
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
deleted file mode 100644
index cbc3b4f7e8..0000000000
--- a/toplevel/usage.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq 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) *)
-(************************************************************************)
-
-(** {6 Prints the version number on the standard output. } *)
-
-val version : unit -> unit
-val machine_readable_version : unit -> unit
-
-(** {6 extra arguments or options to print when asking usage for a
- given executable. } *)
-
-type specific_usage = {
- executable_name : string;
- extra_args : string;
- extra_options : string;
-}
-
-(** {6 Prints the generic part and specific part of usage for a
- given executable. } *)
-
-val print_usage : out_channel -> specific_usage -> unit
-
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index 59e10b09a0..b0d7bb6f78 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -9,9 +9,10 @@
(************************************************************************)
let worker_parse_extra ~opts extra_args =
- (), extra_args
+ let stm_opts, extra_args = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extra_args in
+ ((),stm_opts), extra_args
-let worker_init init () ~opts =
+let worker_init init ((),_) ~opts =
Flags.quiet := true;
init ();
Coqtop.init_toploop opts
@@ -30,6 +31,6 @@ let start ~init ~loop name =
help = worker_specific_usage name;
opts = Coqargs.default;
init = worker_init init;
- run = (fun () ~opts:_ _state (* why is state not used *) -> loop ());
+ run = (fun ((),_) ~opts:_ _state (* why is state not used *) -> loop ());
} in
start_coq custom
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:02:16 +0000