aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cSig.mli2
-rw-r--r--lib/dyn.ml43
-rw-r--r--lib/dyn.mli42
-rw-r--r--lib/exninfo.ml2
-rw-r--r--lib/feedback.ml22
-rw-r--r--lib/feedback.mli16
-rw-r--r--lib/flags.ml6
-rw-r--r--lib/flags.mli10
-rw-r--r--lib/future.ml82
-rw-r--r--lib/future.mli69
-rw-r--r--lib/genarg.ml2
-rw-r--r--lib/minisys.ml14
-rw-r--r--lib/segmenttree.ml8
-rw-r--r--lib/segmenttree.mli8
-rw-r--r--lib/spawn.ml4
-rw-r--r--lib/spawn.mli4
-rw-r--r--lib/store.ml6
-rw-r--r--lib/store.mli7
-rw-r--r--lib/system.ml8
-rw-r--r--lib/system.mli6
20 files changed, 148 insertions, 213 deletions
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 151cfbdca5..6910cbbf03 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -48,8 +48,6 @@ end
(** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml
documentation for more information. *)
-module type EmptyS = sig end
-
module type MapS =
sig
type key
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 6bd43455f6..83e673d2c0 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -11,6 +11,26 @@ sig
type 'a t
end
+module type MapS =
+sig
+ type t
+ type 'a obj
+ type 'a key
+ val empty : t
+ val add : 'a key -> 'a obj -> t -> t
+ val remove : 'a key -> t -> t
+ val find : 'a key -> t -> 'a obj
+ val mem : 'a key -> t -> bool
+
+ type any = Any : 'a key * 'a obj -> any
+
+ type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
+ val map : map -> t -> t
+
+ val iter : (any -> unit) -> t -> unit
+ val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+end
+
module type PreS =
sig
type 'a tag
@@ -24,24 +44,7 @@ type any = Any : 'a tag -> any
val name : string -> any option
-module Map(M : TParam) :
-sig
- type t
- val empty : t
- val add : 'a tag -> 'a M.t -> t -> t
- val remove : 'a tag -> t -> t
- val find : 'a tag -> t -> 'a M.t
- val mem : 'a tag -> t -> bool
-
- type any = Any : 'a tag * 'a M.t -> any
-
- type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
- val map : map -> t -> t
-
- val iter : (any -> unit) -> t -> unit
- val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
-
-end
+module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
val dump : unit -> (int * string) list
@@ -59,7 +62,7 @@ sig
end
-module Make(M : CSig.EmptyS) = struct
+module Make () = struct
module Self : PreS = struct
(* Dynamics, programmed with DANGER !!! *)
@@ -104,6 +107,8 @@ let dump () = Int.Map.bindings !dyntab
module Map(M : TParam) =
struct
type t = Obj.t M.t Int.Map.t
+type 'a obj = 'a M.t
+type 'a key = 'a tag
let cast : 'a M.t -> 'b M.t = Obj.magic
let empty = Int.Map.empty
let add tag v m = Int.Map.add tag (cast v) m
diff --git a/lib/dyn.mli b/lib/dyn.mli
index e43c8a9bcf..e0e1a9d140 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -13,6 +13,26 @@ sig
type 'a t
end
+module type MapS =
+sig
+ type t
+ type 'a obj
+ type 'a key
+ val empty : t
+ val add : 'a key -> 'a obj -> t -> t
+ val remove : 'a key -> t -> t
+ val find : 'a key -> t -> 'a obj
+ val mem : 'a key -> t -> bool
+
+ type any = Any : 'a key * 'a obj -> any
+
+ type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
+ val map : map -> t -> t
+
+ val iter : (any -> unit) -> t -> unit
+ val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+end
+
module type S =
sig
type 'a tag
@@ -26,24 +46,7 @@ type any = Any : 'a tag -> any
val name : string -> any option
-module Map(M : TParam) :
-sig
- type t
- val empty : t
- val add : 'a tag -> 'a M.t -> t -> t
- val remove : 'a tag -> t -> t
- val find : 'a tag -> t -> 'a M.t
- val mem : 'a tag -> t -> bool
-
- type any = Any : 'a tag * 'a M.t -> any
-
- type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
- val map : map -> t -> t
-
- val iter : (any -> unit) -> t -> unit
- val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
-
-end
+module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
val dump : unit -> (int * string) list
@@ -59,5 +62,4 @@ end
end
-(** FIXME: use OCaml 4.02 generative functors when available *)
-module Make(M : CSig.EmptyS) : S
+module Make () : S
diff --git a/lib/exninfo.ml b/lib/exninfo.ml
index d049dc6cff..167d3d6dc8 100644
--- a/lib/exninfo.ml
+++ b/lib/exninfo.ml
@@ -10,7 +10,7 @@
containing a pair composed of the distinguishing [token] and the backtrace
information. We discriminate the token by pointer equality. *)
-module Store = Store.Make(struct end)
+module Store = Store.Make ()
type 'a t = 'a Store.field
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 54d16a9be3..7a126363cc 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -15,6 +15,7 @@ type level =
| Warning
| Error
+type doc_id = int
type route_id = int
type feedback_content =
@@ -35,7 +36,8 @@ type feedback_content =
| Message of level * Loc.t option * Pp.t
type feedback = {
- id : Stateid.t;
+ doc_id : doc_id; (* The document being concerned *)
+ span_id : Stateid.t;
route : route_id;
contents : feedback_content;
}
@@ -52,23 +54,27 @@ let add_feeder =
let del_feeder fid = Hashtbl.remove feeders fid
let default_route = 0
-let feedback_id = ref Stateid.dummy
+let span_id = ref Stateid.dummy
+let doc_id = ref 0
let feedback_route = ref default_route
-let set_id_for_feedback ?(route=default_route) i =
- feedback_id := i; feedback_route := route
+let set_id_for_feedback ?(route=default_route) d i =
+ doc_id := d;
+ span_id := i;
+ feedback_route := route
-let feedback ?id ?route what =
+let feedback ?did ?id ?route what =
let m = {
contents = what;
- route = Option.default !feedback_route route;
- id = Option.default !feedback_id id;
+ route = Option.default !feedback_route route;
+ doc_id = Option.default !doc_id did;
+ span_id = Option.default !span_id id;
} in
Hashtbl.iter (fun _ f -> f m) feeders
(* Logging messages *)
let feedback_logger ?loc lvl msg =
- feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, msg))
+ feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, msg))
let msg_info ?loc x = feedback_logger ?loc Info x
let msg_notice ?loc x = feedback_logger ?loc Notice x
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 45a02d384a..73b84614f1 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -17,6 +17,9 @@ type level =
| Error
+(** Document unique identifier for serialization *)
+type doc_id = int
+
(** Coq "semantic" infos obtained during execution *)
type route_id = int
@@ -43,7 +46,8 @@ type feedback_content =
| Message of level * Loc.t option * Pp.t
type feedback = {
- id : Stateid.t; (* The document part concerned *)
+ doc_id : doc_id; (* The document being concerned *)
+ span_id : Stateid.t; (* The document part concerned *)
route : route_id; (* Extra routing info *)
contents : feedback_content; (* The payload *)
}
@@ -60,13 +64,13 @@ val add_feeder : (feedback -> unit) -> int
(** [del_feeder fid] removes the feeder with id [fid] *)
val del_feeder : int -> unit
-(** [feedback ?id ?route fb] produces feedback fb, with [route] and
- [id] set appropiatedly, if absent, it will use the defaults set by
- [set_id_for_feedback] *)
-val feedback : ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
+(** [feedback ?did ?sid ?route fb] produces feedback [fb], with
+ [route] and [did, sid] set appropiatedly, if absent, it will use
+ the defaults set by [set_id_for_feedback] *)
+val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
(** [set_id_for_feedback route id] Set the defaults for feedback *)
-val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit
+val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit
(** {6 output functions}
diff --git a/lib/flags.ml b/lib/flags.ml
index d4be81c61a..a53a866aba 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -42,12 +42,8 @@ let with_extra_values o l f x =
Exninfo.iraise reraise
let boot = ref false
-let load_init = ref true
-let batch_mode = ref false
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-let compilation_mode = ref BuildVo
-let compilation_output_name = ref None
+let record_aux_file = ref false
let test_mode = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 3024c60396..5233e72a25 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -11,14 +11,10 @@
(** Command-line flags *)
val boot : bool ref
-val load_init : bool ref
-(* Will affect STM caching *)
-val batch_mode : bool ref
-
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-val compilation_mode : compilation_mode ref
-val compilation_output_name : string option ref
+(** Set by coqtop to tell the kernel to output to the aux file; will
+ be eventually removed by cleanups such as PR#1103 *)
+val record_aux_file : bool ref
(* Flag set when the test-suite is called. Its only effect to display
verbose information for `Fail` *)
diff --git a/lib/future.ml b/lib/future.ml
index d9463aa0f1..09285ea27d 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -6,12 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* To deal with side effects we have to save/restore the system state *)
-type freeze
-let freeze = ref (fun () -> assert false : unit -> freeze)
-let unfreeze = ref (fun _ -> () : freeze -> unit)
-let set_freeze f g = freeze := f; unfreeze := g
-
let not_ready_msg = ref (fun name ->
Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
"Please wait or pass "^
@@ -30,6 +24,7 @@ let customize_not_here_msg f = not_here_msg := f
exception NotReady of string
exception NotHere of string
+
let _ = CErrors.register_handler (function
| NotReady name -> !not_ready_msg name
| NotHere name -> !not_here_msg name
@@ -59,7 +54,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat
and 'a comp =
| Delegated of (unit -> unit)
| Closure of (unit -> 'a)
- | Val of 'a * freeze option
+ | Val of 'a
| Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *)
and 'a comput =
@@ -74,7 +69,7 @@ let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x)))
let get x =
match !x with
- | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None))
+ | Finished v -> unnamed, UUID.invalid, id, ref (Val v)
| Ongoing (name, x) ->
try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c
with CEphemeron.InvalidKey ->
@@ -95,13 +90,13 @@ let is_exn kx = let _, _, _, x = get kx in match !x with
| Val _ | Closure _ | Delegated _ -> false
let peek_val kx = let _, _, _, x = get kx in match !x with
- | Val (v, _) -> Some v
+ | Val v -> Some v
| Exn _ | Closure _ | Delegated _ -> None
let uuid kx = let _, id, _, _ = get kx in id
-let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
-let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
+let from_val ?(fix_exn=id) v = create fix_exn (Val v)
+let from_here ?(fix_exn=id) v = create fix_exn (Val v)
let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
@@ -110,7 +105,7 @@ let create_delegate ?(blocking=true) ~name fix_exn =
let _, _, fix_exn, c = get ck in
assert (match !c with Delegated _ -> true | _ -> false);
begin match v with
- | `Val v -> c := Val (v, None)
+ | `Val v -> c := Val v
| `Exn e -> c := Exn (fix_exn e)
| `Comp f -> let _, _, _, comp = get f in c := !comp end;
signal () in
@@ -124,17 +119,16 @@ let create_delegate ?(blocking=true) ~name fix_exn =
ck, assignement signal ck
(* TODO: get rid of try/catch to be stackless *)
-let rec compute ~pure ck : 'a value =
+let rec compute ck : 'a value =
let _, _, fix_exn, c = get ck in
match !c with
- | Val (x, _) -> `Val x
+ | Val x -> `Val x
| Exn (e, info) -> `Exn (e, info)
- | Delegated wait -> wait (); compute ~pure ck
+ | Delegated wait -> wait (); compute ck
| Closure f ->
try
let data = f () in
- let state = if pure then None else Some (!freeze ()) in
- c := Val (data, state); `Val data
+ c := Val data; `Val data
with e ->
let e = CErrors.push e in
let e = fix_exn e in
@@ -142,60 +136,30 @@ let rec compute ~pure ck : 'a value =
| (NotReady _, _) -> `Exn e
| _ -> c := Exn e; `Exn e
-let force ~pure x = match compute ~pure x with
+let force x = match compute x with
| `Val v -> v
| `Exn e -> Exninfo.iraise e
-let chain ~pure ck f =
+let chain ck f =
let name, uuid, fix_exn, c = get ck in
create ~uuid ~name fix_exn (match !c with
- | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck))
+ | Closure _ | Delegated _ -> Closure (fun () -> f (force ck))
| Exn _ as x -> x
- | Val (v, None) when pure -> Val (f v, None)
- | Val (v, Some _) when pure -> Val (f v, None)
- | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
- | Val (v, None) ->
- match !ck with
- | Finished _ -> CErrors.anomaly(Pp.str
- "Future.chain ~pure:false call on an already joined computation.")
- | Ongoing _ -> CErrors.anomaly(Pp.strbrk(
- "Future.chain ~pure:false call on a pure computation. "^
- "This can happen if the computation was initial created with "^
- "Future.from_val or if it was Future.chain ~pure:true with a "^
- "function and later forced.")))
+ | Val v -> Val (f v))
let create fix_exn f = create fix_exn (Closure f)
let replace kx y =
let _, _, _, x = get kx in
match !x with
- | Exn _ -> x := Closure (fun () -> force ~pure:false y)
+ | Exn _ -> x := Closure (fun () -> force y)
| _ -> CErrors.anomaly
(Pp.str "A computation can be replaced only if is_exn holds.")
-let purify f x =
- let state = !freeze () in
- try
- let v = f x in
- !unfreeze state;
- v
- with e ->
- let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
-
-let transactify f x =
- let state = !freeze () in
- try f x
- with e ->
- let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
-
-let purify_future f x = if is_over x then f x else purify f x
-let compute x = purify_future (compute ~pure:false) x
-let force ~pure x = purify_future (force ~pure) x
-let chain ~pure x f =
- let y = chain ~pure x f in
- if is_over x then ignore(force ~pure y);
+let chain x f =
+ let y = chain x f in
+ if is_over x then ignore(force y);
y
-let force x = force ~pure:false x
let join kx =
let v = force kx in
@@ -205,12 +169,11 @@ let join kx =
let sink kx = if is_val kx then ignore(join kx)
let split2 x =
- chain ~pure:true x (fun x -> fst x),
- chain ~pure:true x (fun x -> snd x)
+ chain x (fun x -> fst x), chain x (fun x -> snd x)
let map2 f x l =
CList.map_i (fun i y ->
- let xi = chain ~pure:true x (fun x ->
+ let xi = chain x (fun x ->
try List.nth x i
with Failure _ | Invalid_argument _ ->
CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in
@@ -226,6 +189,5 @@ let print f kx =
match !x with
| Delegated _ -> str "Delegated" ++ uid
| Closure _ -> str "Closure" ++ uid
- | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x)
- | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x)
+ | Val x -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x)
| Exn (e, _) -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e))
diff --git a/lib/future.mli b/lib/future.mli
index acfce51a07..853f81cea0 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -6,42 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* Futures: asynchronous computations with some purity enforcing
+(* Futures: asynchronous computations.
*
* A Future.computation is like a lazy_t but with some extra bells and whistles
- * to deal with imperative code and eventual delegation to a slave process.
+ * to deal with eventual delegation to a slave process.
*
- * Example of a simple scenario taken into account:
- *
- * let f = Future.from_here (number_of_constants (Global.env())) in
- * let g = Future.chain ~pure:false f (fun n ->
- * n = number_of_constants (Global.env())) in
- * ...
- * Lemmas.save_named ...;
- * ...
- * let b = Future.force g in
- *
- * The Future.computation f holds a (immediate, no lazy here) value.
- * We then chain to obtain g that (will) hold false if (when it will be
- * run) the global environment has a different number of constants, true
- * if nothing changed.
- * Before forcing g, we add to the global environment one more constant.
- * When finally we force g. Its value is going to be *true*.
- * This because Future.from_here stores in the computation not only the initial
- * value but the entire system state. When g is forced the state is restored,
- * hence Global.env() returns the environment that was actual when f was
- * created.
- * Last, forcing g is run protecting the system state, hence when g finishes,
- * the actual system state is restored.
- *
- * If you compare this with lazy_t, you see that the value returned is *false*,
- * that is counter intuitive and error prone.
- *
- * Still not all computations are impure and access/alter the system state.
- * This class can be optimized by using ~pure:true, but there is no way to
- * statically check if this flag is misused, hence use it with care.
- *
- * Other differences with lazy_t is that a future computation that produces
+ * One difference with lazy_t is that a future computation that produces
* and exception can be substituted for another computation of the same type.
* Moreover a future computation can be delegated to another execution entity
* that will be allowed to set the result. Finally future computations can
@@ -113,27 +83,17 @@ val is_exn : 'a computation -> bool
val peek_val : 'a computation -> 'a option
val uuid : 'a computation -> UUID.t
-(* [chain pure c f] chains computation [c] with [f].
- * [chain] forces immediately the new computation if the old one is_over (Exn or Val).
- * The [pure] parameter is tricky:
- * [pure]:
- * When pure is true, the returned computation will not keep a copy
- * of the global state.
- * [let c' = chain ~pure:true c f in let c'' = chain ~pure:false c' g in]
- * is invalid. It works if one forces [c''] since the whole computation
- * will be executed in one go. It will not work, and raise an anomaly, if
- * one forces c' and then c''.
- * [join c; chain ~pure:false c g] is invalid and fails at runtime.
- * [force c; chain ~pure:false c g] is correct.
- *)
-val chain : pure:bool ->
- 'a computation -> ('a -> 'b) -> 'b computation
+(* [chain c f] chains computation [c] with [f].
+ * [chain] is eager, that is to say, it won't suspend the new computation
+ * if the old one is_over (Exn or Val).
+*)
+val chain : 'a computation -> ('a -> 'b) -> 'b computation
(* Forcing a computation *)
val force : 'a computation -> 'a
val compute : 'a computation -> 'a value
-(* Final call, no more *inpure* chain allowed since the state is lost.
+(* Final call.
* Also the fix_exn function is lost, hence error reporting can be incomplete
* in a computation obtained by chaining on a joined future. *)
val join : 'a computation -> 'a
@@ -148,19 +108,8 @@ val map2 :
('a computation -> 'b -> 'c) ->
'a list computation -> 'b list -> 'c list
-(* Once set_freeze is called we can purify a computation *)
-val purify : ('a -> 'b) -> 'a -> 'b
-(* And also let a function alter the state but backtrack if it raises exn *)
-val transactify : ('a -> 'b) -> 'a -> 'b
-
(** Debug: print a computation given an inner printing function. *)
val print : ('a -> Pp.t) -> 'a computation -> Pp.t
-type freeze
-(* These functions are needed to get rid of side effects.
- Thy are set for the outermos layer of the system, since they have to
- deal with the whole system state. *)
-val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit
-
val customize_not_ready_msg : (string -> Pp.t) -> unit
val customize_not_here_msg : (string -> Pp.t) -> unit
diff --git a/lib/genarg.ml b/lib/genarg.ml
index b78fe40373..a3bfb405c8 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -11,7 +11,7 @@ open Util
module ArgT =
struct
- module DYN = Dyn.Make(struct end)
+ module DYN = Dyn.Make ()
module Map = DYN.Map
type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag
type any = Any : ('a, 'b, 'c) tag -> any
diff --git a/lib/minisys.ml b/lib/minisys.ml
index 706f0430c3..389b18ad4e 100644
--- a/lib/minisys.ml
+++ b/lib/minisys.ml
@@ -36,10 +36,15 @@ let skipped_dirnames = ref ["CVS"; "_darcs"]
let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
+(* Note: this test is possibly used for Coq module/file names but also for
+ OCaml filenames, whose syntax as of today is more restrictive for
+ module names (only initial letter then letter, digits, _ or quote),
+ but more permissive (though disadvised) for file names *)
+
let ok_dirname f =
not (f = "") && f.[0] != '.' &&
- not (List.mem f !skipped_dirnames) (*&&
- (match Unicode.ident_refutation f with None -> true | _ -> false)*)
+ not (List.mem f !skipped_dirnames) &&
+ match Unicode.ident_refutation f with None -> true | _ -> false
(* Check directory can be opened *)
@@ -55,10 +60,11 @@ let exists_dir dir =
let apply_subdir f path name =
(* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
(* as well as skipped files like CVS, ... *)
- if ok_dirname name then
+ let base = try Filename.chop_extension name with Invalid_argument _ -> name in
+ if ok_dirname base then
let path = if path = "." then name else path//name in
match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with
- | Unix.S_DIR -> f (FileDir (path,name))
+ | Unix.S_DIR when name = base -> f (FileDir (path,name))
| Unix.S_REG -> f (FileRegular name)
| _ -> ()
diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml
index 9ce348a0bd..d0ded4cb59 100644
--- a/lib/segmenttree.ml
+++ b/lib/segmenttree.ml
@@ -1,3 +1,11 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
(** This module is a very simple implementation of "segment trees".
A segment tree of type ['a t] represents a mapping from a union of
diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli
index 3258537b99..e274a6fdc8 100644
--- a/lib/segmenttree.mli
+++ b/lib/segmenttree.mli
@@ -1,3 +1,11 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
(** This module is a very simple implementation of "segment trees".
A segment tree of type ['a t] represents a mapping from a union of
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 0cf163e737..de31d87d0e 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -28,8 +28,6 @@ module type Control = sig
end
-module type Empty = sig end
-
module type MainLoopModel = sig
type async_chan
type condition
@@ -216,7 +214,7 @@ let rec wait p =
end
-module Sync(T : Empty) = struct
+module Sync () = struct
type process = {
cin : in_channel;
diff --git a/lib/spawn.mli b/lib/spawn.mli
index a131715e9d..fd2b92ae3e 100644
--- a/lib/spawn.mli
+++ b/lib/spawn.mli
@@ -34,8 +34,6 @@ module type Control = sig
end
(* Abstraction to work with both threads and main loop models *)
-module type Empty = sig end
-
module type MainLoopModel = sig
type async_chan
type condition
@@ -64,7 +62,7 @@ module Async(ML : MainLoopModel) : sig
end
(* spawn a process and read its output synchronously *)
-module Sync(T : Empty) : sig
+module Sync () : sig
type process
val spawn :
diff --git a/lib/store.ml b/lib/store.ml
index a1788f7da9..97a8fea085 100644
--- a/lib/store.ml
+++ b/lib/store.ml
@@ -14,10 +14,6 @@
stores, we might want something static to avoid troubles with
plugins order. *)
-module type T =
-sig
-end
-
module type S =
sig
type t
@@ -30,7 +26,7 @@ sig
val field : unit -> 'a field
end
-module Make (M : T) : S =
+module Make () : S =
struct
let next =
diff --git a/lib/store.mli b/lib/store.mli
index 8eab314ed7..5cc5bb8593 100644
--- a/lib/store.mli
+++ b/lib/store.mli
@@ -9,11 +9,6 @@
(*** This module implements an "untyped store", in this particular case we
see it as an extensible record whose fields are left unspecified. ***)
-module type T =
-sig
-(** FIXME: Waiting for first-class modules... *)
-end
-
module type S =
sig
type t
@@ -42,5 +37,5 @@ sig
end
-module Make (M : T) : S
+module Make () : S
(** Create a new store type. *)
diff --git a/lib/system.ml b/lib/system.ml
index 0b64b237da..4b5066ef41 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -54,6 +54,8 @@ let make_dir_table dir =
let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
+let trust_file_cache = ref true
+
let exists_in_dir_respecting_case dir bf =
let cache_dir dir =
let contents = make_dir_table dir in
@@ -62,10 +64,10 @@ let exists_in_dir_respecting_case dir bf =
let contents, fresh =
try
(* in batch mode, assume the directory content is still fresh *)
- StrMap.find dir !dirmap, !Flags.batch_mode
+ StrMap.find dir !dirmap, !trust_file_cache
with Not_found ->
(* in batch mode, we are not yet sure the directory exists *)
- if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true
+ if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true
else cache_dir dir, true in
StrSet.mem bf contents ||
not fresh &&
@@ -80,7 +82,7 @@ let file_exists_respecting_case path f =
let df = Filename.dirname f in
(String.equal df "." || aux df)
&& exists_in_dir_respecting_case (Filename.concat path df) bf
- in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f
+ in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f
let rec search paths test =
match paths with
diff --git a/lib/system.mli b/lib/system.mli
index 7281de97c9..aa964abebe 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -54,6 +54,12 @@ val where_in_path_rex :
val find_file_in_path :
?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
+val trust_file_cache : bool ref
+(** [trust_file_cache] indicates whether we trust the underlying
+ mapped file-system not to change along the execution of Coq. This
+ assumption greatly speds up file search, but it is often
+ inconvenient in interactive mode *)
+
val file_exists_respecting_case : string -> string -> bool
(** {6 I/O functions } *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:27:32 +0000