aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml2
-rw-r--r--stm/stm.ml51
-rw-r--r--stm/vernac_classifier.ml36
-rw-r--r--stm/vio_checking.ml31
4 files changed, 35 insertions, 85 deletions
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"
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 22:14:43 +0000