diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 28 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 7 | ||||
| -rw-r--r-- | stm/vio_checking.ml | 9 |
3 files changed, 26 insertions, 18 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 32c6c7d959..1641adbb70 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 () = @@ -3008,7 +3006,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let bname = VCS.mk_branch_name x in let opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) - | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | VernacInstance (_,_ , None, _) -> GuaranteesOpacity | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); let proof_mode = default_proof_mode () in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f40b3e901b..09f531ce13 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -160,11 +160,12 @@ let classify_vernac e = | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ | VernacDeclareReduction _ - | VernacDeclareClass _ | VernacDeclareInstances _ + | VernacExistingClass _ | VernacExistingInstance _ | VernacRegister _ | VernacNameSectionHypSet _ | VernacDeclareCustomEntry _ - | VernacComments _ -> VtSideff [], VtLater + | VernacComments _ + | VernacDeclareInstance _ -> VtSideff [], VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) @@ -214,6 +215,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 |