aboutsummaryrefslogtreecommitdiff
path: root/sysinit
diff options
context:
space:
mode:
Diffstat (limited to 'sysinit')
-rw-r--r--sysinit/coqargs.ml500
-rw-r--r--sysinit/coqargs.mli106
-rw-r--r--sysinit/coqinit.ml136
-rw-r--r--sysinit/coqinit.mli58
-rw-r--r--sysinit/coqloadpath.ml73
-rw-r--r--sysinit/coqloadpath.mli16
-rw-r--r--sysinit/dune7
-rw-r--r--sysinit/sysinit.mllib4
-rw-r--r--sysinit/usage.ml112
-rw-r--r--sysinit/usage.mli28
10 files changed, 1040 insertions, 0 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
new file mode 100644
index 0000000000..c4f12f6bb7
--- /dev/null
+++ b/sysinit/coqargs.ml
@@ -0,0 +1,500 @@
+(************************************************************************)
+(* * 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_debug () =
+ let () = Exninfo.record_backtrace true in
+ Flags.debug := true
+
+(******************************************************************************)
+
+type native_compiler = Coq_config.native_compiler =
+ NativeOff | NativeOn of { ondemand : bool }
+
+type top = TopLogical of Names.DirPath.t | TopPhysical of string
+
+type option_command =
+ | OptionSet of string option
+ | OptionUnset
+ | OptionAppend of string
+
+type injection_command =
+ | OptionInjection of (Goptions.option_name * option_command)
+ | RequireInjection of (string * string option * bool option)
+
+type coqargs_logic_config = {
+ impredicative_set : Declarations.set_predicativity;
+ indices_matter : bool;
+ type_in_type : bool;
+ toplevel_name : top;
+}
+
+type coqargs_config = {
+ logic : coqargs_logic_config;
+ rcfile : string option;
+ coqlib : string option;
+ enable_VM : bool;
+ native_compiler : native_compiler;
+ native_output_dir : CUnix.physical_path;
+ native_include_dirs : CUnix.physical_path list;
+ 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 : injection_command list;
+
+ inputstate : string option;
+}
+
+type coqargs_query =
+ | PrintWhere | PrintConfig
+ | PrintVersion | PrintMachineReadableVersion
+ | PrintHelp of Usage.specific_usage
+
+type coqargs_main =
+ | Queries of coqargs_query list
+ | Run
+
+type coqargs_post = {
+ memory_stat : 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;
+ type_in_type = false;
+ toplevel_name = TopLogical default_toplevel;
+}
+
+let default_config = {
+ logic = default_logic_config;
+ rcfile = None;
+ coqlib = None;
+ enable_VM = true;
+ native_compiler = default_native;
+ native_output_dir = ".coq-native";
+ native_include_dirs = [];
+ 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;
+}
+
+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 = 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 = OptionInjection (opt_name, value) :: opts.pre.injections }}
+
+(** Options for proof general *)
+let set_emacs opts =
+ let opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in
+ { opts with config = { opts.config with print_emacs = true }}
+
+let set_logic f oval =
+ { oval with config = { oval.config with logic = f oval.config.logic }}
+
+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_int_opt ~opt n =
+ if n = "" then None
+ else Some (get_int ~opt n)
+
+let get_float ~opt n =
+ try float_of_string n
+ with Failure _ ->
+ error_wrong_arg ("Error: float expected after option "^opt)
+
+let interp_set_option opt v old =
+ let open Goptions in
+ let opt = String.concat " " opt in
+ match old with
+ | BoolValue _ -> BoolValue (get_bool ~opt v)
+ | IntValue _ -> IntValue (get_int_opt ~opt v)
+ | StringValue _ -> StringValue v
+ | StringOptValue _ -> StringOptValue (Some v)
+
+let set_option = let open Goptions in function
+ | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
+ | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
+ | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
+ | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v
+
+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 ~usage ~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 ())
+ }}
+
+ |"-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" ->
+ let oval = add_set_option oval ["Mangle"; "Names"] (OptionSet None) in
+ add_set_option oval ["Mangle"; "Names"; "Prefix"] (OptionSet(Some(next ())))
+
+ |"-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 = TopLogical topname }}}
+
+ |"-topfile" ->
+ { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopPhysical (next()) }}}
+
+ |"-w" | "-W" ->
+ let w = next () in
+ if w = "none" then add_set_option oval ["Warnings"] (OptionSet(Some w))
+ else add_set_option oval ["Warnings"] (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 (OptionSet v)
+
+ | "-unset" ->
+ add_set_option oval (to_opt_key @@ next ()) 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 *)
+ |"-test-mode" -> Vernacinterp.test_mode := true; oval
+ |"-beautify" -> Flags.beautify := true; oval
+ |"-bt" -> Exninfo.record_backtrace true; oval
+ |"-config"|"--config" -> set_query oval PrintConfig
+ |"-debug" -> set_debug (); oval
+ |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval
+ |"-diffs" ->
+ add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ()))
+ |"-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 (OptionSet None)
+ |"-disallow-sprop" ->
+ add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
+ |"-sprop-cumulative" ->
+ warn_deprecated_sprop_cumul();
+ add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
+ |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
+ |"-m"|"--memory" -> { oval with post = { memory_stat = true }}
+ |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
+ |"-boot" -> { oval with pre = { oval.pre with boot = 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
+ |"-time" -> { oval with config = { oval.config with time = true }}
+ |"-type-in-type" -> set_logic (fun o -> { o with type_in_type = true }) oval
+ |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
+ |"-where" -> set_query oval PrintWhere
+ |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp usage)
+ |"-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 ~usage ~init args =
+ let opts, extra = parse_args ~usage ~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 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
+ Coqloadpath.init_load_path ~coqlib in
+ ml_path @ opts.pre.ml_includes ,
+ vo_path @ opts.pre.vo_includes
+
+let dirpath_of_file f =
+ let ldir0 =
+ try
+ let lp = Loadpath.find_load_path (Filename.dirname f) in
+ Loadpath.logical lp
+ with Not_found -> Libnames.default_root_prefix
+ in
+ let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in
+ let id = Names.Id.of_string f in
+ let ldir = Libnames.add_dirpath_suffix ldir0 id in
+ ldir
+
+let dirpath_of_top = function
+ | TopPhysical f -> dirpath_of_file f
+ | TopLogical dp -> dp
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
new file mode 100644
index 0000000000..aef50193f2
--- /dev/null
+++ b/sysinit/coqargs.mli
@@ -0,0 +1,106 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+val default_toplevel : Names.DirPath.t
+
+type native_compiler = Coq_config.native_compiler =
+ NativeOff | NativeOn of { ondemand : bool }
+
+type top = TopLogical of Names.DirPath.t | TopPhysical of string
+
+type option_command =
+ | OptionSet of string option
+ | OptionUnset
+ | OptionAppend of string
+
+type injection_command =
+ | OptionInjection of (Goptions.option_name * option_command)
+ (** Set flags or options before the initial state is ready. *)
+ | RequireInjection of (string * string option * bool option)
+ (** Require libraries before the initial state is
+ ready. Parameters follow [Library], that is to say,
+ [lib,prefix,import_export] means require library [lib] from
+ optional [prefix] and [import_export] if [Some false/Some true]
+ is used. *)
+
+type coqargs_logic_config = {
+ impredicative_set : Declarations.set_predicativity;
+ indices_matter : bool;
+ type_in_type : bool;
+ toplevel_name : top;
+}
+
+type coqargs_config = {
+ logic : coqargs_logic_config;
+ rcfile : string option;
+ coqlib : string option;
+ enable_VM : bool;
+ native_compiler : native_compiler;
+ native_output_dir : CUnix.physical_path;
+ native_include_dirs : CUnix.physical_path list;
+ 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 : injection_command list;
+
+ inputstate : string option;
+}
+
+type coqargs_query =
+ | PrintWhere | PrintConfig
+ | PrintVersion | PrintMachineReadableVersion
+ | PrintHelp of Usage.specific_usage
+
+type coqargs_main =
+ | Queries of coqargs_query list
+ | Run
+
+type coqargs_post = {
+ memory_stat : bool;
+}
+
+type t = {
+ config : coqargs_config;
+ pre : coqargs_pre;
+ main : coqargs_main;
+ post : coqargs_post;
+}
+
+(* Default options *)
+val default : t
+
+val parse_args : usage:Usage.specific_usage -> init:t -> string list -> t * string list
+
+val injection_commands : t -> injection_command list
+val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
+
+val dirpath_of_top : top -> Names.DirPath.t
+
+(* Common utilities *)
+
+val get_int : opt:string -> string -> int
+val get_int_opt : opt:string -> string -> int option
+val get_bool : opt:string -> string -> bool
+val get_float : opt:string -> string -> float
+val error_missing_arg : string -> 'a
+val error_wrong_arg : string -> 'a
+
+val set_option : Goptions.option_name * option_command -> unit
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
new file mode 100644
index 0000000000..16c8389de5
--- /dev/null
+++ b/sysinit/coqinit.ml
@@ -0,0 +1,136 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(** GC tweaking *)
+
+(** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
+ minor heap is heavily solicited. Unfortunately, the default size is far too
+ small, so we enlarge it a lot (128 times larger).
+
+ To better handle huge memory consumers, we also augment the default major
+ heap increment and the GC pressure coefficient.
+*)
+
+let set_gc_policy () =
+ Gc.set { (Gc.get ()) with
+ Gc.minor_heap_size = 32*1024*1024 (* 32Mwords x 8 bytes/word = 256Mb *)
+ ; Gc.space_overhead = 120
+ }
+
+let set_gc_best_fit () =
+ Gc.set { (Gc.get ()) with
+ Gc.allocation_policy = 2 (* best-fit *)
+ ; Gc.space_overhead = 200
+ }
+
+let init_gc () =
+ try
+ (* OCAMLRUNPARAM environment variable is set.
+ * In that case, we let ocamlrun to use the values provided by the user.
+ *)
+ ignore (Sys.getenv "OCAMLRUNPARAM")
+
+ with Not_found ->
+ (* OCAMLRUNPARAM environment variable is not set.
+ * In this case, we put in place our preferred configuration.
+ *)
+ set_gc_policy ();
+ if Coq_config.caml_version_nums >= [4;10;0] then set_gc_best_fit () else ()
+
+let init_ocaml () =
+ CProfile.init_profile ();
+ init_gc ();
+ Sys.catch_break false (* Ctrl-C is fatal during the initialisation *)
+
+let init_coqlib opts = match opts.Coqargs.config.Coqargs.coqlib with
+ | None when opts.Coqargs.pre.Coqargs.boot -> ()
+ | None ->
+ Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+ | Some s ->
+ Envars.set_user_coqlib s
+
+let print_query opts = let open Coqargs in function
+ | PrintVersion -> Usage.version ()
+ | PrintMachineReadableVersion -> Usage.machine_readable_version ()
+ | PrintWhere ->
+ let () = init_coqlib opts in
+ print_endline (Envars.coqlib ())
+ | PrintHelp h -> Usage.print_usage stderr h
+ | PrintConfig ->
+ let () = init_coqlib opts in
+ Envars.print_config stdout Coq_config.all_src_dirs
+
+let parse_arguments ~parse_extra ~usage ?(initial_args=Coqargs.default) () =
+ let opts, extras =
+ Coqargs.parse_args ~usage ~init:initial_args
+ (List.tl (Array.to_list Sys.argv)) in
+ let customopts, extras = parse_extra extras in
+ if not (CList.is_empty extras) then begin
+ prerr_endline ("Don't know what to do with "^String.concat " " extras);
+ prerr_endline "See -help for the list of supported options";
+ exit 1
+ end;
+ match opts.Coqargs.main with
+ | Coqargs.Queries q -> List.iter (print_query opts) q; exit 0
+ | Coqargs.Run -> opts, customopts
+
+let print_memory_stat () =
+ let open Pp in
+ (* -m|--memory from the command-line *)
+ Feedback.msg_notice
+ (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ());
+ (* operf-macro interface:
+ https://github.com/OCamlPro/operf-macro *)
+ try
+ let fn = Sys.getenv "OCAML_GC_STATS" in
+ let oc = open_out fn in
+ Gc.print_stat oc;
+ close_out oc
+ with _ -> ()
+
+let init_runtime opts =
+ let open Coqargs in
+ Lib.init ();
+ init_coqlib opts;
+ if opts.post.memory_stat then at_exit print_memory_stat;
+ Mltop.init_known_plugins ();
+
+ (* Configuration *)
+ Global.set_engagement opts.config.logic.impredicative_set;
+ Global.set_indices_matter opts.config.logic.indices_matter;
+ Global.set_check_universes (not opts.config.logic.type_in_type);
+ Global.set_VM opts.config.enable_VM;
+ Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
+ Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
+
+ (* Native output dir *)
+ Nativelib.output_dir := opts.config.native_output_dir;
+ Nativelib.include_dirs := opts.config.native_include_dirs;
+
+ (* Paths for loading stuff *)
+ let ml_load_path, vo_load_path = Coqargs.build_load_path opts in
+ List.iter Mltop.add_ml_dir ml_load_path;
+ List.iter Loadpath.add_vo_path vo_load_path;
+
+ injection_commands opts
+
+let require_file (dir, from, exp) =
+ let mp = Libnames.qualid_of_string dir in
+ let mfrom = Option.map Libnames.qualid_of_string from in
+ Flags.silently (Vernacentries.vernac_require mfrom exp) [mp]
+
+let handle_injection = function
+ | Coqargs.RequireInjection r -> require_file r
+ (* | LoadInjection l -> *)
+ | Coqargs.OptionInjection o -> Coqargs.set_option o
+
+let start_library ~top injections =
+ Flags.verbosely Declaremods.start_library top;
+ List.iter handle_injection injections
diff --git a/sysinit/coqinit.mli b/sysinit/coqinit.mli
new file mode 100644
index 0000000000..bea2186d81
--- /dev/null
+++ b/sysinit/coqinit.mli
@@ -0,0 +1,58 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(** Main etry point to the sysinit component, all other modules are private.
+
+ The following API shoud be called in order, and the first 3 steps only once
+ since they initialize global data. On the contrary step 4 can be called
+ many times to init the compilation of a unit.
+*)
+
+(** 1 initialization of OCaml's runtime
+
+ Profiling, GC parameters and signals. Nothing specific to Coq per se, but
+ the defaults here are good for Coq.
+ This API should be called up very early, or not at all. *)
+val init_ocaml : unit -> unit
+
+(** 2 parsing of Sys.argv
+
+ This API parses command line options which are known by Coq components.
+ Ideally it is functional, but some values in the `Flags` modules are set
+ on the spot instead of being represented as "injection commands" (a field
+ of Coqargs.t).
+
+ [parse_extra] and [usage] can be used to parse/document more options. *)
+val parse_arguments :
+ parse_extra:(string list -> 'a * string list) ->
+ usage:Usage.specific_usage ->
+ ?initial_args:Coqargs.t ->
+ unit ->
+ Coqargs.t * 'a
+
+(** 3 initialization of global runtime data
+
+ All global setup is done here, like COQLIB and the paths for native
+ compilation. If Coq is used to process multiple libraries, what is set up
+ here is really global and common to all of them.
+
+ The returned injections are options (as in "Set This Thing" or "Require
+ that") as specified on the command line.
+ The prelude is one of these (unless "-nois" is passed).
+
+ This API must be called, typically jsut after parsing arguments. *)
+val init_runtime : Coqargs.t -> Coqargs.injection_command list
+
+(** 4 Start a library (sets options and loads objects like the prelude)
+
+ Given the logical name [top] of the current library and the set of initial
+ options and required libraries, it starts its processing (see also
+ Declaremods.start_library) *)
+val start_library : top:Names.DirPath.t -> Coqargs.injection_command list -> unit
diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml
new file mode 100644
index 0000000000..8635345e00
--- /dev/null
+++ b/sysinit/coqloadpath.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(* * 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
+
+(* 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 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/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli
new file mode 100644
index 0000000000..d853e9ea54
--- /dev/null
+++ b/sysinit/coqloadpath.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(** 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 init_load_path
+ : coqlib:CUnix.physical_path
+ -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/sysinit/dune b/sysinit/dune
new file mode 100644
index 0000000000..04b46fb2a2
--- /dev/null
+++ b/sysinit/dune
@@ -0,0 +1,7 @@
+(library
+ (name sysinit)
+ (public_name coq.sysinit)
+ (synopsis "Coq's initialization")
+ (wrapped false)
+ (libraries coq.vernac)
+ )
diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib
new file mode 100644
index 0000000000..6e86536648
--- /dev/null
+++ b/sysinit/sysinit.mllib
@@ -0,0 +1,4 @@
+Usage
+Coqloadpath
+Coqargs
+Coqinit
diff --git a/sysinit/usage.ml b/sysinit/usage.ml
new file mode 100644
index 0000000000..1831a3f9b2
--- /dev/null
+++ b/sysinit/usage.ml
@@ -0,0 +1,112 @@
+(************************************************************************)
+(* * 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 -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/sysinit/usage.mli b/sysinit/usage.mli
new file mode 100644
index 0000000000..2d1a8e94cc
--- /dev/null
+++ b/sysinit/usage.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(* * 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:40:56 +0000