Merge branch 'v8.5'

6 files changed, 51 insertions, 35 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 672527d9b5..e3fb0b607a 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -177,7 +177,7 @@ module Make(T : Task) = struct
       if not (Worker.is_alive proc) then ()
       else if cancelled () || !(!expiration_date) then
         let () = stop_waiting := true in
-        let () = TQueue.signal_destruction queue in
+        let () = TQueue.broadcast queue in
         Worker.kill proc
       else
         let () = Unix.sleep 1 in
@@ -253,6 +253,8 @@ module Make(T : Task) = struct
     Pool.destroy active;
     TQueue.destroy queue
 
+  let broadcast { queue } = TQueue.broadcast queue
+
   let enqueue_task { queue; active } (t, _ as item) =
     prerr_endline ("Enqueue task "^T.name_of_task t);
     TQueue.push queue item
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index 78f295d3d5..a3fe4b8c0d 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -61,6 +61,8 @@ module MakeQueue(T : Task) : sig
 
   val set_order : queue -> (T.task -> T.task -> int) -> unit
 
+  val broadcast : queue -> unit
+
   (* Take a snapshot (non destructive but waits until all workers are
    * enqueued) *)
   val snapshot : queue -> T.task list
diff --git a/stm/stm.ml b/stm/stm.ml
index 207afd8aee..43db6f3f6c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -132,6 +132,7 @@ type branch_type =
   | `Proof of proof_mode * depth
   | `Edit of proof_mode * Stateid.t * Stateid.t ]
 type cmd_t = {
+  ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
   cast : ast;
   cids : Id.t list;
   cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
@@ -144,7 +145,7 @@ type qed_t = {
   brinfo : branch_type Vcs_.branch_info
 }
 type seff_t = ast option
-type alias_t = Stateid.t
+type alias_t = Stateid.t * ast
 type transaction =
   | Cmd    of cmd_t
   | Fork   of fork_t
@@ -315,7 +316,7 @@ end = struct (* {{{ *)
             (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
       | Sideff None -> "EnvChange"
       | Noop -> " "
-      | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id)
+      | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
       | Qed { qast } -> string_of_ppcmds (pr_ast qast) in
     let is_green id = 
       match get_info vcs id with
@@ -769,19 +770,20 @@ end = struct (* {{{ *)
     match info.vcs_backup with
     | None, _ -> next acc
     | Some vcs, _ ->
-        let ids =
-          if id = Stateid.initial || id = Stateid.dummy then [] else
+        let ids, tactic, undo =
+          if id = Stateid.initial || id = Stateid.dummy then [],false,0 else
           match VCS.visit id with
-          | { step = `Fork ((_,_,_,l),_) } -> l
-          | { step = `Cmd { cids = l } } -> l
-          | _ -> [] in
-        match f acc (id, vcs, ids) with
+          | { step = `Fork ((_,_,_,l),_) } -> l, false,0
+          | { step = `Cmd { cids = l; ctac } } -> l, ctac,0
+          | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n
+          | _ -> [],false,0 in
+        match f acc (id, vcs, ids, tactic, undo) with
         | `Stop x -> x
         | `Cont acc -> next acc
  
   let back_safe () =
     let id =
-      fold_until (fun n (id,_,_) ->
+      fold_until (fun n (id,_,_,_,_) ->
         if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
         0 (VCS.get_branch_pos (VCS.current_branch ())) in
     backto id
@@ -797,7 +799,7 @@ end = struct (* {{{ *)
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
             let oid =
-              fold_until (fun b (id,_,label) ->
+              fold_until (fun b (id,_,label,_,_) ->
                 if b then `Stop id else `Cont (List.mem name label))
               false id in
             VtStm (VtBack oid, true), VtNow
@@ -805,17 +807,15 @@ end = struct (* {{{ *)
             VtStm (VtBack id, true), VtNow)
       | VernacBack n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun n (id,_,_) ->
+          let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
           VtStm (VtBack oid, true), VtNow
       | VernacUndo n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun n (id,_,_) ->
-            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode &&
-             not !Flags.print_emacs then
-           VtStm (VtBack oid, false), VtNow
-          else VtStm (VtBack oid, true), VtLater
+          let oid = fold_until (fun n (id,_,_,tactic,undo) ->
+            let value = (if tactic then 1 else 0) - undo in
+            if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
+          VtStm (VtBack oid, true), VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -826,15 +826,15 @@ end = struct (* {{{ *)
             | Some vcs, _ -> vcs in
           let cb, _ =
             Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in
-          let n = fold_until (fun n (_,vcs,_) ->
+          let n = fold_until (fun n (_,vcs,_,_,_) ->
             if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
             0 id in
-          let oid = fold_until (fun n (id,_,_) ->
+          let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
           VtStm (VtBack oid, true), VtLater
       | VernacAbortAll ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun () (id,vcs,_) ->
+          let oid = fold_until (fun () (id,vcs,_,_,_) ->
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
           VtStm (VtBack oid, true), VtLater
@@ -907,7 +907,10 @@ module rec ProofTask : sig
   val build_proof_here :
     Stateid.t * Stateid.t -> Loc.t -> Stateid.t ->
       Proof_global.closed_proof_output Future.computation
-   
+
+  (* If set, only tasks overlapping with this list are processed *)
+  val set_perspective : Stateid.t list -> unit  
+
 end = struct (* {{{ *)
 
   let forward_feedback msg = Hooks.(call forward_feedback msg)
@@ -946,9 +949,14 @@ end = struct (* {{{ *)
   let name = ref "proofworker"
   let extra_env () = !async_proofs_workers_extra_env
 
+  let perspective = ref []
+  let set_perspective l = perspective := l
+
   let task_match age t =
     match age, t with
-    | `Fresh, BuildProof _ -> true
+    | `Fresh, BuildProof { t_states } ->
+        not !Flags.async_proofs_full ||
+        List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states
     | `Old my_states, States l ->
         List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l
     | _ -> false
@@ -1239,6 +1247,8 @@ end = struct (* {{{ *)
       name, max (time1 +. time2) 0.0001,i) 0 l
 
   let set_perspective idl =
+    ProofTask.set_perspective idl;
+    TaskQueue.broadcast (Option.get !queue);
     let open Stateid in
     let open ProofTask in
     let overlap s1 s2 =
@@ -1667,7 +1677,7 @@ let known_state ?(redefine_qed=false) ~cache id =
     let step, cache_step, feedback_processed =
       let view = VCS.visit id in
       match view.step with
-      | `Alias id -> (fun () ->
+      | `Alias (id,_) -> (fun () ->
             reach view.next; reach id
           ), cache, true
       | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
@@ -1968,11 +1978,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           List.iter (fun b ->
             if not(VCS.Branch.equal b head) then begin
               VCS.checkout b;
-              VCS.commit (VCS.new_node ()) (Alias oid);
+              VCS.commit (VCS.new_node ()) (Alias (oid,x));
             end)
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
-          VCS.commit id (Alias oid);
+          VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtStm (VtBack id, false), VtNow ->
           prerr_endline ("undo to state " ^ Stateid.to_string id);
@@ -2001,7 +2011,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           let queue =
             if !Flags.async_proofs_full then `QueryQueue (ref false)
             else `MainQueue in
-          VCS.commit id (Cmd { cast = x; cids = []; cqueue = queue });
+          VCS.commit id (Cmd {ctac=false;cast = x; cids = []; cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQuery (false,_), VtLater ->
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
@@ -2025,7 +2035,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtProofMode mode, VtNow ->
           let id = VCS.new_node ~id:newtip () in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Cmd {cast = x; cids=[]; cqueue = `MainQueue});
+          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
@@ -2044,7 +2054,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtProofStep paral, w ->
           let id = VCS.new_node ~id:newtip () in
           let queue = if paral then `TacQueue (ref false) else `MainQueue in
-          VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue });
+          VCS.commit id (Cmd {ctac = true;cast = x;cids = [];cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQed keep, w ->
           let valid = if tty then Some(VCS.get_branch_pos head) else None in
@@ -2060,7 +2070,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtSideff l, w ->
           let id = VCS.new_node ~id:newtip () in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Cmd { cast = x; cids = l; cqueue = `MainQueue});
+          VCS.commit id (Cmd {ctac=false;cast=x;cids=l;cqueue=`MainQueue});
           VCS.propagate_sideff (Some x);
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -2084,7 +2094,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
               VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode "Classic";
             end else begin
-              VCS.commit id (Cmd { cast = x; cids = []; cqueue = `MainQueue});
+              VCS.commit id (Cmd {ctac=false; cast = x; cids = []; cqueue = `MainQueue});
               VCS.propagate_sideff (Some x);
               VCS.checkout_shallowest_proof_branch ();
             end in
@@ -2332,7 +2342,7 @@ let get_script prf =
          find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
     | `Sideff (`Id id)  -> find acc id
     | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
-    | `Alias id -> find acc id
+    | `Alias (id,_) -> find acc id
     | `Fork _ -> find acc view.next
     in
   find [] (VCS.get_branch_pos branch)
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 8a62fe79e1..6fef895ae8 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -79,7 +79,7 @@ let pop ?(picky=(fun _ -> true)) ?(destroy=ref false)
   Mutex.unlock m;
   x
 
-let signal_destruction { lock = m; cond = c } =
+let broadcast { lock = m; cond = c } =
   Mutex.lock m;
   Condition.broadcast c;
   Mutex.unlock m
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index bc3922b33a..7458de510f 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -14,7 +14,9 @@ val pop : ?picky:('a -> bool) -> ?destroy:bool ref -> 'a t -> 'a
 val push : 'a t -> 'a -> unit
 val set_order : 'a t -> ('a -> 'a -> int) -> unit
 val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
-val signal_destruction : 'a t -> unit
+
+(* Wake up all waiting threads *)
+val broadcast : 'a t -> unit
 
 (* Non destructive *)
 val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index e9302bb735..81fad13793 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -151,8 +151,8 @@ let rec classify_vernac e =
         let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in
         VtSideff ids, VtLater
     | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
+    | VernacBeginSection (_,id) -> VtSideff [id], VtLater
     | VernacUniverse _ | VernacConstraint _
-    | VernacBeginSection _
     | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
     | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
     | VernacChdir _