diff options
Diffstat (limited to 'sysinit')
| -rw-r--r-- | sysinit/coqargs.ml | 45 | ||||
| -rw-r--r-- | sysinit/coqargs.mli | 13 | ||||
| -rw-r--r-- | sysinit/coqinit.ml | 135 | ||||
| -rw-r--r-- | sysinit/coqinit.mli | 58 | ||||
| -rw-r--r-- | sysinit/dune | 1 | ||||
| -rw-r--r-- | sysinit/sysinit.mllib | 1 |
6 files changed, 224 insertions, 29 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 930c3b135f..32025ac434 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -35,12 +35,10 @@ let set_debug () = (******************************************************************************) -type color = [`ON | `AUTO | `EMACS | `OFF] - type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } -type interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string +type top = TopLogical of Names.DirPath.t | TopPhysical of string type option_command = | OptionSet of string option @@ -54,14 +52,13 @@ type injection_command = type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : interactive_top; + toplevel_name : 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; @@ -86,7 +83,7 @@ type coqargs_pre = { } type coqargs_query = - | PrintTags | PrintWhere | PrintConfig + | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of Usage.specific_usage @@ -120,7 +117,6 @@ 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"; @@ -181,18 +177,11 @@ let add_set_option opts opt_name value = (** 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 }} + { 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_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]) @@ -306,7 +295,7 @@ let get_native_compiler s = (* Main parsing routine *) (*s Parsing of the command line *) -let parse_args ~help ~init arglist : t * string list = +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 @@ -435,7 +424,6 @@ let parse_args ~help ~init arglist : t * string list = |"-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" -> set_debug (); oval |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval @@ -462,12 +450,11 @@ let parse_args ~help ~init arglist : t * string list = 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) + |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp usage) |"-v"|"--version" -> set_query oval PrintVersion |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion @@ -483,8 +470,8 @@ let parse_args ~help ~init arglist : t * string list = 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 parse_args ~usage ~init args = + let opts, extra = parse_args ~usage ~init args in let opts = { opts with pre = { opts.pre with @@ -513,3 +500,19 @@ let build_load_path opts = 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 index 894e0f2ef3..ebf367270d 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -8,14 +8,12 @@ (* * (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 interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string +type top = TopLogical of Names.DirPath.t | TopPhysical of string type option_command = | OptionSet of string option @@ -35,14 +33,13 @@ type injection_command = type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : interactive_top; + toplevel_name : 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; @@ -67,7 +64,7 @@ type coqargs_pre = { } type coqargs_query = - | PrintTags | PrintWhere | PrintConfig + | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of Usage.specific_usage @@ -90,11 +87,13 @@ type t = { (* Default options *) val default : t -val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list +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 diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml new file mode 100644 index 0000000000..cbecc52827 --- /dev/null +++ b/sysinit/coqinit.ml @@ -0,0 +1,135 @@ +(************************************************************************) +(* * 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_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/dune b/sysinit/dune index 6146aa60d0..04b46fb2a2 100644 --- a/sysinit/dune +++ b/sysinit/dune @@ -4,5 +4,4 @@ (synopsis "Coq's initialization") (wrapped false) (libraries coq.vernac) - (modules coqloadpath coqargs usage) ) diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib index 9d35a931bc..715de2bb82 100644 --- a/sysinit/sysinit.mllib +++ b/sysinit/sysinit.mllib @@ -1,3 +1,4 @@ Usage Coqloadpath Coqargs +Coqinit
\ No newline at end of file |