diff options
| author | Enrico Tassi | 2014-02-25 11:05:28 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-02-26 14:53:08 +0100 |
| commit | 0278c2637ccab060fdfc49924bb6c3aa37aab961 (patch) | |
| tree | dd0888d2e50e2209cd0c1b9c454f490a68d60216 /toplevel/stm.ml | |
| parent | 8eae572c0bbc0a3f597f43a00c0c84875bcf2286 (diff) | |
STM: better messages when checking/finishing tasks
Diffstat (limited to 'toplevel/stm.ml')
| -rw-r--r-- | toplevel/stm.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 9a86d7ea0e..38355956cf 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -837,10 +837,11 @@ end = struct (* {{{ *) VCS.print (); r - let check_task_aux name l i = + let check_task_aux extra name l i = match List.nth l i with - | ReqBuildProof ((id,valid),eop,vcs,loc,_,s) as req -> - Pp.msg_info(str(Printf.sprintf "Checking task %d (%s) of %s" i s name)); + | ReqBuildProof ((id,valid),eop,vcs,loc,_,s) -> + Pp.msg_info( + str(Printf.sprintf "Checking task %d (%s%s) of %s" i s extra name)); VCS.restore vcs; try !reach_known_state ~cache:`No eop; @@ -851,7 +852,7 @@ end = struct (* {{{ *) vernac_interp eop ~proof { verbose = false; loc; expr = (VernacEndProof (Proved (true,None))) }; - Some (req,proof) + Some proof with e -> (try match Stateid.get e with | None -> @@ -878,9 +879,11 @@ end = struct (* {{{ *) str (Printexc.to_string e))); None let finish_task name u d p l i = - match check_task_aux name l i with + let bucket = + match List.nth l i with ReqBuildProof (_,_,_,_,bucket,_) -> bucket in + match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with | None -> exit 1 - | Some (ReqBuildProof ((id,valid),eop,vcs,loc,bucket,s), (po,pt)) -> + | Some (po,pt) -> let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in let con = Nametab.locate_constant @@ -894,15 +897,12 @@ end = struct (* {{{ *) let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in ignore(Future.join pr); ignore(Future.join uc); - Pp.msg_info(str(Printf.sprintf - "Assigning output of task %d (%s) of %s to bucket %d" - i s name bucket)); u.(bucket) <- uc; p.(bucket) <- pr | _ -> assert false let check_task name l i = - match check_task_aux name l i with + match check_task_aux "" name l i with | Some _ -> true | None -> false |