From 4f640bb24dfc45699670f41441355cdf71c83130 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 15 Feb 2016 16:11:11 +0100 Subject: STM: classify some variants of Instance as regular `Fork nodes. "Instance name : Type." is like "Lemma name : Type", i.e. it starts a proof. Unfortunately sometimes it does not, so we say VtUnknown. Still, if there is an open proof, we classify it as a regular Lemma, i.e. the opacity depends only on the terminator. This makes CoqIDE and PIDE based UI way more responsive when processing files containing Instance that are proved by tactics, since they are now correctly delegated to workers. Bug reported privately by Alec Faithfull. --- stm/stm.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 56dcda6a4a..f2855d5087 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2254,7 +2254,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[])); + let opacity_of_produced_term = + match x.expr with + | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | _ -> Doesn'tGuaranteeOpacity in + VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode "Classic"; end else begin -- cgit v1.2.3 From 9aa2d99fb1ad6b348142fce244f277b9dd25017f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Feb 2016 11:51:04 +0100 Subject: STM: Print/Extraction have to be skipped if -quick Print and Extraction commands may pierce opacity: if the task producing the proof term is not finished, we wait for its completion. In -quick mode no worker is going to process a task, since tasks are simply stored to disk (and resumed later in -vio2vo mode). This commit avoids coqc waits forever for a task in order to Print/Extract the corresponding term. Bug reported privately by Alec Faithfull. --- stm/stm.ml | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index f2855d5087..a6d119f0cd 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -83,6 +83,18 @@ let async_proofs_workers_extra_env = ref [||] type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr } let pr_ast { expr } = pr_vernac expr +(* Commands piercing opaque *) +let may_pierce_opaque = function + | { expr = VernacPrint (PrintName _) } -> true + | { expr = VernacExtend (("Extraction",_), _) } -> true + | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true + | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true + | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true + | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true + | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true + | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true + | _ -> false + (* Wrapper for Vernacentries.interp to set the feedback id *) let vernac_interp ?proof id ?route { verbose; loc; expr } = let rec internal_command = function @@ -145,7 +157,7 @@ type cmd_t = { ceff : bool; (* is a side-effecting command *) cast : ast; cids : Id.t list; - cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] } + cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] } type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list type qed_t = { qast : ast; @@ -1665,7 +1677,7 @@ let delegate name = let time = get_hint_bp_time name in time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio || !Flags.async_proofs_full - + let collect_proof keep cur hd brkind id = prerr_endline ("Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -1687,23 +1699,20 @@ 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 - (* These do not exactly pierce opaque, but are anyway impossible to properly - * delegate *) + let too_complex_to_delegate = function | { expr = (VernacDeclareModule _ | VernacDefineModule _ | VernacDeclareModuleType _ | VernacInclude _) } -> true | { expr = (VernacRequire _ | VernacImport _) } -> true - | _ -> false in + | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> 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) + when too_complex_to_delegate 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 (* An Alias could jump everywhere... we hope we can ignore it*) @@ -1811,6 +1820,8 @@ let known_state ?(redefine_qed=false) ~cache id = | `Alias (id,_) -> (fun () -> reach view.next; reach id ), cache, true + | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () -> + reach view.next), cache, true | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> reach ~cache:`Shallow view.next; Hooks.(call tactic_being_run true); @@ -2176,6 +2187,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let id = VCS.new_node ~id:newtip () in let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) + else if Flags.(!compilation_mode = BuildVio) && + VCS.((get_branch head).kind = `Master) && + may_pierce_opaque x + then `SkipQueue else `MainQueue in VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok -- cgit v1.2.3