From 7461f18cbe722610613bdd8c729665ac48395b6e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 5 Apr 2019 21:21:53 +0200
Subject: [vernac] [ast] Make location info an attribute of vernaculars.

This has been a mess for quite a while, we try to improve it.
---
 stm/proofBlockDelimiter.ml |  4 +--
 stm/stm.ml                 | 88 ++++++++++++++++++++++++----------------------
 stm/stm.mli                |  4 +--
 stm/vernac_classifier.ml   | 10 +++---
 4 files changed, 54 insertions(+), 52 deletions(-)

(limited to 'stm')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index d13763cdec..2b32838964 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -99,7 +99,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
+         recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
       }
   | `Not -> `Leaks
 
@@ -128,7 +128,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
+         recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
       }
   | `Not -> `Leaks
 
diff --git a/stm/stm.ml b/stm/stm.ml
index e1ab45163a..3eade34448 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -119,7 +119,6 @@ let async_proofs_workers_extra_env = ref [||]
 
 type aast = {
   verbose : bool;
-  loc : Loc.t option;
   indentation : int;
   strlen : int;
   mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *)
@@ -1147,12 +1146,12 @@ end
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 (* It is currently called 19 times, this number should be certainly
    reduced... *)
-let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t =
+let stm_vernac_interp ?proof ?route id st { verbose; expr } : Vernacstate.t =
   (* The Stm will gain the capability to interpret commmads affecting
      the whole document state, such as backtrack, etc... so we start
      to design the stm command interpreter now *)
   set_id_for_feedback ?route dummy_doc id;
-  Aux_file.record_in_aux_set_at ?loc ();
+  Aux_file.record_in_aux_set_at ?loc:expr.CAst.loc ();
   (* We need to check if a command should be filtered from
    * vernac_entries, as it cannot handle it. This should go away in
    * future refactorings.
@@ -1173,7 +1172,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
       | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *)
       | _ ->
         stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
-        try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr)
+        try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr
         with e ->
           let e = CErrors.push e in
           Exninfo.iraise Hooks.(call_process_error_once e)
