aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml1
-rw-r--r--ide/coq.mli1
-rw-r--r--ide/coqOps.ml29
-rw-r--r--lib/aux_file.ml26
-rw-r--r--lib/aux_file.mli1
-rw-r--r--lib/interface.mli11
-rw-r--r--lib/serialize.ml29
-rw-r--r--lib/serialize.mli1
-rw-r--r--toplevel/ide_slave.ml22
-rw-r--r--toplevel/stm.ml123
-rw-r--r--toplevel/stm.mli3
-rw-r--r--toplevel/vernac.ml4
-rw-r--r--toplevel/vi_checking.ml4
13 files changed, 130 insertions, 125 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 280f1df68..3dd2ce006 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -511,7 +511,6 @@ let eval_call ?(logger=default_logger) call handle k =
let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x)
let edit_at i = eval_call (Serialize.edit_at i)
let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x)
-let inloadpath s = eval_call (Serialize.inloadpath s)
let mkcases s = eval_call (Serialize.mkcases s)
let status ?logger force = eval_call ?logger (Serialize.status force)
let hints x = eval_call (Serialize.hints x)
diff --git a/ide/coq.mli b/ide/coq.mli
index 0b246b842..542cc4462 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -126,7 +126,6 @@ val goals : ?logger:Ideutils.logger ->
Interface.goals_sty -> Interface.goals_rty query
val evars : Interface.evars_sty -> Interface.evars_rty query
val hints : Interface.hints_sty -> Interface.hints_rty query
-val inloadpath : Interface.inloadpath_sty -> Interface.inloadpath_rty query
val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query
val search : Interface.search_sty -> Interface.search_rty query
val init : Interface.init_sty -> Interface.init_rty query
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index a43a7989a..18069c471 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -764,32 +764,7 @@ object(self)
let next = function
| Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return ()
| Good id -> initial_state <- id; Coq.return () in
- Coq.bind (Coq.init ()) next in
- let add_load_path = match get_filename () with
- | None -> Coq.return ()
- | Some f ->
- let dir = Filename.dirname f in
- let loadpath = Coq.inloadpath dir in
- let next = function
- | Fail (_, _, s) ->
- messages#set
- ("Could not determine lodpath, this might lead to problems:\n"^s);
- Coq.return ()
- | Good true -> Coq.return ()
- | Good false ->
- let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
- let cmd = Coq.add ((cmd,hidden_edit_id ()),(Stateid.initial,false)) in
- let next = function
- | Fail (_, l, str) ->
- messages#set ("Couln't add loadpath:\n"^str);
- Coq.return ()
- | Good (id, _) ->
- initial_state <- id; Coq.return ()
- in
- Coq.bind cmd next
- in
- Coq.bind loadpath next
- in
- Coq.seq get_initial_state (Coq.seq add_load_path Coq.PrintOpt.enforce)
+ Coq.bind (Coq.init (get_filename ())) next in
+ Coq.seq get_initial_state Coq.PrintOpt.enforce
end
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index 5a3d29746..80ac14f7d 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -20,10 +20,16 @@ let oc = ref None
let aux_file_name_for vfile =
dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux"
+let mk_absolute vfile =
+ let vfile = CUnix.remove_path_dot vfile in
+ if Filename.is_relative vfile then CUnix.correct_path vfile (Sys.getcwd ())
+ else vfile
+
let start_aux_file_for vfile =
+ let vfile = mk_absolute vfile in
oc := Some (open_out (aux_file_name_for vfile));
Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n"
- version (Digest.to_hex (Digest.file vfile)) (CUnix.strip_path vfile)
+ version (Digest.to_hex (Digest.file vfile)) vfile
let stop_aux_file () =
close_out (Option.get !oc);
@@ -52,33 +58,35 @@ let record_in_aux_set_at loc = current_loc := loc
let record_in_aux key v = record_in_aux_at !current_loc key v
-exception Outdated
+let set h loc k v =
+ let m = try H.find loc h with Not_found -> M.empty in
+ H.add loc (M.add k v m) h
let load_aux_file_for vfile =
+ let vfile = mk_absolute vfile in
let ret3 x y z = x, y, z in
let ret4 x y z t = x, y, z, t in
let h = ref empty_aux_file in
- let add loc k v =
- let m = try H.find loc !h with Not_found -> M.empty in
- h := H.add loc (M.add k v m) !h in
+ let add loc k v = h := set !h loc k v in
let aux_fname = aux_file_name_for vfile in
try
let ic = open_in aux_fname in
let ver, hash, fname = Scanf.fscanf ic "COQAUX%d %s %s\n" ret3 in
if ver <> version then raise (Failure "aux file version mismatch");
- if fname <> CUnix.strip_path vfile then
+ if fname <> vfile then
raise (Failure "aux file name mismatch");
- if Digest.to_hex (Digest.file vfile) <> hash then raise Outdated;
+ let only_dummyloc = Digest.to_hex (Digest.file vfile) <> hash in
while true do
let i, j, k, v = Scanf.fscanf ic "%d %d %s %S\n" ret4 in
- add (i,j) k v;
+ if not only_dummyloc || (i = 0 && j = 0) then add (i,j) k v;
done;
raise End_of_file
with
| End_of_file -> !h
- | Outdated -> empty_aux_file
| Sys_error s | Scanf.Scan_failure s
| Failure s | Invalid_argument s ->
Flags.if_verbose
Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
empty_aux_file
+
+let set h loc k v = set h (Loc.unloc loc) k v
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index b24515c99..f31b23408 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -11,6 +11,7 @@ type aux_file
val load_aux_file_for : string -> aux_file
val get : aux_file -> Loc.t -> string -> string
val empty_aux_file : aux_file
+val set : aux_file -> Loc.t -> string -> string -> aux_file
val start_aux_file_for : string -> unit
val stop_aux_file : unit -> unit
diff --git a/lib/interface.mli b/lib/interface.mli
index a089eb574..8af26196c 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -212,10 +212,6 @@ type get_options_rty = (option_name * option_state) list
type set_options_sty = (option_name * option_value) list
type set_options_rty = unit
-(** Is a directory part of Coq's loadpath ? *)
-type inloadpath_sty = string
-type inloadpath_rty = bool
-
(** Create a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
followed by enough pattern variables. *)
@@ -226,8 +222,10 @@ type mkcases_rty = string list list
type quit_sty = unit
type quit_rty = unit
-(* Initialize, and return the initial state id *)
-type init_sty = unit
+(* Initialize, and return the initial state id. The argument is the filename.
+ * If its directory is not in dirpath, it adds it. It also loads
+ * compilation hints for the filename. *)
+type init_sty = string option
type init_rty = state_id
type about_sty = unit
@@ -256,7 +254,6 @@ type handler = {
search : search_sty -> search_rty;
get_options : get_options_sty -> get_options_rty;
set_options : set_options_sty -> set_options_rty;
- inloadpath : inloadpath_sty -> inloadpath_rty;
mkcases : mkcases_sty -> mkcases_rty;
about : about_sty -> about_rty;
stop_worker : stop_worker_sty -> stop_worker_rty;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 386ab8e45..d91f736fd 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -10,7 +10,7 @@
(** WARNING: TO BE UPDATED WHEN MODIFIED! *)
-let protocol_version = "20130918"
+let protocol_version = "20140312"
(** * Interface of calls to Coq by CoqIde *)
@@ -617,11 +617,10 @@ let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t)
let get_options_sty_t : get_options_sty val_t = unit_t
let set_options_sty_t : set_options_sty val_t =
list_t (pair_t (list_t string_t) option_value_t)
-let inloadpath_sty_t : inloadpath_sty val_t = string_t
let mkcases_sty_t : mkcases_sty val_t = string_t
let quit_sty_t : quit_sty val_t = unit_t
let about_sty_t : about_sty val_t = unit_t
-let init_sty_t : init_sty val_t = unit_t
+let init_sty_t : init_sty val_t = option_t string_t
let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
let stop_worker_sty_t : stop_worker_sty val_t = int_t
@@ -640,7 +639,6 @@ let search_rty_t : search_rty val_t = list_t (coq_object_t string_t)
let get_options_rty_t : get_options_rty val_t =
list_t (pair_t (list_t string_t) option_state_t)
let set_options_rty_t : set_options_rty val_t = unit_t
-let inloadpath_rty_t : inloadpath_rty val_t = bool_t
let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t)
let quit_rty_t : quit_rty val_t = unit_t
let about_rty_t : about_rty val_t = coq_info_t
@@ -660,7 +658,6 @@ let calls = [|
"Search", ($)search_sty_t, ($)search_rty_t;
"GetOptions", ($)get_options_sty_t, ($)get_options_rty_t;
"SetOptions", ($)set_options_sty_t, ($)set_options_rty_t;
- "InLoadPath", ($)inloadpath_sty_t, ($)inloadpath_rty_t;
"MkCases", ($)mkcases_sty_t, ($)mkcases_rty_t;
"Quit", ($)quit_sty_t, ($)quit_rty_t;
"About", ($)about_sty_t, ($)about_rty_t;
@@ -680,7 +677,6 @@ type 'a call =
| Search of search_sty
| GetOptions of get_options_sty
| SetOptions of set_options_sty
- | InLoadPath of inloadpath_sty
| MkCases of mkcases_sty
| Quit of quit_sty
| About of about_sty
@@ -700,13 +696,12 @@ let id_of_call = function
| Search _ -> 7
| GetOptions _ -> 8
| SetOptions _ -> 9
- | InLoadPath _ -> 10
- | MkCases _ -> 11
- | Quit _ -> 12
- | About _ -> 13
- | Init _ -> 14
- | Interp _ -> 15
- | StopWorker _ -> 16
+ | MkCases _ -> 10
+ | Quit _ -> 11
+ | About _ -> 12
+ | Init _ -> 13
+ | Interp _ -> 14
+ | StopWorker _ -> 15
let str_of_call c = pi1 calls.(id_of_call c)
@@ -722,7 +717,6 @@ let hints x : hints_rty call = Hints x
let status x : status_rty call = Status x
let get_options x : get_options_rty call = GetOptions x
let set_options x : set_options_rty call = SetOptions x
-let inloadpath x : inloadpath_rty call = InLoadPath x
let mkcases x : mkcases_rty call = MkCases x
let search x : search_rty call = Search x
let quit x : quit_rty call = Quit x
@@ -744,7 +738,6 @@ let abstract_eval_call handler (c : 'a call) : 'a value =
| Search x -> mkGood (handler.search x)
| GetOptions x -> mkGood (handler.get_options x)
| SetOptions x -> mkGood (handler.set_options x)
- | InLoadPath x -> mkGood (handler.inloadpath x)
| MkCases x -> mkGood (handler.mkcases x)
| Quit x -> mkGood (handler.quit x)
| About x -> mkGood (handler.about x)
@@ -766,7 +759,6 @@ let of_answer (q : 'a call) (v : 'a value) : xml = match q with
| Search _ -> of_value (of_value_type search_rty_t ) (Obj.magic v)
| GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v)
| SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v)
- | InLoadPath _ -> of_value (of_value_type inloadpath_rty_t ) (Obj.magic v)
| MkCases _ -> of_value (of_value_type mkcases_rty_t ) (Obj.magic v)
| Quit _ -> of_value (of_value_type quit_rty_t ) (Obj.magic v)
| About _ -> of_value (of_value_type about_rty_t ) (Obj.magic v)
@@ -785,7 +777,6 @@ let to_answer (q : 'a call) (x : xml) : 'a value = match q with
| Search _ -> Obj.magic (to_value (to_value_type search_rty_t ) x)
| GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x)
| SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x)
- | InLoadPath _ -> Obj.magic (to_value (to_value_type inloadpath_rty_t ) x)
| MkCases _ -> Obj.magic (to_value (to_value_type mkcases_rty_t ) x)
| Quit _ -> Obj.magic (to_value (to_value_type quit_rty_t ) x)
| About _ -> Obj.magic (to_value (to_value_type about_rty_t ) x)
@@ -806,7 +797,6 @@ let of_call (q : 'a call) : xml =
| Search x -> mkCall (of_value_type search_sty_t x)
| GetOptions x -> mkCall (of_value_type get_options_sty_t x)
| SetOptions x -> mkCall (of_value_type set_options_sty_t x)
- | InLoadPath x -> mkCall (of_value_type inloadpath_sty_t x)
| MkCases x -> mkCall (of_value_type mkcases_sty_t x)
| Quit x -> mkCall (of_value_type quit_sty_t x)
| About x -> mkCall (of_value_type about_sty_t x)
@@ -828,7 +818,6 @@ let to_call : xml -> unknown call =
| "Search" -> Search (mkCallArg search_sty_t a)
| "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a)
| "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a)
- | "InLoadPath" -> InLoadPath (mkCallArg inloadpath_sty_t a)
| "MkCases" -> MkCases (mkCallArg mkcases_sty_t a)
| "Quit" -> Quit (mkCallArg quit_sty_t a)
| "About" -> About (mkCallArg about_sty_t a)
@@ -864,7 +853,6 @@ let pr_full_value call value = match call with
| Search _ -> pr_value_gen (print search_rty_t ) (Obj.magic value)
| GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value)
| SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value)
- | InLoadPath _ -> pr_value_gen (print inloadpath_rty_t ) (Obj.magic value)
| MkCases _ -> pr_value_gen (print mkcases_rty_t ) (Obj.magic value)
| Quit _ -> pr_value_gen (print quit_rty_t ) (Obj.magic value)
| About _ -> pr_value_gen (print about_rty_t ) (Obj.magic value)
@@ -882,7 +870,6 @@ let pr_call call = match call with
| Search x -> str_of_call call ^ " " ^ print search_sty_t x
| GetOptions x -> str_of_call call ^ " " ^ print get_options_sty_t x
| SetOptions x -> str_of_call call ^ " " ^ print set_options_sty_t x
- | InLoadPath x -> str_of_call call ^ " " ^ print inloadpath_sty_t x
| MkCases x -> str_of_call call ^ " " ^ print mkcases_sty_t x
| Quit x -> str_of_call call ^ " " ^ print quit_sty_t x
| About x -> str_of_call call ^ " " ^ print about_sty_t x
diff --git a/lib/serialize.mli b/lib/serialize.mli
index db92dc9ea..b8bb1a33a 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -21,7 +21,6 @@ val query : query_sty -> query_rty call
val goals : goals_sty -> goals_rty call
val hints : hints_sty -> hints_rty call
val status : status_sty -> status_rty call
-val inloadpath : inloadpath_sty -> inloadpath_rty call
val mkcases : mkcases_sty -> mkcases_rty call
val evars : evars_sty -> evars_rty call
val search : search_sty -> search_rty call
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 1b97a69ba..8ea5de365 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -233,9 +233,6 @@ let hints () =
(** Other API calls *)
-let inloadpath dir =
- Loadpath.is_in_load_paths (CUnix.physical_path_of_string dir)
-
let status force =
(** We remove the initial part of the current [DirPath.t]
(usually Top in an interactive session, cf "coqtop -top"),
@@ -301,9 +298,23 @@ let handle_exn e =
let init =
let initialized = ref false in
- fun () ->
+ fun file ->
if !initialized then anomaly (str "Already initialized")
- else (initialized := true; Stm.get_current_state ())
+ else begin
+ initialized := true;
+ match file with
+ | None -> Stm.get_current_state ()
+ | Some file ->
+ let dir = Filename.dirname file in
+ let open Loadpath in let open CUnix in
+ let initial_id, _ =
+ if not (is_in_load_paths (physical_path_of_string dir)) then
+ Stm.add false ~ontop:(Stm.get_current_state ())
+ 0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
+ else Stm.get_current_state (), `NewTip in
+ Stm.set_compilation_hints file;
+ initial_id
+ end
(* Retrocompatibility stuff *)
let interp ((_raw, verbose), s) =
@@ -344,7 +355,6 @@ let eval_call xml_oc log c =
Interface.hints = interruptible hints;
Interface.status = interruptible status;
Interface.search = interruptible search;
- Interface.inloadpath = interruptible inloadpath;
Interface.get_options = interruptible get_options;
Interface.set_options = interruptible set_options;
Interface.mkcases = interruptible Vernacentries.make_cases;
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 9cb5e9511..c61258655 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -502,8 +502,8 @@ module State : sig
val install_cached : Stateid.t -> unit
val is_cached : Stateid.t -> bool
- val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn
+ val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn
(* to send states across worker/master *)
type frozen_state
val get_cached : Stateid.t -> frozen_state
@@ -595,13 +595,18 @@ end
(* }}} *)
let hints = ref Aux_file.empty_aux_file
-let set_compilation_hints h = hints := h
+let set_compilation_hints file =
+ hints := Aux_file.load_aux_file_for file
let get_hint_ctx loc =
let s = Aux_file.get !hints loc "context_used" in
let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
let ids = List.map (fun id -> Loc.ghost, id) ids in
SsExpr (SsSet ids)
+let get_hint_bp_time proof_name =
+ try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
+ with Not_found -> 1.0
+
module Worker = Spawn.Sync(struct
let add_timeout ~sec f =
ignore(Thread.create (fun () ->
@@ -612,6 +617,14 @@ module Worker = Spawn.Sync(struct
())
end)
+let record_pb_time proof_name loc time =
+ let proof_build_time = Printf.sprintf "%.3f" time in
+ Aux_file.record_in_aux_at loc "proof_build_time" proof_build_time;
+ if proof_name <> "" then begin
+ Aux_file.record_in_aux_at Loc.ghost proof_name proof_build_time;
+ hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
+ end
+
(* Slave processes (if initialized, otherwise local lazy evaluation) *)
module Slaves : sig
@@ -773,7 +786,7 @@ end = struct (* {{{ *)
let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s
type response =
- | RespBuiltProof of Entries.proof_output list
+ | RespBuiltProof of Entries.proof_output list * float
| RespError of (* err, safe, msg, safe_state *)
Stateid.t * Stateid.t * std_ppcmds * State.frozen_state option
| RespFeedback of Interface.feedback
@@ -825,7 +838,8 @@ end = struct (* {{{ *)
| ReqBuildProof(exn_info,eop,vcs,loc,_,_) ->
VCS.restore vcs;
VCS.print ();
- let r = RespBuiltProof (
+ let rc, time =
+ let wall_clock = Unix.gettimeofday () in
let l = Future.force (build_proof_here exn_info loc eop) in
List.iter (fun (_,se) -> Declareops.iter_side_effects (function
| Declarations.SEsubproof(_,
@@ -833,9 +847,9 @@ end = struct (* {{{ *)
Opaqueproof.join_opaque f
| _ -> ())
se) l;
- l) in
+ l, Unix.gettimeofday () -. wall_clock in
VCS.print ();
- r
+ RespBuiltProof(rc,time)
let check_task_aux extra name l i =
match List.nth l i with
@@ -974,8 +988,8 @@ end = struct (* {{{ *)
try `Val (build_proof_here_core loc stop ()) with e -> `Exn e in
let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
let uuid = Future.uuid f in
- TQueue.push queue
- (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
+ TQueue.push queue (TaskBuildProof
+ (exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
f, cancel_switch
end else
build_proof_here exn_info loc stop, cancel_switch
@@ -983,8 +997,8 @@ end = struct (* {{{ *)
let f, assign = Future.create_delegate (State.exn_on id ~valid) in
let uuid = Future.uuid f in
Pp.feedback (Interface.InProgress 1);
- TQueue.push queue
- (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
+ TQueue.push queue (TaskBuildProof
+ (exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
f, cancel_switch
exception RemoteException of std_ppcmds
@@ -1028,13 +1042,16 @@ end = struct (* {{{ *)
let rec loop () =
let response = unmarshal_response ic in
match task, response with
- | TaskBuildProof(_,_,_, assign,_,_,_,_), RespBuiltProof pl ->
+ | TaskBuildProof(_,_,_, assign,_,loc,_,s),
+ RespBuiltProof(pl, time)->
assign (`Val pl);
(* We restart the slave, to avoid memory leaks. We could just
Pp.feedback (Interface.InProgress ~-1) *)
+ record_pb_time s loc time;
last_task := None;
raise KillRespawn
- | TaskBuildProof(_,_,_, assign,_,_,_,_),RespError(err_id,valid,e,s) ->
+ | TaskBuildProof(_,_,_, assign,_,_,_,_),
+ RespError(err_id,valid,e,s) ->
let e = Stateid.add ~valid (RemoteException e) err_id in
assign (`Exn e);
Option.iter (State.assign valid) s;
@@ -1216,15 +1233,19 @@ end = struct (* {{{ *)
let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
-let delegate_policy_check () =
+let delegate_policy_check time =
if interactive () = `Yes then
- !Flags.async_proofs_mode = Flags.APonParallel 0 ||
- !Flags.async_proofs_mode = Flags.APonLazy
+ (!Flags.async_proofs_mode = Flags.APonParallel 0 ||
+ !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0
else if !Flags.compilation_mode = Flags.BuildVi then true
else !Flags.async_proofs_mode <> Flags.APoff
let collect_proof cur hd brkind id =
prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
+ let no_name = "" in
+ let name = function
+ | [] -> no_name
+ | id :: _ -> Id.to_string id in
let loc = (snd cur).loc in
let is_defined = function
| _, { expr = VernacEndProof (Proved (false,_)) } -> true
@@ -1233,40 +1254,54 @@ let collect_proof cur hd brkind id =
let view = VCS.visit id in
match last, view.step with
| _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
- | _, `Alias _ -> `Sync `Alias
- | _, `Fork(_,_,_,_::_::_)-> `Sync `MutualProofs
+ | _, `Alias _ -> `Sync (no_name,`Alias)
+ | _, `Fork(_,_,_,_::_::_)-> `Sync (no_name,`MutualProofs)
| _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) ->
- `Sync `Doesn'tGuaranteeOpacity
+ `Sync (no_name,`Doesn'tGuaranteeOpacity)
| Some (parent, ({ expr = VernacProof(_,Some _)} as v)),
`Fork (_, hd', GuaranteesOpacity, ids) ->
+ let name = name ids in
+ let time = get_hint_bp_time name in
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
- if delegate_policy_check () then `ASync (parent,Some v,accn,ids)
- else `Sync `Policy
+ if delegate_policy_check time
+ then `ASync (parent,Some v,accn,name)
+ else `Sync (name,`Policy)
| Some (parent, ({ expr = VernacProof(t,None)} as v)),
`Fork (_, hd', GuaranteesOpacity, ids) when
not (State.is_cached parent) &&
!Flags.compilation_mode = Flags.BuildVi ->
(try
- let hint = get_hint_ctx loc in
+ let name = name ids in
+ let hint, time = get_hint_ctx loc, get_hint_bp_time name in
assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
v.expr <- VernacProof(t, Some hint);
- if delegate_policy_check () then `ASync (parent,Some v,accn,ids)
- else `Sync `Policy
- with Not_found -> `Sync `NoHint)
+ if delegate_policy_check time
+ then `ASync (parent,Some v,accn,name)
+ else `Sync (name,`Policy)
+ with Not_found -> `Sync (no_name,`NoHint))
| Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
- if delegate_policy_check () then `MaybeASync (parent, accn, ids)
- else `Sync `Policy
- | _, `Sideff _ -> `Sync `NestedProof
- | _ -> `Sync `Unknown in
+ let name = name ids in
+ let time = get_hint_bp_time name in
+ if delegate_policy_check time
+ then `MaybeASync (parent, accn, name)
+ else `Sync (name,`Policy)
+ | _, `Sideff _ -> `Sync (no_name,`NestedProof)
+ | _ -> `Sync (no_name,`Unknown) in
match cur, (VCS.visit id).step, brkind with
|( parent, { expr = VernacExactProof _ }), `Fork _, _ ->
- `Sync `Immediate
+ `Sync (no_name,`Immediate)
| _, _, { VCS.kind = `Edit _ } -> collect (Some cur) [] id
| _ ->
- if State.is_cached id then `Sync `AlreadyEvaluated
- else if is_defined cur then `Sync `Transparent
- else collect (Some cur) [] id
+ if is_defined cur then `Sync (no_name,`Transparent)
+ else
+ let rc = collect (Some cur) [] id in
+ if not (State.is_cached id) then rc
+ else (* we already have the proof, no gain in delaying *)
+ match rc with
+ | `Sync(name,_) -> `Sync (name,`AlreadyEvaluated)
+ | `MaybeASync(_,_,name) -> `Sync (name,`AlreadyEvaluated)
+ | `ASync(_,_,_,name) -> `Sync (name,`AlreadyEvaluated)
let string_of_reason = function
| `Transparent -> "Transparent"
@@ -1318,7 +1353,7 @@ let known_state ?(redefine_qed=false) ~cache id =
), `Yes
| `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
let rec aux = function
- | `ASync (start, proof_using_ast, nodes,ids) -> (fun () ->
+ | `ASync (start, proof_using_ast, nodes, name) -> (fun () ->
prerr_endline ("Asynchronous " ^ Stateid.to_string id);
VCS.create_cluster nodes ~tip:id;
begin match keep, brinfo, qed.fproof with
@@ -1327,16 +1362,14 @@ let known_state ?(redefine_qed=false) ~cache id =
assert(redefine_qed = true);
VCS.create_cluster nodes ~tip:id;
let fp, cancel = Slaves.build_proof
- ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop
- ~name:(String.concat " " (List.map Id.to_string ids)) in
+ ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in
Future.replace ofp fp;
qed.fproof <- Some (fp, cancel)
| VtKeep, { VCS.kind = `Proof _ }, Some _ -> assert false
| VtKeep, { VCS.kind = `Proof _ }, None ->
reach ~cache:`Shallow start;
let fp, cancel = Slaves.build_proof
- ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop
- ~name:(String.concat " " (List.map Id.to_string ids)) in
+ ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in
qed.fproof <- Some (fp, cancel);
let proof =
Proof_global.close_future_proof ~feedback_id:id fp in
@@ -1351,17 +1384,16 @@ let known_state ?(redefine_qed=false) ~cache id =
end;
Proof_global.discard_all ()
), if redefine_qed then `No else `Yes
- | `Sync `Immediate -> (fun () ->
+ | `Sync (name, `Immediate) -> (fun () ->
assert (Stateid.equal view.next eop);
reach eop; vernac_interp id x; Proof_global.discard_all ()
), `Yes
- | `Sync reason -> (fun () ->
+ | `Sync (name, reason) -> (fun () ->
prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^
string_of_reason reason);
reach eop;
let wall_clock = Unix.gettimeofday () in
- Aux_file.record_in_aux_at x.loc "proof_build_time"
- (Printf.sprintf "%.3f" (wall_clock -. !wall_clock_last_fork));
+ record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork);
begin match keep with
| VtKeep ->
let proof =
@@ -1378,16 +1410,13 @@ let known_state ?(redefine_qed=false) ~cache id =
end;
Proof_global.discard_all ()
), `Yes
- | `MaybeASync (start, nodes, ids) -> (fun () ->
+ | `MaybeASync (start, nodes, name) -> (fun () ->
prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id);
reach ~cache:`Shallow start;
(* no sections *)
if List.is_empty (Environ.named_context (Global.env ()))
- (* && Safe_typing.is_curmod_library (Global.safe_env ()) *)
- then
- fst (aux (`ASync (start, None, nodes,ids))) ()
- else
- fst (aux (`Sync `Unknown)) ()
+ then fst (aux (`ASync (start, None, nodes, name))) ()
+ else fst (aux (`Sync (name, `Unknown))) ()
), if redefine_qed then `No else `Yes
in
aux (collect_proof (view.next, x) brname brinfo eop)
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 1eba274ab..cd9245895 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -60,7 +60,8 @@ val init : unit -> unit
val slave_main_loop : unit -> unit
val slave_init_stdout : unit -> unit
-val set_compilation_hints : Aux_file.aux_file -> unit
+(* Filename *)
+val set_compilation_hints : string -> unit
(** read-eval-print loop compatible interface ****************************** **)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 11cb726c7..27509fcc0 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -336,7 +336,7 @@ let compile verbosely f =
| BuildVi ->
let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
Dumpglob.noglob ();
- Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+ Stm.set_compilation_hints long_f_dot_v;
let _ = load_vernac verbosely long_f_dot_v in
Stm.finish ();
check_pending_proofs ();
@@ -347,7 +347,7 @@ let compile verbosely f =
Dumpglob.noglob ();
let f = if check_suffix f ".vi" then chop_extension f else f in
let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
- Stm.set_compilation_hints (Aux_file.load_aux_file_for lfdv);
+ Stm.set_compilation_hints lfdv;
let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
Library.save_library_raw lfdv lib univs proofs
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
index 37f4266d0..cb6e60136 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -11,7 +11,7 @@ open Util
let check_vi (ts,f) =
Dumpglob.noglob ();
let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
- Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+ Stm.set_compilation_hints long_f_dot_v;
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
module Worker = Spawn.Sync(struct
@@ -39,7 +39,7 @@ let schedule_vi_checking j fs =
if Filename.check_suffix f ".vi" then Filename.chop_extension f
else f in
let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
- Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+ Stm.set_compilation_hints long_f_dot_v;
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
if infos <> [] then jobs := (f, eta, infos) :: !jobs)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 05:05:53 +0000