aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cErrors.ml7
-rw-r--r--lib/cErrors.mli11
-rw-r--r--lib/cMap.ml10
-rw-r--r--lib/cMap.mli2
-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/cSig.mli6
-rw-r--r--lib/cUnix.ml5
-rw-r--r--lib/cUnix.mli7
-rw-r--r--lib/control.ml25
-rw-r--r--lib/control.mli14
-rw-r--r--lib/dyn.ml10
-rw-r--r--lib/dyn.mli1
-rw-r--r--lib/envars.ml12
-rw-r--r--lib/feedback.ml38
-rw-r--r--lib/feedback.mli8
-rw-r--r--lib/flags.ml77
-rw-r--r--lib/flags.mli56
-rw-r--r--lib/hMap.ml26
-rw-r--r--lib/lib.mllib2
-rw-r--r--lib/loc.ml6
-rw-r--r--lib/loc.mli11
-rw-r--r--lib/pp.ml1
-rw-r--r--lib/pp.mli3
-rw-r--r--lib/system.ml6
-rw-r--r--lib/system.mli3
26 files changed, 147 insertions, 200 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 3f4e8aa12..eaffc28ac 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -91,7 +91,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with
let print_anomaly askreport e =
if askreport then
- hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e) ++ spc ()) ++
+ hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e)) ++ spc () ++
hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")
else
hov 0 (raw_anomaly e)
@@ -137,8 +137,3 @@ let handled e =
let bottom _ = raise Bottom in
try let _ = print_gen bottom !handle_stack e in true
with Bottom -> false
-
-(* Deprecated functions *)
-let error string = user_err (str string)
-let user_err_loc (loc,hdr,msg) = user_err ~loc ~hdr msg
-let errorlabstrm hdr msg = user_err ~hdr msg
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index f3253979f..6fcc97a91 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -93,14 +93,3 @@ val noncritical : exn -> bool
(** Check whether an exception is handled by some toplevel printer. The
[Anomaly] exception is never handled. *)
val handled : exn -> bool
-
-(** Deprecated functions *)
-val error : string -> 'a
- [@@ocaml.deprecated "use [user_err] instead"]
-
-val errorlabstrm : string -> Pp.t -> 'a
- [@@ocaml.deprecated "use [user_err ~hdr] instead"]
-
-val user_err_loc : Loc.t * string * Pp.t -> 'a
- [@@ocaml.deprecated "use [user_err ~loc] instead"]
-
diff --git a/lib/cMap.ml b/lib/cMap.ml
index 0ecb40209..b4c4aedd0 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -26,7 +26,7 @@ sig
include CSig.MapS
module Set : CSig.SetS with type elt = key
val get : key -> 'a t -> 'a
- val update : key -> 'a -> 'a t -> 'a t
+ val set : key -> 'a -> 'a t -> 'a t
val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
val domain : 'a t -> Set.t
val bind : (key -> 'a) -> Set.t -> 'a t
@@ -50,7 +50,7 @@ end
module MapExt (M : Map.OrderedType) :
sig
type 'a map = 'a Map.Make(M).t
- val update : M.t -> 'a -> 'a map -> 'a map
+ val set : M.t -> 'a -> 'a map -> 'a map
val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map
val domain : 'a map -> Set.Make(M).t
val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map
@@ -93,19 +93,19 @@ struct
let set_prj : set -> _set = Obj.magic
let set_inj : _set -> set = Obj.magic
- let rec update k v (s : 'a map) : 'a map = match map_prj s with
+ let rec set k v (s : 'a map) : 'a map = match map_prj s with
| MEmpty -> raise Not_found
| MNode (l, k', v', r, h) ->
let c = M.compare k k' in
if c < 0 then
- let l' = update k v l in
+ let l' = set k v l in
if l == l' then s
else map_inj (MNode (l', k', v', r, h))
else if c = 0 then
if v' == v then s
else map_inj (MNode (l, k', v, r, h))
else
- let r' = update k v r in
+ let r' = set k v r in
if r == r' then s
else map_inj (MNode (l, k', v', r', h))
diff --git a/lib/cMap.mli b/lib/cMap.mli
index f65036139..5e65bd200 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -34,7 +34,7 @@ sig
val get : key -> 'a t -> 'a
(** Same as {!find} but fails an assertion instead of raising [Not_found] *)
- val update : key -> 'a -> 'a t -> 'a t
+ val set : key -> 'a -> 'a t -> 'a t
(** Same as [add], but expects the key to be present, and thus faster.
@raise Not_found when the key is unbound in the map. *)
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/cSig.mli b/lib/cSig.mli
index 6910cbbf0..32e9d2af0 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -56,6 +56,12 @@ sig
val is_empty: 'a t -> bool
val mem: key -> 'a t -> bool
val add: key -> 'a -> 'a t -> 'a t
+ (* when Coq requires OCaml 4.06 or later, can add:
+
+ val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
+
+ allowing Coq to use OCaml's "update"
+ *)
val singleton: key -> 'a -> 'a t
val remove: key -> 'a t -> 'a t
val merge:
diff --git a/lib/cUnix.ml b/lib/cUnix.ml
index 867f86a74..34fb660db 100644
--- a/lib/cUnix.ml
+++ b/lib/cUnix.ml
@@ -14,6 +14,11 @@ type load_path = physical_path list
let physical_path_of_string s = s
let string_of_physical_path p = p
+let escaped_string_of_physical_path p =
+ (* We assume a reasonable-enough path (typically utf8) and prevents
+ the presence of space; other escapings might be useful... *)
+ if String.contains p ' ' then "\"" ^ p ^ "\"" else p
+
let path_to_list p =
let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in
Str.split sep p
diff --git a/lib/cUnix.mli b/lib/cUnix.mli
index a39481404..d08dc4c40 100644
--- a/lib/cUnix.mli
+++ b/lib/cUnix.mli
@@ -14,9 +14,12 @@ type load_path = physical_path list
val physical_path_of_string : string -> physical_path
val string_of_physical_path : physical_path -> string
+(** Escape what has to be escaped (e.g. surround with quotes if with spaces) *)
+val escaped_string_of_physical_path : physical_path -> string
+
val canonical_path_name : string -> string
-(** remove all initial "./" in a path *)
+(** Remove all initial "./" in a path *)
val remove_path_dot : string -> string
(** If a path [p] starts with the current directory $PWD then
@@ -61,6 +64,6 @@ val sys_command : string -> string list -> Unix.process_status
val waitpid_non_intr : int -> Unix.process_status
-(** checks if two file names refer to the same (existing) file *)
+(** Check if two file names refer to the same (existing) file *)
val same_file : string -> string -> bool
diff --git a/lib/control.ml b/lib/control.ml
index f5d7df204..c6489938e 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -12,21 +12,18 @@ 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
(** This function does not work on windows, sigh... *)
-let unix_timeout n f e =
+let unix_timeout n f x e =
let timeout_handler _ = raise e in
let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
let _ = Unix.alarm n in
@@ -35,7 +32,7 @@ let unix_timeout n f e =
Sys.set_signal Sys.sigalrm psh
in
try
- let res = f () in
+ let res = f x in
restore_timeout ();
res
with e ->
@@ -43,7 +40,7 @@ let unix_timeout n f e =
restore_timeout ();
Exninfo.iraise e
-let windows_timeout n f e =
+let windows_timeout n f x e =
let killed = ref false in
let exited = ref false in
let thread init =
@@ -60,7 +57,7 @@ let windows_timeout n f e =
let init = Unix.gettimeofday () in
let _id = Thread.create thread init in
try
- let res = f () in
+ let res = f x in
let () = killed := true in
let cur = Unix.gettimeofday () in
(** The thread did not interrupt, but the computation took longer than
@@ -80,12 +77,10 @@ let windows_timeout n f e =
let e = Backtrace.add_backtrace e in
Exninfo.iraise e
-type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }
+type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b }
let timeout_fun = match Sys.os_type with
-| "Unix" | "Cygwin" -> ref { timeout = unix_timeout }
-| _ -> ref { timeout = windows_timeout }
+| "Unix" | "Cygwin" -> { timeout = unix_timeout }
+| _ -> { timeout = windows_timeout }
-let set_timeout f = timeout_fun := f
-
-let timeout n f e = !timeout_fun.timeout n f e
+let timeout n f e = timeout_fun.timeout n f e
diff --git a/lib/control.mli b/lib/control.mli
index 337cdf67b..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) *)
@@ -16,11 +19,6 @@ val check_for_interrupt : unit -> unit
(** Use this function as a potential yield function. If {!interrupt} has been
set, il will raise [Sys.Break]. *)
-val timeout : int -> (unit -> 'a) -> exn -> 'a
-(** [timeout n f e] tries to compute [f], and if it fails to do so before [n]
- seconds, it raises [e] instead. *)
-
-type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }
-
-val set_timeout : timeout -> unit
-(** Set a particular timeout function. *)
+val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b
+(** [timeout n f x e] tries to compute [f x], and if it fails to do so
+ before [n] seconds, it raises [e] instead. *)
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 83e673d2c..64535d35f 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -55,6 +55,8 @@ sig
include PreS
module Easy : sig
+
+ val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
val make_dyn : string -> ('a -> t) * (t -> 'a)
val inj : 'a -> 'a tag -> t
val prj : t -> 'a tag -> 'a option
@@ -129,8 +131,9 @@ end
include Self
module Easy = struct
+
(* now tags are opaque, we can do the trick *)
-let make_dyn (s : string) =
+let make_dyn_tag (s : string) =
(fun (type a) (tag : a tag) ->
let infun : (a -> t) = fun x -> Dyn (tag, x) in
let outfun : (t -> a) = fun (Dyn (t, x)) ->
@@ -138,9 +141,12 @@ let make_dyn (s : string) =
| None -> assert false
| Some CSig.Refl -> x
in
- (infun, outfun))
+ infun, outfun, tag)
(create s)
+let make_dyn (s : string) =
+ let inf, outf, _ = make_dyn_tag s in inf, outf
+
let inj x tag = Dyn(tag,x)
let prj : type a. t -> a tag -> a option =
fun (Dyn(tag',x)) tag ->
diff --git a/lib/dyn.mli b/lib/dyn.mli
index e0e1a9d14..2206394e2 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -53,6 +53,7 @@ val dump : unit -> (int * string) list
module Easy : sig
(* To create a dynamic type on the fly *)
+ val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
val make_dyn : string -> ('a -> t) * (t -> 'a)
(* For types declared with the [create] function above *)
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/feedback.ml b/lib/feedback.ml
index 7a126363c..1007582e0 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -63,6 +63,7 @@ let set_id_for_feedback ?(route=default_route) d i =
span_id := i;
feedback_route := route
+let warn_no_listeners = ref true
let feedback ?did ?id ?route what =
let m = {
contents = what;
@@ -70,6 +71,8 @@ let feedback ?did ?id ?route what =
doc_id = Option.default !doc_id did;
span_id = Option.default !span_id id;
} in
+ if !warn_no_listeners && Hashtbl.length feeders = 0 then
+ Format.eprintf "Warning, feedback message received but no listener to handle it!@\n%!";
Hashtbl.iter (fun _ f -> f m) feeders
(* Logging messages *)
@@ -81,3 +84,38 @@ let msg_notice ?loc x = feedback_logger ?loc Notice x
let msg_warning ?loc x = feedback_logger ?loc Warning x
let msg_error ?loc x = feedback_logger ?loc Error x
let msg_debug ?loc x = feedback_logger ?loc Debug x
+
+(* Helper for tools willing to understand only the messages *)
+let console_feedback_listener fmt =
+ let open Format in
+ let pp_lvl fmt lvl = match lvl with
+ | Error -> fprintf fmt "Error: "
+ | Info -> fprintf fmt "Info: "
+ | Debug -> fprintf fmt "Debug: "
+ | Warning -> fprintf fmt "Warning: "
+ | Notice -> fprintf fmt ""
+ in
+ let pp_loc fmt loc = let open Loc in match loc with
+ | None -> fprintf fmt ""
+ | Some loc ->
+ let where =
+ match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in
+ fprintf fmt "\"%s\", line %d, characters %d-%d:@\n"
+ where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in
+ let checker_feed (fb : feedback) =
+ match fb.contents with
+ | Processed -> ()
+ | Incomplete -> ()
+ | Complete -> ()
+ | ProcessingIn _ -> ()
+ | InProgress _ -> ()
+ | WorkerStatus (_,_) -> ()
+ | AddedAxiom -> ()
+ | GlobRef (_,_,_,_,_) -> ()
+ | GlobDef (_,_,_,_) -> ()
+ | FileDependency (_,_) -> ()
+ | FileLoaded (_,_) -> ()
+ | Custom (_,_,_) -> ()
+ | Message (lvl,loc,msg) ->
+ fprintf fmt "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg
+ in checker_feed
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 73b84614f..62b909516 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -99,3 +99,11 @@ val msg_error : ?loc:Loc.t -> Pp.t -> unit
val msg_debug : ?loc:Loc.t -> Pp.t -> unit
(** For debugging purposes *)
+
+val console_feedback_listener : Format.formatter -> feedback -> unit
+(** Helper for tools willing to print to the feedback system *)
+
+val warn_no_listeners : bool ref
+(** The library will print a warning to the console if no listener is
+ available by default; ML-clients willing to use Coq without a
+ feedback handler should set this to false. *)
diff --git a/lib/flags.ml b/lib/flags.ml
index a53a866ab..644f66d02 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,13 +6,17 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-let with_option o f x =
- let old = !o in o:=true;
- try let r = f x in if !o = true then o := old; r
- with reraise ->
- let reraise = Backtrace.add_backtrace reraise in
- let () = o := old in
- Exninfo.iraise reraise
+let with_modified_ref r nf f x =
+ let old_ref = !r in r := nf !r;
+ try let res = f x in r := old_ref; res
+ with reraise ->
+ let reraise = Backtrace.add_backtrace reraise in
+ r := old_ref;
+ Exninfo.iraise reraise
+
+let with_option o f x = with_modified_ref o (fun _ -> true) f x
+let without_option o f x = with_modified_ref o (fun _ -> false) f x
+let with_extra_values o l f x = with_modified_ref o (fun ol -> ol@l) f x
let with_options ol f x =
let vl = List.map (!) ol in
@@ -25,58 +29,16 @@ let with_options ol f x =
let () = List.iter2 (:=) ol vl in
Exninfo.iraise reraise
-let without_option o f x =
- let old = !o in o:=false;
- try let r = f x in if !o = false then o := old; r
- with reraise ->
- let reraise = Backtrace.add_backtrace reraise in
- let () = o := old in
- Exninfo.iraise reraise
-
-let with_extra_values o l f x =
- let old = !o in o:=old@l;
- try let r = f x in o := old; r
- with reraise ->
- let reraise = Backtrace.add_backtrace reraise in
- let () = o := old in
- Exninfo.iraise reraise
-
let boot = ref false
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
@@ -140,10 +102,6 @@ let verbosely f x = without_option quiet f x
let if_silent f x = if !quiet then f x
let if_verbose f x = if not !quiet then f x
-let make_silent flag = quiet := flag
-let is_silent () = !quiet
-let is_verbose () = not !quiet
-
let auto_intros = ref true
let make_auto_intros flag = auto_intros := flag
let is_auto_intros () = !auto_intros
@@ -195,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
@@ -211,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 5233e72a2..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 *)
@@ -87,14 +66,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b
val if_silent : ('a -> unit) -> 'a -> unit
val if_verbose : ('a -> unit) -> 'a -> unit
-(* Deprecated *)
-val make_silent : bool -> unit
-[@@ocaml.deprecated "Please use Flags.quiet"]
-val is_silent : unit -> bool
-[@@ocaml.deprecated "Please use Flags.quiet"]
-val is_verbose : unit -> bool
-[@@ocaml.deprecated "Please use Flags.quiet"]
-
(* Miscellaneus flags for vernac *)
val make_auto_intros : bool -> unit
val is_auto_intros : unit -> bool
@@ -118,6 +89,15 @@ val warn : bool ref
val make_warn : bool -> unit
val if_warn : ('a -> unit) -> 'a -> unit
+(** [with_modified_ref r nf f x] Temporarily modify a reference in the
+ call to [f x] . Be very careful with these functions, it is very
+ easy to fall in the typical problem with effects:
+
+ with_modified_ref r nf f x y != with_modified_ref r nf (f x) y
+
+*)
+val with_modified_ref : 'c ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b
+
(** Temporarily activate an option (to activate option [o] on [f x y z],
use [with_option o (f x y) z]) *)
val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
@@ -142,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/hMap.ml b/lib/hMap.ml
index c69efdb71..37079af78 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -47,7 +47,7 @@ struct
try
let m = Int.Map.find h s in
let m = Set.add x m in
- Int.Map.update h m s
+ Int.Map.set h m s
with Not_found ->
let m = Set.singleton x in
Int.Map.add h m s
@@ -65,7 +65,7 @@ struct
if Set.is_empty m then
Int.Map.remove h s
else
- Int.Map.update h m s
+ Int.Map.set h m s
with Not_found -> s
let height s = Int.Map.height s
@@ -135,7 +135,7 @@ struct
let s' = Int.Map.find h accu in
let si = Set.filter (fun e -> not (Set.mem e s)) s' in
if Set.is_empty si then Int.Map.remove h accu
- else Int.Map.update h si accu
+ else Int.Map.set h si accu
with Not_found -> accu
in
Int.Map.fold fold s2 s1
@@ -242,11 +242,19 @@ struct
try
let m = Int.Map.find h s in
let m = Map.add k x m in
- Int.Map.update h m s
+ Int.Map.set h m s
with Not_found ->
let m = Map.singleton k x in
Int.Map.add h m s
+ (* when Coq requires OCaml 4.06 or later, the module type
+ CSig.MapS may include the signature of OCaml's "update",
+ requiring an implementation here, which could be just:
+
+ let update k f s = assert false (* not implemented *)
+
+ *)
+
let singleton k x =
let h = M.hash k in
Int.Map.singleton h (Map.singleton k x)
@@ -259,7 +267,7 @@ struct
if Map.is_empty m then
Int.Map.remove h s
else
- Int.Map.update h m s
+ Int.Map.set h m s
with Not_found -> s
let merge f s1 s2 =
@@ -359,7 +367,7 @@ struct
let h = M.hash k in
let m = Int.Map.find h s in
let m = Map.modify k f m in
- Int.Map.update h m s
+ Int.Map.set h m s
let bind f s =
let fb m = Map.bind f m in
@@ -367,11 +375,11 @@ struct
let domain s = Int.Map.map Map.domain s
- let update k x s =
+ let set k x s =
let h = M.hash k in
let m = Int.Map.find h s in
- let m = Map.update k x m in
- Int.Map.update h m s
+ let m = Map.set k x m in
+ Int.Map.set h m s
let smartmap f s =
let fs m = Map.smartmap f m in
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
diff --git a/lib/loc.ml b/lib/loc.ml
index 4a935a9d9..2cf4d3960 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -84,9 +84,3 @@ let raise ?loc e =
let info = Exninfo.add Exninfo.null location loc in
Exninfo.iraise (e, info)
-(** Deprecated *)
-let located_fold_left f x (_,a) = f x a
-let located_iter2 f (_,a) (_,b) = f a b
-let down_located f (_,a) = f a
-
-
diff --git a/lib/loc.mli b/lib/loc.mli
index fde490cc8..800940f21 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -65,14 +65,3 @@ val tag : ?loc:t -> 'a -> 'a located
val map : ('a -> 'b) -> 'a located -> 'b located
(** Modify an object carrying a location *)
-
-(** Deprecated functions *)
-val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
- [@@ocaml.deprecated "use pattern matching"]
-
-val down_located : ('a -> 'b) -> 'a located -> 'b
- [@@ocaml.deprecated "use pattern matching"]
-
-val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
- [@@ocaml.deprecated "use pattern matching"]
-
diff --git a/lib/pp.ml b/lib/pp.ml
index c3338688d..770e650cb 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-06 15:25:51 +0000