aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/library.ml12
-rw-r--r--library/library.mli1
-rw-r--r--tools/coqc.ml3
-rw-r--r--toplevel/coqtop.ml45
-rw-r--r--toplevel/stm.ml107
-rw-r--r--toplevel/stm.mli3
-rw-r--r--toplevel/toplevel.mllib1
-rw-r--r--toplevel/vernac.ml1
-rw-r--r--toplevel/vi_checking.ml61
-rw-r--r--toplevel/vi_checking.mli14
10 files changed, 209 insertions, 39 deletions
diff --git a/library/library.ml b/library/library.ml
index 8b390832f..1088bcb16 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -394,6 +394,18 @@ let intern_from_file f =
close_in ch;
library
+let load_library_todo f =
+ let paths = Loadpath.get_paths () in
+ let _, longf =
+ System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+ let f = longf^"i" in
+ let ch = System.with_magic_number_check raw_intern_library f in
+ let _ = System.skip_in_segment f ch in
+ let tasks, _, _ = System.marshal_in_segment f ch in
+ match tasks with
+ | Some a -> a, longf
+ | None -> errorlabstrm "load_library_todo" (str"not a .vi file")
+
let rec intern_library needed (dir, f) =
(* Look if in the current logical environment *)
try find_library dir, needed
diff --git a/library/library.mli b/library/library.mli
index 530209485..647138483 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -38,6 +38,7 @@ val start_library : string -> DirPath.t * string
(** {6 End the compilation of a library and save it to a ".vo" file } *)
val save_library_to : ?todo:'a -> DirPath.t -> string -> unit
+val load_library_todo : string -> 'a * string
(** {6 Interrogate the status of libraries } *)
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 3b01f90c4..378f493ad 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -126,7 +126,8 @@ let parse_args () =
| ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
|"-load-vernac-source"|"-l"|"-load-vernac-object"
|"-load-ml-source"|"-require"|"-load-ml-object"
- |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem ->
+ |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
+ |"-check-vi-tasks" as o) :: rem ->
begin
match rem with
| s :: rem' -> parse (cfiles,s::o::args) rem'
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ad3ce7879..f902206e2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -238,6 +238,33 @@ let get_host_port opt s =
| [host; port] -> Some (host, int_of_string port)
| _ -> prerr_endline ("Error: host:port expected after option "^opt); exit 1
+let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
+
+let vi_tasks = ref []
+
+let add_vi_task f =
+ set_batch_mode ();
+ Flags.make_silent true;
+ vi_tasks := f :: !vi_tasks
+
+let check_vi_tasks () = List.iter Vi_checking.check_vi (List.rev !vi_tasks)
+
+let vi_files = ref []
+let vi_files_j = ref 0
+
+let add_vi_file f =
+ set_batch_mode ();
+ Flags.make_silent true;
+ vi_files := f :: !vi_files
+let set_vi_checking_j j = vi_files_j := int_of_string j
+
+let is_not_dash_option = function
+ | Some f when String.length f > 0 && f.[0] <> '-' -> true
+ | _ -> false
+
+let schedule_vi_checking () =
+ Vi_checking.schedule_vi_checking !vi_files_j !vi_files
+
let parse_args arglist =
let args = ref arglist in
let extras = ref [] in
@@ -245,10 +272,14 @@ let parse_args arglist =
| [] -> List.rev !extras
| opt :: rem ->
args := rem;
- let next () = match rem with
+ let next () = match !args with
| x::rem -> args := rem; x
| [] -> error_missing_arg opt
in
+ let peek_next () = match !args with
+ | x::_ -> Some x
+ | [] -> None
+ in
begin match opt with
(* Complex options with many args *)
@@ -266,6 +297,16 @@ let parse_args arglist =
| d :: p :: rem -> set_rec_include d p; args := rem
| _ -> error_missing_arg opt
end
+
+ (* Options with two arg *)
+ |"-check-vi-tasks" ->
+ let tno = get_task_list (next ()) in
+ let tfile = next () in
+ add_vi_task (tno,tfile)
+ |"-schedule-vi-checking" ->
+ set_vi_checking_j (next ());
+ add_vi_file (next ());
+ while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
(* Options with one arg *)
|"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
@@ -396,6 +437,8 @@ let init arglist =
load_rcfile();
load_vernacular ();
compile_files ();
+ schedule_vi_checking ();
+ check_vi_tasks ();
outputstate ()
with any ->
flush_all();
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index f5cc9a856..bb531056f 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -571,12 +571,19 @@ end = struct (* {{{ *)
end
(* }}} *)
+let hints = ref Aux_file.empty_aux_file
+let set_compilation_hints h = hints := h
+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
+ ids
(* Slave processes (if initialized, otherwise local lazy evaluation) *)
module Slaves : sig
(* (eventually) remote calls *)
- val build_proof :
+ val build_proof : loc:Loc.t ->
exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t ->
name:string -> future_proof * cancel_switch
@@ -596,6 +603,8 @@ module Slaves : sig
type tasks
val dump : unit -> tasks
+ val check_task : tasks -> int -> unit
+ val info_tasks : tasks -> (string * float * int) list
end = struct (* {{{ *)
@@ -713,9 +722,10 @@ end = struct (* {{{ *)
let set_reach_known_state f = reach_known_state := f
type request =
- ReqBuildProof of (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * string
+ ReqBuildProof of
+ (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * string
- let name_of_request (ReqBuildProof (_,_,_,s)) = s
+ let name_of_request (ReqBuildProof (_,_,_,_,s)) = s
type response =
| RespBuiltProof of Entries.proof_output list
@@ -741,33 +751,37 @@ end = struct (* {{{ *)
type task =
| TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
(Entries.proof_output list Future.assignement -> unit) * cancel_switch
- * string
+ * Loc.t * string
let pr_task = function
- | TaskBuildProof(_,bop,eop,_,_,s) ->
+ | TaskBuildProof(_,bop,eop,_,_,_,s) ->
"TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^
","^s^")"
let request_of_task task =
match task with
- | TaskBuildProof (exn_info,bop,eop,_,_,s) ->
- ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,s)
+ | TaskBuildProof (exn_info,bop,eop,_,_,loc,s) ->
+ ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,s)
let cancel_switch_of_task = function
- | TaskBuildProof (_,_,_,_,c,_) -> c
+ | TaskBuildProof (_,_,_,_,c,_,_) -> c
- let build_proof_here_core eop () =
+ let build_proof_here_core loc eop () =
+ let wall_clock1 = Unix.gettimeofday () in
!reach_known_state ~cache:`No eop;
+ let wall_clock2 = Unix.gettimeofday () in
+ Aux_file.record_in_aux_at loc "proof_build_time"
+ (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Proof_global.return_proof ()
- let build_proof_here (id,valid) eop =
- Future.create (State.exn_on id ~valid) (build_proof_here_core eop)
+ let build_proof_here (id,valid) loc eop =
+ Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop)
let slave_respond msg =
match msg with
- | ReqBuildProof(exn_info,eop,vcs,_) ->
+ | ReqBuildProof(exn_info,eop,vcs,loc,_) ->
VCS.restore vcs;
VCS.print ();
let r = RespBuiltProof (
- let l = Future.force (build_proof_here exn_info eop) in
+ let l = Future.force (build_proof_here exn_info loc eop) in
List.iter (fun (_,se) -> Declareops.iter_side_effects (function
| Declarations.SEsubproof(_,
{ Declarations.const_body = Declarations.OpaqueDef f;
@@ -779,6 +793,30 @@ end = struct (* {{{ *)
VCS.print ();
r
+ let check_task l i =
+ match List.nth l i with
+ | ReqBuildProof ((id,valid),eop,vcs,loc,s) ->
+ Pp.msg_info (str"Checking "++str s);
+ VCS.restore vcs;
+ !reach_known_state ~cache:`No eop;
+ (* The original terminator, a hook, has not been saved in the .vi*)
+ Proof_global.set_terminator
+ (Lemmas.standard_proof_terminator [] (fun _ _ -> ()));
+ let proof = Proof_global.close_proof (fun x -> x) in
+ vernac_interp eop ~proof
+ { verbose = false; loc;
+ expr = (VernacEndProof (Proved (true,None))) }
+
+ let info_tasks l =
+ CList.map_i (fun i (ReqBuildProof(_,_,_,loc,s)) ->
+ let time1 =
+ try float_of_string (Aux_file.get !hints loc "proof_build_time")
+ with Not_found -> 0.0 in
+ let time2 =
+ try float_of_string (Aux_file.get !hints loc "proof_check_time")
+ with Not_found -> 0.0 in
+ s,max (time1 +. time2) 0.0001,i) 0 l
+
open Interface
exception MarshalError of string
@@ -833,23 +871,23 @@ end = struct (* {{{ *)
TQueue.wait_until_n_are_waiting_and_queue_empty
(SlavesPool.n_slaves ()) queue
- let build_proof ~exn_info:(id,valid as exn_info) ~start ~stop ~name =
+ let build_proof ~loc ~exn_info:(id,valid as exn_info) ~start ~stop ~name =
let cancel_switch = ref false in
if SlavesPool.is_empty () then
if !Flags.compilation_mode = Flags.BuildVi then begin
let force () : Entries.proof_output list Future.assignement =
- try `Val (build_proof_here_core stop ()) with e -> `Exn e in
+ 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
TQueue.push queue
- (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,name));
+ (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
f, cancel_switch
end else
- build_proof_here exn_info stop, cancel_switch
+ build_proof_here exn_info loc stop, cancel_switch
else
let f, assign = Future.create_delegate (State.exn_on id ~valid) in
Pp.feedback (Interface.InProgress 1);
TQueue.push queue
- (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,name));
+ (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
f, cancel_switch
exception RemoteException of std_ppcmds
@@ -882,13 +920,13 @@ end = struct (* {{{ *)
let rec loop () =
let response = unmarshal_response ic in
match task, response with
- | TaskBuildProof(_,_,_, assign,_,_), RespBuiltProof pl ->
+ | TaskBuildProof(_,_,_, assign,_,_,_), RespBuiltProof pl ->
assign (`Val pl);
(* We restart the slave, to avoid memory leaks. We could just
Pp.feedback (Interface.InProgress ~-1) *)
last_task := None;
raise KillRespawn
- | TaskBuildProof(_,_,_, assign,_,_), RespError (err_id,valid,e) ->
+ | TaskBuildProof(_,_,_, assign,_,_,_), RespError (err_id,valid,e) ->
let e = Stateid.add ~valid (RemoteException e) err_id in
assign (`Exn e);
(* We restart the slave, to avoid memory leaks. We could just
@@ -920,8 +958,8 @@ end = struct (* {{{ *)
msg_warning(strbrk("Marshalling error: "^s^". "^
"The system state could not be sent to the slave process. "^
"Falling back to local, lazy, evaluation."));
- let TaskBuildProof (exn_info, _, stop, assign,_,_) = task in
- assign(`Comp(build_proof_here exn_info stop));
+ let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+ assign(`Comp(build_proof_here exn_info loc stop));
Pp.feedback (Interface.InProgress ~-1)
| (Sys_error _ | Invalid_argument _ | End_of_file | KillRespawn) as e ->
raise e (* we pass the exception to the external handler *)
@@ -949,8 +987,8 @@ end = struct (* {{{ *)
(match !last_task with
| Some task ->
msg_warning(strbrk "Falling back to local, lazy, evaluation.");
- let TaskBuildProof (exn_info, _, stop, assign,_,_) = task in
- assign(`Comp(build_proof_here exn_info stop));
+ let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+ assign(`Comp(build_proof_here exn_info loc stop));
Pp.feedback (Interface.InProgress ~-1);
| None -> ());
close_in ic;
@@ -1055,14 +1093,6 @@ end = struct (* {{{ *)
end (* }}} *)
-let hints = ref Aux_file.empty_aux_file
-let set_compilation_hints h = hints := h
-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
- ids
-
(* Runs all transactions needed to reach a state *)
module Reach : sig
@@ -1181,17 +1211,17 @@ let known_state ?(redefine_qed=false) ~cache id =
| VtKeep, { VCS.kind = `Edit _ }, Some (ofp, cancel) ->
assert(redefine_qed = true);
VCS.create_cluster nodes ~tip:id;
- let fp, cancel =
- Slaves.build_proof ~exn_info:(id,eop) ~start ~stop:eop
+ 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
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 ~exn_info:(id,eop) ~start ~stop:eop
- ~name:(String.concat " " (List.map Id.to_string ids)) in
+ 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
qed.fproof <- Some (fp, cancel);
let proof =
Proof_global.close_future_proof ~feedback_id:id fp in
@@ -1459,6 +1489,8 @@ let join () =
type tasks = Slaves.tasks
let dump () = Slaves.dump ()
+let check_task tasks i = Slaves.check_task tasks i
+let info_tasks tasks = Slaves.info_tasks tasks
let merge_proof_branch qast keep brname =
let brinfo = VCS.get_branch brname in
@@ -1917,6 +1949,7 @@ let show_script ?proof () =
let indented_cmds = List.rev (indented_cmds) in
msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds))
with Proof_global.NoCurrentProof -> ()
+ | Vcs_aux.Expired -> ()
let () = Vernacentries.show_script := show_script
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 4949845b5..89efdc718 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -44,6 +44,9 @@ val join : unit -> unit
type tasks
val dump : unit -> tasks
+val check_task : tasks -> int -> unit
+val info_tasks : tasks -> (string * float * int) list
+
(* Id of the tip of the current branch *)
val get_current_state : unit -> Stateid.t
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 0ad82abd3..6f39725ff 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -23,4 +23,5 @@ Ide_slave
Usage
Coqloop
Coqinit
+Vi_checking
Coqtop
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 789f6bebb..d9c23c0ad 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -371,3 +371,4 @@ let compile verbosely f =
check_pending_proofs ();
let todo = Stm.dump () in
Library.save_library_to ~todo ldir long_f_dot_v
+
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
new file mode 100644
index 000000000..debb1e969
--- /dev/null
+++ b/toplevel/vi_checking.ml
@@ -0,0 +1,61 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+let check_vi (ts,f) =
+ Dumpglob.noglob ();
+ let tasks, long_f_dot_v = Library.load_library_todo f in
+ Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+ List.iter (Stm.check_task tasks) ts
+
+let schedule_vi_checking j fs =
+ let jobs = ref [] in
+ List.iter (fun f ->
+ let tasks, long_f_dot_v = Library.load_library_todo f in
+ Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+ let infos = Stm.info_tasks tasks in
+ jobs := List.map (fun (name,time,id) -> (f,id),name,time) infos @ !jobs)
+ fs;
+ let cmp_job (_,_,t1) (_,_,t2) = compare t2 t1 in
+ jobs := List.sort cmp_job !jobs;
+ let workers = Array.make j (0.0,[]) in
+ let cmp_worker (t1,_) (t2,_) = compare t1 t2 in
+ while !jobs <> [] do
+ Array.sort cmp_worker workers;
+ for i=0 to j-2 do
+ while !jobs <> [] && fst workers.(i) <= fst workers.(i+1) do
+ let ((f,id),_,t as job) = List.hd !jobs in
+ let rest = List.tl !jobs in
+ let tot, joblist = workers.(i) in
+ workers.(i) <- tot +. t, job::joblist;
+ jobs := rest
+ done
+ done;
+ done;
+ for i=0 to j-1 do
+ let tot, joblist = workers.(i) in
+ let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
+ workers.(i) <- tot, List.sort cmp_job joblist
+ done;
+ let pack = function
+ | [] -> []
+ | ((f,_),_,_) :: _ as l ->
+ let rec aux last acc = function
+ | [] -> [last,acc]
+ | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl
+ | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in
+ aux f [] l in
+ Array.iter
+ (fun (tot, joblist) -> if joblist <> [] then
+ let joblist = pack joblist in
+ Printf.printf "%s -check-vi-tasks %s & # eta %.2f\n"
+ Sys.argv.(0)
+ (String.concat " -check-vi-tasks "
+ (List.map (fun (f,tl) ->
+ let tl = List.map string_of_int tl in
+ String.concat "," tl ^ " " ^ f) joblist)) tot)
+ workers
diff --git a/toplevel/vi_checking.mli b/toplevel/vi_checking.mli
new file mode 100644
index 000000000..9866fdb97
--- /dev/null
+++ b/toplevel/vi_checking.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* [check_vi tasks file] checks the [tasks] stored in [file] *)
+val check_vi : int list * string -> unit
+
+(* [schedule_vi_checking j files] prints [j] command lines to
+ * be executed in parallel to check all tasks in [files] *)
+val schedule_vi_checking : int -> string list -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 00:51:15 +0000