From 99ed6c907c3b2c4901ba51446e0b67696929e02e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Mar 2015 16:57:31 +0100 Subject: STM: avoid processing asynchronously empty proofs (Close: #4134) --- stm/stm.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index d9ecc8bcce..267f08ed5f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1638,6 +1638,7 @@ let collect_proof keep cur hd brkind id = | { expr = VernacPrint (PrintName _) } -> true | _ -> false 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 @@ -1687,7 +1688,8 @@ let collect_proof keep cur hd brkind id = else if keep == VtDrop then `Sync (no_name,None,`Aborted) else let rc = collect (Some cur) [] id in - if (keep == VtKeep || keep == VtKeepAsAxiom) && + if is_empty rc then make_sync `AlreadyEvaluated rc + else if (keep == VtKeep || keep == VtKeepAsAxiom) && (not(State.is_cached id) || !Flags.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc -- cgit v1.2.3 From 2ef5fa7910e644d7eb39ee01024878a67086bd42 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Mar 2015 10:45:38 +0100 Subject: STM: change how proof mode switching commands are handled (decl_mode) This is likely to make nested proofs containing proof modes switch broken, but fixes the problems Arnaud has in his branch. It is possible that the classification function we have today is not fine grained enough. If a command that changes the proof mode has as the only global effect changing the proof mode, then the current code is fine. If it has a more global effect that persists after the proof is over but has no impact on the proof itself, then the old code is fine. As far as I can get, the proof mode switching commands have a global effect (changing parser) but also a proof effect (un/focusing). We don't have a classification for these. Today a command having a global effect is played twice: on the proof branch an on master. Of course if such command cannot work on master (where there is no finished proof for example) we need a special treatment for it. --- stm/stm.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 267f08ed5f..9e30cbbcd9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2126,9 +2126,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = anomaly(str"VtProofMode must be executed VtNow") | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in - VCS.checkout VCS.Branch.master; VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue}); - VCS.propagate_sideff (Some x); List.iter (fun bn -> match VCS.get_branch bn with | { VCS.root; kind = `Master; pos } -> () -- cgit v1.2.3 From a5a333ddbf5c27320e767ca0611caf8a821449aa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 27 Mar 2015 12:02:30 +0100 Subject: STM: refine the notion of "simply a tactic" When a worker sends back a system state to master, it tries to just send a delta. If the command is a simple tactic, then only the proof state changes. Now, what is a simple tactic? 1. a tactic 2. that does not change the environment Check 1. was surely incomplete. Now it is: VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ Is it complete? --- stm/stm.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 9e30cbbcd9..477ca1f0dc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1093,6 +1093,9 @@ end = struct (* {{{ *) let perform_states query = if query = [] then [] else + let is_tac = function + | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true + | _ -> false in let initial = let rec aux id = try match VCS.visit id with { next } -> aux next @@ -1110,8 +1113,8 @@ end = struct (* {{{ *) if State.is_cached id then Some (State.get_cached id) else None in match prev, this with | _, None -> None - | Some (prev, o, `Cmd { cast = { expr = VernacSolve _ }}), Some n - when State.same_env o n -> (* A pure tactic *) + | Some (prev, o, `Cmd { cast = { expr }}), Some n + when is_tac expr && State.same_env o n -> (* A pure tactic *) Some (id, `Proof (prev, State.proof_part_of_frozen n)) | Some _, Some s -> msg_warning (str "Sending back a fat state"); -- cgit v1.2.3 From e8b4756c655eacd8a2b9b23630ba02dbbbc4e96e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 27 Mar 2015 18:17:03 +0100 Subject: Putting the From parameter of the Require command into the AST. --- stm/texmacspp.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index a0979f8b15..083fd54bfa 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -617,14 +617,17 @@ let rec tmpp v loc = | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id) | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id) | VernacNameSectionHypSet _ as x -> xmlTODO loc x - | VernacRequire (None,l) -> - xmlRequire loc (List.map (fun ref -> - xmlReference ref) l) - | VernacRequire (Some true,l) -> - xmlRequire loc ~attr:["export","true"] (List.map (fun ref -> - xmlReference ref) l) - | VernacRequire (Some false,l) -> - xmlRequire loc ~attr:["import","true"] (List.map (fun ref -> + | VernacRequire (from, import, l) -> + let import = match import with + | None -> [] + | Some true -> ["export","true"] + | Some false -> ["import","true"] + in + let from = match from with + | None -> [] + | Some r -> ["from", Libnames.string_of_reference r] + in + xmlRequire loc ~attr:(from @ import) (List.map (fun ref -> xmlReference ref) l) | VernacImport (true,l) -> xmlImport loc ~attr:["export","true"] (List.map (fun ref -> -- cgit v1.2.3