diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 26 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 | ||||
| -rw-r--r-- | stm/vio_checking.ml | 9 |
3 files changed, 22 insertions, 15 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 32c6c7d959..169d608d2d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -869,7 +869,6 @@ end = struct (* {{{ *) cur_id := id | { state = Error ie } -> - cur_id := id; Exninfo.iraise ie | _ -> @@ -2017,7 +2016,7 @@ end = struct (* {{{ *) find ~time:false ~batch:false ~fail:false e in let st = Vernacstate.freeze_interp_state ~marshallable:false in Vernacentries.with_fail st fail (fun () -> - (if time then System.with_time ~batch else (fun x -> x)) (fun () -> + (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in @@ -2832,17 +2831,9 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - match Stateid.get info with - | None -> - VCS.restore vcs; - VCS.print (); - anomaly(str"error with no safe_id attached:" ++ spc() ++ - CErrors.iprint_no_report (e, info) ++ str".") - | Some (safe_id, id) -> - stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); - VCS.restore vcs; - VCS.print (); - Exninfo.iraise (e, info) + VCS.restore vcs; + VCS.print (); + Exninfo.iraise (e, info) let snapshot_vio ~doc ldir long_f_dot_vo = let doc = finish ~doc in @@ -2993,7 +2984,14 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - let id = VCS.new_node ~id:newtip () in + if not (get_allow_nested_proofs ()) && in_proof then + "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." + |> Pp.str + |> (fun s -> (UserError (None, s), Exninfo.null)) + |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> Exninfo.iraise + else + let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f40b3e901b..454a4b66e7 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -214,6 +214,6 @@ let classify_vernac e = | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow - | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater) in static_control_classifier e diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 64f19e1fd9..69c1d9bd23 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -95,6 +95,7 @@ let schedule_vio_checking j fs = done; let pid, ret = Unix.wait () in if ret <> Unix.WEXITED 0 then rc := 1; + Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; exit !rc @@ -124,6 +125,7 @@ let schedule_vio_compilation j fs = | s :: rest -> s :: filter_argv b rest in let prog = Sys.argv.(0) in let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in + let all_jobs = !jobs in let make_job () = let f, t = List.hd !jobs in jobs := List.tl !jobs; @@ -137,8 +139,15 @@ let schedule_vio_compilation j fs = done; let pid, ret = Unix.wait () in if ret <> Unix.WEXITED 0 then rc := 1; + Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; + if !rc = 0 then begin + (* set the access and last modification time of all files to the same t + * not to confuse make into thinking that some of them are outdated *) + let t = Unix.gettimeofday () in + List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs; + end; exit !rc |