From 85e5450775fd8cfaefa8962c9907941aa8154274 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Dec 2013 11:23:31 +0100 Subject: coqtop: -check-vi-tasks and -schedule-vi-checking The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2, in this precise order, stored in a.vi. The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi and .{a,b,c}.aux and spits 4 command lines to check all the tasks in {a,b,c}.vi trying to equally partition the job between the 4 workers, that can indeed be run in parallel. The aux file contains the time that it took to check the proofs stored in the .vi files last time the file was fully checked. This user interface is still very rough, it should probably run the workers instead of just printing their command line. --- library/library.ml | 12 ++++++ library/library.mli | 1 + tools/coqc.ml | 3 +- toplevel/coqtop.ml | 45 +++++++++++++++++++- toplevel/stm.ml | 107 +++++++++++++++++++++++++++++++---------------- toplevel/stm.mli | 3 ++ toplevel/toplevel.mllib | 1 + toplevel/vernac.ml | 1 + toplevel/vi_checking.ml | 61 +++++++++++++++++++++++++++ toplevel/vi_checking.mli | 14 +++++++ 10 files changed, 209 insertions(+), 39 deletions(-) create mode 100644 toplevel/vi_checking.ml create mode 100644 toplevel/vi_checking.mli 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 *) +(* + 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 *) +(* 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 -- cgit v1.2.3