diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 73 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 5 |
2 files changed, 54 insertions, 24 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 70e242bb54..d9ecc8bcce 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -8,7 +8,8 @@ let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let prerr_endline s = if false then begin pr_err s end else () +let prerr_debug s = if !Flags.debug then begin pr_err s end else () open Vernacexpr open Errors @@ -1601,10 +1602,11 @@ let pstate = summary_pstate let async_policy () = let open Flags in - if interactive () = `Yes then - (async_proofs_is_master () || !async_proofs_mode = Flags.APonLazy) + if is_universe_polymorphism () then false + else if interactive () = `Yes then + (async_proofs_is_master () || !async_proofs_mode = APonLazy) else - (!compilation_mode = Flags.BuildVio || !async_proofs_mode <> Flags.APoff) + (!compilation_mode = BuildVio || !async_proofs_mode <> APoff) let delegate name = let time = get_hint_bp_time name in @@ -1632,12 +1634,17 @@ let collect_proof keep cur hd brkind id = let has_proof_no_using = function | Some (_, { expr = VernacProof(_,None) }) -> true | _ -> false in + let may_pierce_opaque = function + | { expr = VernacPrint (PrintName _) } -> true + | _ -> false in let parent = function Some (p, _) -> p | None -> assert false in let rec collect last accn id = let view = VCS.visit id in match view.step with + | (`Sideff (`Ast(x,_)) | `Cmd { cast = x }) + when may_pierce_opaque x -> `Sync(no_name,None,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next - | `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next + | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) | `Alias _ -> `Sync (no_name,None,`Alias) | `Fork((_,_,_,_::_::_), _) -> @@ -1657,7 +1664,9 @@ let collect_proof keep cur hd brkind id = let t, v = proof_no_using last in v.expr <- VernacProof(t, Some hint); `ASync (parent last,proof_using_ast last,accn,name,delegate name) - with Not_found -> `Sync (no_name,None,`NoHint)) + with Not_found -> + let name = name ids in + `MaybeASync (parent last, None, accn, name, delegate name)) | `Fork((_, hd', GuaranteesOpacity, ids), _) -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in @@ -1684,16 +1693,27 @@ let collect_proof keep cur hd brkind id = else make_sync `AlreadyEvaluated rc let string_of_reason = function - | `Transparent -> "Transparent" - | `AlreadyEvaluated -> "AlreadyEvaluated" - | `Policy -> "Policy" - | `NestedProof -> "NestedProof" - | `Immediate -> "Immediate" - | `Alias -> "Alias" - | `NoHint -> "NoHint" - | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity" - | `Aborted -> "Aborted" - | _ -> "Unknown Reason" + | `Transparent -> "non opaque" + | `AlreadyEvaluated -> "proof already evaluated" + | `Policy -> "policy" + | `NestedProof -> "contains nested proof" + | `Immediate -> "proof term given explicitly" + | `Aborted -> "aborted proof" + | `Doesn'tGuaranteeOpacity -> "not a simple opaque lemma" + | `MutualProofs -> "block of mutually recursive proofs" + | `Alias -> "contains Undo-like command" + | `Print -> "contains Print-like command" + | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section" + | `Unknown -> "unsupported case" + +let log_string s = prerr_debug ("STM: " ^ s) +let log_processing_async id name = log_string Printf.(sprintf + "%s: proof %s: asynch" (Stateid.to_string id) name +) +let log_processing_sync id name reason = log_string Printf.(sprintf + "%s: proof %s: synch (cause: %s)" + (Stateid.to_string id) name (string_of_reason reason) +) let wall_clock_last_fork = ref 0.0 @@ -1758,7 +1778,7 @@ let known_state ?(redefine_qed=false) ~cache id = assert(keep == VtKeep || keep == VtKeepAsAxiom); let drop_pt = keep == VtKeepAsAxiom in let stop, exn_info, loc = eop, (id, eop), x.loc in - prerr_endline ("Asynchronous " ^ Stateid.to_string id); + log_processing_async id name; VCS.create_cluster nodes ~qed:id ~start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false @@ -1796,8 +1816,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach eop; vernac_interp id x; Proof_global.discard_all () ), `Yes, true | `Sync (name, pua, reason) -> (fun () -> - prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^ - string_of_reason reason); + log_processing_sync id name reason; reach eop; let wall_clock = Unix.gettimeofday () in record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork); @@ -1823,12 +1842,11 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.discard_all () ), `Yes, true | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () -> - prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id); reach ~cache:`Shallow start; (* no sections *) if List.is_empty (Environ.named_context (Global.env ())) then pi1 (aux (`ASync (start, pua, nodes, name, delegate))) () - else pi1 (aux (`Sync (name, pua, `Unknown))) () + else pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) () ), (if redefine_qed then `No else `Yes), true in aux (collect_proof keep (view.next, x) brname brinfo eop) @@ -1885,9 +1903,16 @@ let observe id = iraise e let finish ?(print_goals=false) () = - observe (VCS.get_branch_pos (VCS.current_branch ())); + let head = VCS.current_branch () in + observe (VCS.get_branch_pos head); if print_goals then msg_notice (pr_open_cur_subgoals ()); - VCS.print () + VCS.print (); + (* Some commands may by side effect change the proof mode *) + match VCS.get_branch head with + | { VCS.kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode + | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode + | _ -> () + let wait () = Slaves.wait_all_done (); @@ -2356,7 +2381,7 @@ let interp verb (_,e as lexpr) = verb && match clas with | VtQuery _, _ -> false | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true - | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in + | _ -> not !Flags.coqtop_ui in try finish ~print_goals () with e -> let e = Errors.push e in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 81fad13793..783ff2e116 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -65,6 +65,11 @@ let rec classify_vernac e = | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) when !Flags.print_emacs -> VtStm(VtPG,false), VtNow + (* Univ poly compatibility: we run it now, so that we can just + * look at Flags in stm.ml. Would be nicer to have the stm + * look at the entire dag to detect this option. *) + | VernacSetOption (["Universe"; "Polymorphism"],_) + | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow (* Stm *) | VernacStm Finish -> VtStm (VtFinish, true), VtNow | VernacStm Wait -> VtStm (VtWait, true), VtNow |