@@ -1628,8 +1627,8 @@ end = struct (* {{{ *)
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           stm_vernac_interp stop
             ~proof:(pobject, terminator) st
-            { verbose = false; loc; indentation = 0; strlen = 0;
-              expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
+            { verbose = false; indentation = 0; strlen = 0;
+              expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1778,8 +1777,8 @@ end = struct (* {{{ *)
       (* STATE We use the state resulting from reaching start. *)
       let st = Vernacstate.freeze_interp_state ~marshallable:false in
       ignore(stm_vernac_interp stop ~proof st
-        { verbose = false; loc; indentation = 0; strlen = 0;
-          expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
+        { verbose = false; indentation = 0; strlen = 0;
+          expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
       `OK proof
       end
     with e ->
@@ -1791,10 +1790,11 @@ end = struct (* {{{ *)
             spc () ++ iprint (e, info))
       | Some (_, cur) ->
           match VCS.visit cur with
-          | { step = `Cmd { cast = { loc } } }
-          | { step = `Fork (( { loc }, _, _, _), _) }
-          | { step = `Qed ( { qast = { loc } }, _) }
-          | { step = `Sideff (ReplayCommand { loc }, _) } ->
+          | { step = `Cmd { cast } }
+          | { step = `Fork (( cast, _, _, _), _) }
+          | { step = `Qed ( { qast = cast }, _) }
+          | { step = `Sideff (ReplayCommand cast, _) } ->
+              let loc = cast.expr.CAst.loc in
               let start, stop = Option.cata Loc.unloc (0,0) loc in
               msg_warning Pp.(
                 str"File " ++ str name ++ str ": proof of " ++ str r_name ++
@@ -2071,14 +2071,14 @@ end = struct (* {{{ *)
       f ()
 
   let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
-    { indentation; verbose; loc; expr = e; strlen } : unit
+    { indentation; verbose; expr = e; strlen } : unit
   =
     let e, time, batch, fail =
-      let rec find ~time ~batch ~fail = function
-        | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e
-        | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e
-        | VernacFail {CAst.v=e} -> find ~time ~batch ~fail:true e
-        | e -> e, time, batch, fail in
+      let rec find ~time ~batch ~fail v = CAst.with_loc_val (fun ?loc -> function
+        | VernacTime (batch,e) -> find ~time:true ~batch ~fail e
+        | VernacRedirect (_,e) -> find ~time ~batch ~fail e
+        | VernacFail e -> find ~time ~batch ~fail:true e
+        | e -> CAst.make ?loc e, time, batch, fail) v in
       find ~time:false ~batch:false ~fail:false e in
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     stm_fail ~st fail (fun () ->
@@ -2092,7 +2092,7 @@ end = struct (* {{{ *)
           Future.create_delegate
             ~name:(Printf.sprintf "subgoal %d" i)
             (State.exn_on id ~valid:safe_id) in
-        let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in
+        let t_ast = (i, { indentation; verbose; expr = e; strlen }) in
         let t_name = Goal.uid g in
         TaskQueue.enqueue_task queue
           { t_state = safe_id; t_state_fb = id;
@@ -2241,7 +2241,7 @@ let collect_proof keep cur hd brkind id =
  let name = function
    | [] -> no_name
    | id :: _ -> Names.Id.to_string id in
- let loc = (snd cur).loc in
+ let loc = (snd cur).expr.CAst.loc in
  let is_defined_expr = function
    | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
    | _ -> false in
@@ -2307,7 +2307,7 @@ let collect_proof keep cur hd brkind id =
         (try
           let name, hint = name ids, get_hint_ctx loc  in
           let t, v = proof_no_using last in
-          v.expr <- VernacExpr([], VernacProof(t, Some hint));
+          v.expr <- CAst.map (fun _ -> VernacExpr([], VernacProof(t, Some hint))) v.expr;
           `ASync (parent last,accn,name,delegate name)
         with Not_found ->
           let name = name ids in
@@ -2410,7 +2410,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                (* STATE: We use an updated state with proof *)
                let st = Vernacstate.freeze_interp_state ~marshallable:false in
                Option.iter (fun expr -> ignore(stm_vernac_interp id st {
-                  verbose = true; loc = None; expr; indentation = 0;
+                  verbose = true; expr; indentation = 0;
                   strlen = 0 } ))
                recovery_command
            | _ -> assert false
@@ -2530,7 +2530,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
             | `ASync (block_start, nodes, name, delegate) -> (fun () ->
                 let keep' = get_vtkeep keep in
                 let drop_pt = keep' == VtKeepAxiom in
-                let block_stop, exn_info, loc = eop, (id, eop), x.loc in
+                let block_stop, exn_info, loc = eop, (id, eop), x.expr.CAst.loc in
                 log_processing_async id name;
                 VCS.create_proof_task_box nodes ~qed:id ~block_start;
                 begin match brinfo, qed.fproof with
@@ -2590,7 +2590,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 log_processing_sync id name reason;
                 reach eop;
                 let wall_clock = Unix.gettimeofday () in
-                record_pb_time name ?loc:x.loc (wall_clock -. !wall_clock_last_fork);
+                record_pb_time name ?loc:x.expr.CAst.loc (wall_clock -. !wall_clock_last_fork);
                 let proof =
                   match keep with
                   | VtDrop -> None
@@ -2612,7 +2612,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 let st = Vernacstate.freeze_interp_state ~marshallable:false in
                 ignore(stm_vernac_interp id ?proof st x);
                 let wall_clock3 = Unix.gettimeofday () in
-                Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
+                Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
                   (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
                 Vernacstate.Proof_global.discard_all ()
               ), true, true
@@ -2932,7 +2932,7 @@ let get_allow_nested_proofs =
 
 (** [process_transaction] adds a node in the document *)
 let process_transaction ~doc ?(newtip=Stateid.fresh ())
-  ({ verbose; loc; expr } as x) c =
+  ({ verbose; expr } as x) c =
   stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
   try
@@ -3118,11 +3118,11 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
 
 let get_ast ~doc id =
   match VCS.visit id with
-  | { step = `Cmd { cast = { loc; expr } } }
-  | { step = `Fork (({ loc; expr }, _, _, _), _) }
-  | { step = `Sideff ((ReplayCommand {loc; expr}) , _) }
-  | { step = `Qed ({ qast = { loc; expr } }, _) } ->
-         Some (Loc.tag ?loc expr)
+  | { step = `Cmd { cast = { expr } } }
+  | { step = `Fork (({ expr }, _, _, _), _) }
+  | { step = `Sideff ((ReplayCommand { expr }) , _) }
+  | { step = `Qed ({ qast = { expr } }, _) } ->
+    Some expr
   | _ -> None
 
 let stop_worker n = Slaves.cancel_worker n
@@ -3139,8 +3139,8 @@ let parse_sentence ~doc sid ~entry pa =
 let ind_len_loc_of_id sid =
   if Stateid.equal sid Stateid.initial then None
   else match (VCS.visit sid).step with
-  | `Cmd { ctac = true; cast = { indentation; strlen; loc } } ->
-         Some (indentation, strlen, loc)
+  | `Cmd { ctac = true; cast = { indentation; strlen; expr } } ->
+    Some (indentation, strlen, expr.CAst.loc)
   | _ -> None
 
 (* the indentation logic works like this: if the beginning of the
@@ -3167,7 +3167,8 @@ let compute_indentation ?loc sid = Option.cata (fun loc ->
     eff_indent, len
   ) (0, 0) loc
 
-let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
+let add ~doc ~ontop ?newtip verb ast =
+  let loc = ast.CAst.loc in
   let cur_tip = VCS.cur_tip () in
   if not (Stateid.equal ontop cur_tip) then
     user_err ?loc ~hdr:"Stm.add"
@@ -3177,7 +3178,7 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
   let indentation, strlen = compute_indentation ?loc ontop in
   (* XXX: Classifiy vernac should be moved inside process transaction *)
   let clas = Vernac_classifier.classify_vernac ast in
-  let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
+  let aast = { verbose = verb; indentation; strlen; expr = ast } in
   match process_transaction ~doc ?newtip aast clas with
   | `Ok -> doc, VCS.cur_tip (), `NewTip
   | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ())
@@ -3197,14 +3198,15 @@ let query ~doc ~at ~route s =
       let rec loop () =
         match parse_sentence ~doc at ~entry:Pvernac.main_entry s with
         | None -> ()
-        | Some {CAst.loc; v=ast} ->
-           let indentation, strlen = compute_indentation ?loc at in
-           let st = State.get_cached at in
-           let aast = {
-             verbose = true; indentation; strlen;
-             loc; expr = ast } in
-           ignore(stm_vernac_interp ~route at st aast);
-           loop ()
+        | Some ast ->
+          let loc = ast.CAst.loc in
+          let indentation, strlen = compute_indentation ?loc at in
+          let st = State.get_cached at in
+          let aast = {
+            verbose = true; indentation; strlen;
+            expr = ast } in
+          ignore(stm_vernac_interp ~route at st aast);
+          loop ()
       in
       loop ()
   )
diff --git a/stm/stm.mli b/stm/stm.mli
index 91651e3534..9d2bf56629 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -111,7 +111,7 @@ val parse_sentence :
    If [newtip] is provided, then the returned state id is guaranteed
    to be [newtip] *)
 val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
-  bool -> Vernacexpr.vernac_control CAst.t ->
+  bool -> Vernacexpr.vernac_control ->
   doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
 (* Returns the proof state before the last tactic that was applied at or before
@@ -175,7 +175,7 @@ val get_current_state : doc:doc -> Stateid.t
 val get_ldir : doc:doc -> Names.DirPath.t
 
 (* This returns the node at that position *)
-val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option
+val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option
 
 (* Filename *)
 val set_compilation_hints : string -> unit
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 243b5c333d..674b4285d2 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -200,20 +200,20 @@ let classify_vernac e =
         try Vernacextend.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
-  let rec static_control_classifier = function
+  let rec static_control_classifier v = v |> CAst.with_val (function
     | VernacExpr (f, e) ->
       let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
       static_classifier ~poly e
-    | VernacTimeout (_,{v=e}) -> static_control_classifier e
-    | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
+    | VernacTimeout (_,e) -> static_control_classifier e
+    | VernacTime (_,e) | VernacRedirect (_, e) ->
        static_control_classifier e
-    | VernacFail {v=e} -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+    | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match static_control_classifier e with
         | ( VtQuery | VtProofStep _ | VtSideff _
           | VtMeta), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtLater
-        | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)
+        | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater))
   in
   static_control_classifier e
-- 
cgit v1.2.3


From a7f678c2209bbe56b18ed3cdf1306fed161d7b07 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 7 May 2019 08:07:34 +0000
Subject: [Record] Une a record to gather field declaration attributes

---
 stm/vernac_classifier.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 674b4285d2..4a4c5c94e9 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -137,7 +137,7 @@ let classify_vernac e =
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
            CList.map_filter (function
-            | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n
+            | AssumExpr({v=Names.Name n},_), _ -> Some n
             | _ -> None) l) l in
         VtSideff (List.flatten ids), VtLater
     | VernacScheme l ->
-- 
cgit v1.2.3


From 6211fd6e067e781a160db8765dd87067428048f2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 1 Nov 2018 23:26:06 +0100
Subject: Moving Evd.evars_of_term from constr to econstr + consequences.

This impacts a lot of code, apparently in the good, removing several
conversions back and forth constr.
---
 stm/proofBlockDelimiter.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 2b32838964..74a3ee035c 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -41,7 +41,7 @@ let simple_goal sigma g gs =
   let open Evd in
   let open Evarutil in
   let evi = Evd.find sigma g in
-  Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) &&
+  Set.is_empty (evars_of_term evi.evar_concl) &&
   Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
-- 
cgit v1.2.3


From 6608f64f001f8f1a50b2dc41fefdf63c0b84b270 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Nov 2018 00:17:47 +0100
Subject: Passing evar_map to evars_of_term rather than expecting the term to
 be evar-nf.

---
 stm/proofBlockDelimiter.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 74a3ee035c..04f10e7399 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -41,8 +41,8 @@ let simple_goal sigma g gs =
   let open Evd in
   let open Evarutil in
   let evi = Evd.find sigma g in
-  Set.is_empty (evars_of_term evi.evar_concl) &&
-  Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
+  Set.is_empty (evars_of_term sigma evi.evar_concl) &&
+  Set.is_empty (evars_of_filtered_evar_info sigma (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
 let is_focused_goal_simple ~doc id =
-- 
cgit v1.2.3


From 63a953ddc0db1ec1bf101ed6afdf9262d0d9f355 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 May 2019 21:28:25 +0200
Subject: Ensuring suffix of file to compile also for -vio2vo checking.

We do it by consistently using variants of the "ensure_exists" policy
in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and
parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and
parallel vio checking (schedule-vio-checking).

For instance, coqc -vio2vo dir/file.vio now works, while before,
dir/file was expected.

Incidentally, this avoids the non-recommended Loadpath.locate_file.
---
 stm/vio_checking.ml | 31 ++++++++++++-------------------
 1 file changed, 12 insertions(+), 19 deletions(-)

(limited to 'stm')

diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 69c1d9bd23..0f78e0acf6 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -10,11 +10,11 @@
 
 open Util
 
-let check_vio (ts,f) =
+let check_vio (ts,f_in) =
   Dumpglob.noglob ();
-  let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in
-  Stm.set_compilation_hints long_f_dot_v;
-  List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
+  let _, _, _, _, tasks, _ = Library.load_library_todo f_in in
+  Stm.set_compilation_hints f_in;
+  List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts
 
 module Worker = Spawn.Sync ()
 
@@ -28,15 +28,12 @@ module Pool = Map.Make(IntOT)
 let schedule_vio_checking j fs =
   if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
   let jobs = ref [] in
-  List.iter (fun f ->
-    let f =
-      if Filename.check_suffix f ".vio" then Filename.chop_extension f
-      else f in
-    let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in
-    Stm.set_compilation_hints long_f_dot_v;
+  List.iter (fun long_f_dot_vio ->
+    let _,_,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in
+    Stm.set_compilation_hints long_f_dot_vio;
     let infos = Stm.info_tasks tasks in
     let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
-    if infos <> [] then jobs := (f, eta, infos) :: !jobs)
+    if infos <> [] then jobs := (long_f_dot_vio, eta, infos) :: !jobs)
   fs;
   let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in
   jobs := List.sort cmp_job !jobs;
@@ -103,16 +100,12 @@ let schedule_vio_checking j fs =
 let schedule_vio_compilation j fs =
   if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
   let jobs = ref [] in
-  List.iter (fun f ->
-    let f =
-      if Filename.check_suffix f ".vio" then Filename.chop_extension f
-      else f in
-    let long_f_dot_v = Loadpath.locate_file (f^".v") in
-    let aux = Aux_file.load_aux_file_for long_f_dot_v in
+  List.iter (fun long_f_dot_vio ->
+    let aux = Aux_file.load_aux_file_for long_f_dot_vio in
     let eta =
       try float_of_string (Aux_file.get aux "vo_compile_time")
       with Not_found -> 0.0 in
-    jobs := (f, eta) :: !jobs)
+    jobs := (long_f_dot_vio, eta) :: !jobs)
   fs;
   let cmp_job (_,t1) (_,t2) = compare t2 t1 in
   jobs := List.sort cmp_job !jobs;
@@ -146,7 +139,7 @@ let schedule_vio_compilation j fs =
     (* 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;
+    List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs;
   end;
   exit !rc
 
-- 
cgit v1.2.3


From 9a49153b2104e8d7ca0d7789b47299295272746c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 May 2019 01:45:42 +0200
Subject: Removing no more existing option -emacs-U.

---
 stm/asyncTaskQueue.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 2493b1fac4..8b455821af 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -125,7 +125,7 @@ module Make(T : Task) () = struct
                  "-async-proofs-worker-priority";
                  CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
         (* Options to discard: 0 arguments *)
-        | ("-emacs"|"-emacs-U"|"-batch")::tl ->
+        | ("-emacs"|"-batch")::tl ->
           set_slave_opt tl
         (* Options to discard: 1 argument *)
         | ( "-async-proofs" | "-vio2vo" | "-o"
-- 
cgit v1.2.3


From 682ec8fe694e37757d2cd6c98fb5e2e609a6f08f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 9 May 2019 14:07:16 +0200
Subject: Allow run_tactic to return a value, remove hack from ltac2

---
 stm/stm.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 3eb6d03529..21618bc044 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2085,8 +2085,8 @@ end = struct (* {{{ *)
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     stm_fail ~st fail (fun () ->
     (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
-    ignore(TaskQueue.with_n_workers nworkers (fun queue ->
-    PG_compat.with_current_proof (fun _ p ->
+    TaskQueue.with_n_workers nworkers (fun queue ->
+    PG_compat.simple_with_current_proof (fun _ p ->
       let Proof.{goals} = Proof.data p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
@@ -2131,7 +2131,8 @@ end = struct (* {{{ *)
             if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
         end)
       in
-      Proof.run_tactic (Global.env()) assign_tac p)))) ())
+      let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in
+      p))) ())
 
 end (* }}} *)
 
-- 
cgit v1.2.3


From c352873936db93c251c544383853474736f128d6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 00:48:36 +0100
Subject: Remove VtUnknown classification

This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.

The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.

We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.

Fixes #3632 #3890 #4638.
---
 stm/stm.ml               | 51 +-----------------------------------------------
 stm/vernac_classifier.ml | 36 ++++++++++++++++++++--------------
 2 files changed, 22 insertions(+), 65 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 21618bc044..6f7cefb582 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -364,7 +364,6 @@ module VCS : sig
   val set_parsing_state : id -> Vernacstate.Parser.state -> unit
   val get_parsing_state : id -> Vernacstate.Parser.state option
   val get_proof_mode : id -> Pvernac.proof_mode option
-  val set_proof_mode : id -> Pvernac.proof_mode option -> unit
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
   val slice : block_start:id -> block_stop:id -> vcs
@@ -572,6 +571,7 @@ end = struct (* {{{ *)
     (match Vernacprop.under_control x with
     | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
     | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
+    | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i
     | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -611,7 +611,6 @@ end = struct (* {{{ *)
     info.state <- new_state
 
   let get_proof_mode id = (get_info id).proof_mode
-  let set_proof_mode id pm = (get_info id).proof_mode <- pm
 
   let reached id =
     let info = get_info id in
@@ -3050,53 +3049,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               VCS.set_parsing_state id parsing_state) new_ids;
           `Ok
 
-      (* 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
-          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 newtip
-            |> Exninfo.iraise
-          else
-            let id = VCS.new_node ~id:newtip proof_mode () 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 () =
-            VCS.checkout VCS.Branch.master;
-            let mid = VCS.get_branch_pos VCS.Branch.master in
-            let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in
-            let st = Vernacstate.freeze_interp_state ~marshallable:false in
-            ignore(stm_vernac_interp id st x);
-            (* Vernac x may or may not start a proof *)
-            if not in_proof && PG_compat.there_are_pending_proofs () then
-            begin
-              let bname = VCS.mk_branch_name x in
-              let opacity_of_produced_term = function
-                (* This AST is ambiguous, hence we check it dynamically *)
-                | VernacInstance (_,_ , None, _) -> GuaranteesOpacity
-                | _ -> Doesn'tGuaranteeOpacity in
-              VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
-              VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ()));
-              VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
-            end else begin
-              begin match (VCS.get_branch head).VCS.kind with
-              | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-              | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-              | `Proof _ ->
-                  VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-                  (* We hope it can be replayed, but we can't really know *)
-                  ignore(VCS.propagate_sideff ~action:(ReplayCommand x));
-              end;
-              VCS.checkout_shallowest_proof_branch ();
-            end in
-          State.define ~doc ~safe_id:head_id ~cache:true step id;
-          Backtrack.record (); `Ok
-
-      | VtUnknown, VtLater ->
-          anomaly(str"classifier: VtUnknown must imply VtNow.")
-
       | VtProofMode pm, VtNow ->
         let proof_mode = Pvernac.lookup_proof_mode pm in
         let id = VCS.new_node ~id:newtip proof_mode () in
@@ -3106,7 +3058,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
 
       | VtProofMode _, VtLater ->
           anomaly(str"classifier: VtProofMode must imply VtNow.")
-
     end in
     let pr_rc rc = match rc with
       | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4a4c5c94e9..7cecd801e4 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -21,7 +21,6 @@ let string_of_parallel = function
   | `No -> ""
 
 let string_of_vernac_type = function
-  | VtUnknown -> "Unknown"
   | VtStartProof _ -> "StartProof"
   | VtSideff _ -> "Sideff"
   | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
@@ -61,7 +60,7 @@ let options_affecting_stm_scheduling =
   ]
 
 let classify_vernac e =
-  let static_classifier ~poly e = match e with
+  let static_classifier ~atts e = match e with
     (* 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. *)
@@ -97,15 +96,18 @@ let classify_vernac e =
       VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
 
     | VernacDefinition (_,({v=i},_),ProveBody _) ->
-       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof(guarantee, idents_of_name i), VtLater
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+      VtStartProof(guarantee, idents_of_name i), VtLater
     | VernacStartTheoremProof (_,l) ->
-        let ids = List.map (fun (({v=i}, _), _) -> i) l in
-       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof (guarantee,ids), VtLater
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+      let ids = List.map (fun (({v=i}, _), _) -> i) l in
+      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+      VtStartProof (guarantee,ids), VtLater
     | VernacFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
@@ -115,8 +117,9 @@ let classify_vernac e =
         then VtStartProof (guarantee,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
@@ -185,8 +188,12 @@ let classify_vernac e =
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
     | VernacProofMode pm -> VtProofMode pm, VtNow
-    (* These are ambiguous *)
-    | VernacInstance _ -> VtUnknown, VtNow
+    | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+      VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater
+    | VernacInstance (_,((name,_),_,_),_,_) ->
+      VtSideff (idents_of_name name.CAst.v), VtLater
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
@@ -201,9 +208,8 @@ let classify_vernac e =
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier v = v |> CAst.with_val (function
-    | VernacExpr (f, e) ->
-      let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
-      static_classifier ~poly e
+    | VernacExpr (atts, e) ->
+      static_classifier ~atts e
     | VernacTimeout (_,e) -> static_control_classifier e
     | VernacTime (_,e) | VernacRedirect (_, e) ->
        static_control_classifier e
@@ -214,6 +220,6 @@ let classify_vernac e =
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtLater
-        | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater))
+        | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater))
   in
   static_control_classifier e
-- 
cgit v1.2.3