diff options
-rw-r--r-- | library/library.ml | 12 | ||||
-rw-r--r-- | library/library.mli | 1 | ||||
-rw-r--r-- | tools/coqc.ml | 3 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 45 | ||||
-rw-r--r-- | toplevel/stm.ml | 107 | ||||
-rw-r--r-- | toplevel/stm.mli | 3 | ||||
-rw-r--r-- | toplevel/toplevel.mllib | 1 | ||||
-rw-r--r-- | toplevel/vernac.ml | 1 | ||||
-rw-r--r-- | toplevel/vi_checking.ml | 61 | ||||
-rw-r--r-- | toplevel/vi_checking.mli | 14 |
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 |