diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/cProfile.ml (renamed from lib/profile.ml) | 0 | ||||
-rw-r--r-- | lib/cProfile.mli (renamed from lib/profile.mli) | 0 | ||||
-rw-r--r-- | lib/control.ml | 7 | ||||
-rw-r--r-- | lib/control.mli | 3 | ||||
-rw-r--r-- | lib/envars.ml | 12 | ||||
-rw-r--r-- | lib/flags.ml | 39 | ||||
-rw-r--r-- | lib/flags.mli | 39 | ||||
-rw-r--r-- | lib/lib.mllib | 2 | ||||
-rw-r--r-- | lib/pp.ml | 1 | ||||
-rw-r--r-- | lib/pp.mli | 3 | ||||
-rw-r--r-- | lib/system.ml | 6 | ||||
-rw-r--r-- | lib/system.mli | 3 |
12 files changed, 21 insertions, 94 deletions
diff --git a/lib/profile.ml b/lib/cProfile.ml index 0bc226a45..0bc226a45 100644 --- a/lib/profile.ml +++ b/lib/cProfile.ml diff --git a/lib/profile.mli b/lib/cProfile.mli index cae4397a1..cae4397a1 100644 --- a/lib/profile.mli +++ b/lib/cProfile.mli diff --git a/lib/control.ml b/lib/control.ml index d936d7557..c6489938e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -12,15 +12,12 @@ let interrupt = ref false let steps = ref 0 -let are_we_threading = lazy ( - match !Flags.async_proofs_mode with - | Flags.APon -> true - | _ -> false) +let enable_thread_delay = ref false let check_for_interrupt () = if !interrupt then begin interrupt := false; raise Sys.Break end; incr steps; - if !steps = 1000 && Lazy.force are_we_threading then begin + if !enable_thread_delay && !steps = 1000 then begin Thread.delay 0.001; steps := 0; end diff --git a/lib/control.mli b/lib/control.mli index f6c63ffb3..261b07693 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -8,6 +8,9 @@ (** Global control of Coq. *) +(** Will periodically call [Thread.delay] if set to true *) +val enable_thread_delay : bool ref + val interrupt : bool ref (** Coq interruption: set the following boolean reference to interrupt Coq (it eventually raises [Break], simulating a Ctrl-C) *) diff --git a/lib/envars.ml b/lib/envars.ml index 206d75033..8ebf84057 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -153,19 +153,17 @@ let coqpath = let exe s = s ^ Coq_config.exec_extension -let ocamlfind () = - if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind +let ocamlfind () = Coq_config.ocamlfind (** {2 Camlp4 paths} *) let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) let camlp4bin () = - if !Flags.camlp4bin_spec then !Flags.camlp4bin else - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () - with Not_found -> - Coq_config.camlp4bin + if !Flags.boot then Coq_config.camlp4bin else + try guess_camlp4bin () + with Not_found -> + Coq_config.camlp4bin let camlp4 () = camlp4bin () / exe Coq_config.camlp4 diff --git a/lib/flags.ml b/lib/flags.ml index ddc8f8482..644f66d02 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -35,36 +35,10 @@ let record_aux_file = ref false let test_mode = ref false -type async_proofs = APoff | APonLazy | APon -let async_proofs_mode = ref APoff -type cache = Force -let async_proofs_cache = ref None -let async_proofs_n_workers = ref 1 -let async_proofs_n_tacworkers = ref 2 -let async_proofs_private_flags = ref None -let async_proofs_full = ref false -let async_proofs_never_reopen_branch = ref false -let async_proofs_flags_for_workers = ref [] let async_proofs_worker_id = ref "master" -type priority = Low | High -let async_proofs_worker_priority = ref Low -let string_of_priority = function Low -> "low" | High -> "high" -let priority_of_string = function - | "low" -> Low - | "high" -> High - | _ -> raise (Invalid_argument "priority_of_string") -type tac_error_filter = [ `None | `Only of string list | `All ] -let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) -let async_proofs_cmd_error_resilience = ref true - -let async_proofs_is_worker () = - !async_proofs_worker_id <> "master" -let async_proofs_is_master () = - !async_proofs_mode = APon && !async_proofs_worker_id = "master" -let async_proofs_delegation_threshold = ref 0.03 +let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let debug = ref false -let stm_debug = ref false let in_debugger = ref false let in_toplevel = ref false @@ -179,14 +153,6 @@ let is_standard_doc_url url = let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" -(* Options for changing ocamlfind (used by coqmktop) *) -let ocamlfind_spec = ref false -let ocamlfind = ref Coq_config.camlbin - -(* Options for changing camlp4bin (used by coqmktop) *) -let camlp4bin_spec = ref false -let camlp4bin = ref Coq_config.camlp4bin - (* Level of inlining during a functor application *) let default_inline_level = 100 @@ -195,12 +161,11 @@ let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level (* Native code compilation for conversion and normalization *) -let native_compiler = ref false +let output_native_objects = ref false (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false -let tactic_context_compat = ref false let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli index c4afb8318..000862b2c 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -21,35 +21,14 @@ val record_aux_file : bool ref val test_mode : bool ref (** Async-related flags *) -type async_proofs = APoff | APonLazy | APon -val async_proofs_mode : async_proofs ref -type cache = Force -val async_proofs_cache : cache option ref -val async_proofs_n_workers : int ref -val async_proofs_n_tacworkers : int ref -val async_proofs_private_flags : string option ref -val async_proofs_is_worker : unit -> bool -val async_proofs_is_master : unit -> bool -val async_proofs_full : bool ref -val async_proofs_never_reopen_branch : bool ref -val async_proofs_flags_for_workers : string list ref val async_proofs_worker_id : string ref -type priority = Low | High -val async_proofs_worker_priority : priority ref -val string_of_priority : priority -> string -val priority_of_string : string -> priority -type tac_error_filter = [ `None | `Only of string list | `All ] -val async_proofs_tac_error_resilience : tac_error_filter ref -val async_proofs_cmd_error_resilience : bool ref -val async_proofs_delegation_threshold : float ref +val async_proofs_is_worker : unit -> bool +(** Debug flags *) val debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref -(** Enable STM debugging *) -val stm_debug : bool ref - val profile : bool (* -ide_slave: printing will be more verbose, will affect stm caching *) @@ -143,27 +122,17 @@ val is_standard_doc_url : string -> bool val coqlib_spec : bool ref val coqlib : string ref -(** Options for specifying where OCaml binaries reside *) -val ocamlfind_spec : bool ref -val ocamlfind : string ref -val camlp4bin_spec : bool ref -val camlp4bin : string ref - (** Level of inlining during a functor application *) val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(** Native code compilation for conversion and normalization *) -val native_compiler : bool ref +(** When producing vo objects, also compile the native-code version *) +val output_native_objects : bool ref (** Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref -val tactic_context_compat : bool ref -(** Set to [true] to trigger the compatibility bugged context matching (old - context vs. appcontext) is set. *) - val profile_ltac : bool ref val profile_ltac_cutoff : float ref diff --git a/lib/lib.mllib b/lib/lib.mllib index 8791f0741..66f939a91 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -9,7 +9,7 @@ System CThread Spawn Trie -Profile +CProfile Explore Predicate Rtree @@ -208,6 +208,7 @@ let string_of_ppcmds c = let pr_comma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () +let pr_spcbar () = str " |" ++ spc () let pr_arg pr x = spc () ++ pr x let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x diff --git a/lib/pp.mli b/lib/pp.mli index 2d11cad86..d9be1c5ce 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -120,6 +120,9 @@ val pr_semicolon : unit -> t val pr_bar : unit -> t (** Well-spaced pipe bar. *) +val pr_spcbar : unit -> t +(** Pipe bar with space before and after. *) + val pr_arg : ('a -> t) -> 'a -> t (** Adds a space in front of its argument. *) diff --git a/lib/system.ml b/lib/system.ml index 4b5066ef4..2c8dbac7c 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -309,9 +309,3 @@ let with_time time f x = let msg2 = if time then "" else " (failure)" in Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e - -let process_id () = - Printf.sprintf "%d:%s:%d" (Unix.getpid ()) - (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id - else "master") - (Thread.id (Thread.self ())) diff --git a/lib/system.mli b/lib/system.mli index aa964abeb..c02bc9c8a 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -105,6 +105,3 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t val with_time : bool -> ('a -> 'b) -> 'a -> 'b - -(** {6 Name of current process.} *) -val process_id : unit -> string |