aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/spawned.ml4
-rw-r--r--stm/stm.ml90
-rw-r--r--stm/tQueue.ml2
-rw-r--r--stm/vcs.ml2
-rw-r--r--stm/vernac_classifier.ml4
5 files changed, 52 insertions, 50 deletions
diff --git a/stm/spawned.ml b/stm/spawned.ml
index c5bd5f6f96..de19dd5352 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -46,7 +46,7 @@ let control_channel = ref None
let channels = ref None
let init_channels () =
- if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice");
+ if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice.");
let () = match !main_channel with
| None -> ()
| Some (Socket(mh,mpr,mpw)) ->
@@ -65,7 +65,7 @@ let init_channels () =
| Some (Socket (ch, cpr, cpw)) ->
controller ch cpr cpw
| Some AnonPipe ->
- CErrors.anomaly (Pp.str "control channel cannot be a pipe")
+ CErrors.anomaly (Pp.str "control channel cannot be a pipe.")
let get_channels () =
match !channels with
diff --git a/stm/stm.ml b/stm/stm.ml
index 2057496f4b..8ca50e2d54 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -80,7 +80,7 @@ type aast = {
}
let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
(* Commands piercing opaque *)
let may_pierce_opaque = function
@@ -219,7 +219,7 @@ end = struct (* {{{ *)
let find_proof_at_depth vcs pl =
try List.find (function
| _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
- | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
+ | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth.")
| _ -> false)
(List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
with Not_found -> failwith "find_proof_at_depth"
@@ -227,9 +227,9 @@ end = struct (* {{{ *)
exception Expired
let visit vcs id =
if Stateid.equal id Stateid.initial then
- anomaly(Pp.str "Visiting the initial state id")
+ anomaly(Pp.str "Visiting the initial state id.")
else if Stateid.equal id Stateid.dummy then
- anomaly(Pp.str "Visiting the dummy state id")
+ anomaly(Pp.str "Visiting the dummy state id.")
else
try
match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
@@ -245,7 +245,7 @@ end = struct (* {{{ *)
| [n, Sideff (ReplayCommand x); p, Noop]
| [p, Noop; n, Sideff (ReplayCommand x)]-> { step = `Sideff(ReplayCommand x,p); next = n }
| [n, Sideff (ReplayCommand x)]-> {step = `Sideff(ReplayCommand x, Stateid.dummy); next=n}
- | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
+ | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id^"."))
with Not_found -> raise Expired
end (* }}} *)
@@ -474,10 +474,12 @@ end = struct (* {{{ *)
vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
- (match x with
+ (let rec aux x = match x with
| VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
| VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i
- | _ -> "branch")
+ | VernacTime (_, e)
+ | VernacTimeout (_, e) -> aux e
+ | _ -> "branch" in aux x)
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
let get_info id =
@@ -500,7 +502,7 @@ end = struct (* {{{ *)
if List.mem edit_branch (Vcs_.branches !vcs) then begin
checkout edit_branch;
match get_branch edit_branch with
- | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode
+ | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
| _ -> assert false
end else
let pl = proof_nesting () in
@@ -509,10 +511,10 @@ end = struct (* {{{ *)
| h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
checkout branch;
stm_prerr_endline (fun () -> "mode:" ^ mode);
- Proof_global.activate_proof_mode mode
+ Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
with Failure _ ->
checkout Branch.master;
- Proof_global.disactivate_current_proof_mode ()
+ Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"]
(* copies the transaction on every open branch *)
let propagate_sideff ~action =
@@ -533,7 +535,7 @@ end = struct (* {{{ *)
| { next = n; step = `Sideff (ReplayCommand x,_) } ->
(id,Sideff (ReplayCommand x)) :: aux n
| _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^
- " to "^Stateid.to_string block_stop))
+ " to "^Stateid.to_string block_stop^"."))
in aux block_stop
let slice ~block_start ~block_stop =
@@ -585,11 +587,11 @@ end = struct (* {{{ *)
l
let create_proof_task_box l ~qed ~block_start:lemma =
- if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes");
+ if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes.");
vcs := create_property !vcs l (ProofTask { qed; lemma })
let create_proof_block ({ block_start; block_stop} as decl) name =
let l = nodes_in_slice ~block_start ~block_stop in
- if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes");
+ if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes.");
vcs := create_property !vcs l (ProofBlock (decl, name))
let box_of id = List.map Dag.Property.data (property_of !vcs id)
let delete_boxes_of id =
@@ -600,7 +602,7 @@ end = struct (* {{{ *)
with
| [] -> None
| [x] -> Some x
- | _ -> anomaly Pp.(str "node with more than 1 proof task box")
+ | _ -> anomaly Pp.(str "node with more than 1 proof task box.")
let gc () =
let old_vcs = !vcs in
@@ -764,13 +766,13 @@ end = struct (* {{{ *)
| _ ->
(* coqc has a 1 slot cache and only for valid states *)
if interactive () = `No && Stateid.equal id !cur_id then ()
- else anomaly Pp.(str "installing a non cached state")
+ else anomaly Pp.(str "installing a non cached state.")
let get_cached id =
try match VCS.get_info id with
| { state = Valid s } -> s
- | _ -> anomaly Pp.(str "not a cached state")
- with VCS.Expired -> anomaly Pp.(str "not a cached state (expired)")
+ | _ -> anomaly Pp.(str "not a cached state.")
+ with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).")
let assign id what =
if VCS.get_state id <> Empty then () else
@@ -821,7 +823,7 @@ end = struct (* {{{ *)
feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
let str_id = Stateid.to_string id in
if is_cached id && not redefine then
- anomaly Pp.(str"defining state "++str str_id++str" twice");
+ anomaly Pp.(str"defining state "++str str_id++str" twice.");
try
stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
@@ -929,7 +931,7 @@ let show_script ?proof () =
try
let prf =
try match proof with
- | None -> Some (Pfedit.get_current_proof_name ())
+ | None -> Some (Proof_global.get_current_proof_name ())
| Some (p,_) -> Some (p.Proof_global.id)
with Proof_global.NoCurrentProof -> None
in
@@ -1013,7 +1015,7 @@ end = struct (* {{{ *)
match info.vcs_backup with
| None, _ ->
anomaly Pp.(str"Backtrack.backto "++str(Stateid.to_string oid)++
- str": a state with no vcs_backup")
+ str": a state with no vcs_backup.")
| Some vcs, _ -> VCS.restore vcs
let branches_of id =
@@ -1021,7 +1023,7 @@ end = struct (* {{{ *)
match info.vcs_backup with
| _, None ->
anomaly Pp.(str"Backtrack.branches_of "++str(Stateid.to_string id)++
- str": a state with no vcs_backup")
+ str": a state with no vcs_backup.")
| _, Some x -> x
let rec fold_until f acc id =
@@ -1075,7 +1077,7 @@ end = struct (* {{{ *)
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let vcs =
match (VCS.get_info id).vcs_backup with
- | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup")
+ | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.")
| Some vcs, _ -> vcs in
let cb, _ =
try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
@@ -1834,11 +1836,11 @@ end = struct (* {{{ *)
1 goals in
TaskQueue.join queue;
let assign_tac : unit Proofview.tactic =
- Proofview.(Goal.nf_enter { Goal.enter = fun g ->
+ Proofview.(Goal.nf_enter begin fun g ->
let gid = Goal.goal g in
let f =
try List.assoc gid res
- with Not_found -> CErrors.anomaly(str"Partac: wrong focus") in
+ with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in
if not (Future.is_over f) then
(* One has failed and cancelled the others, but not this one *)
if solve then Tacticals.New.tclZEROMSG
@@ -1857,7 +1859,7 @@ end = struct (* {{{ *)
Tactics.exact_no_check (EConstr.of_constr pt))
with TacTask.NoProgress ->
if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
- })
+ end)
in
Proof.run_tactic (Global.env()) assign_tac p)))) ())
@@ -2044,7 +2046,8 @@ let collect_proof keep cur hd brkind id =
| `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in
let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
match cur, (VCS.visit id).step, brkind with
- | (parent, { expr = VernacExactProof _ }), `Fork _, _ ->
+ | (parent, { expr = VernacExactProof _ }), `Fork _, _
+ | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ ->
`Sync (no_name,None,`Immediate)
| _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id)
| _ ->
@@ -2106,12 +2109,11 @@ let known_state ?(redefine_qed=false) ~cache id =
| `Leaks -> Exninfo.iraise exn
| `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
let tac =
- let open Proofview.Notations in
- Proofview.Goal.nf_enter { enter = fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
if CList.mem_f Evar.equal
(Proofview.Goal.goal gl) goals_to_admit then
Proofview.give_up else Proofview.tclUNIT ()
- } in
+ end in
match (VCS.get_info base_state).state with
| Valid { proof } ->
Proof_global.unfreeze proof;
@@ -2367,8 +2369,8 @@ let finish () =
hides true bugs cf bug #5363. Also, what happens with observe? *)
(* Some commands may by side effect change the proof mode *)
match VCS.get_branch head with
- | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
- | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
+ | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
+ | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
| _ -> ()
let wait () =
@@ -2455,7 +2457,7 @@ let handle_failure (e, info) vcs =
VCS.restore vcs;
VCS.print ();
anomaly(str"error with no safe_id attached:" ++ spc() ++
- CErrors.iprint_no_report (e, info))
+ CErrors.iprint_no_report (e, info) ++ str".")
| Some (safe_id, id) ->
stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
@@ -2487,7 +2489,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
| VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
| VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok
| VtStm ((VtJoinDocument|VtWait),_), VtLater ->
- anomaly(str"classifier: join actions cannot be classified as VtLater")
+ anomaly(str"classifier: join actions cannot be classified as VtLater.")
(* Back *)
| VtStm (VtBack oid, true), w ->
@@ -2515,7 +2517,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.checkout_shallowest_proof_branch ();
Reach.known_state ~cache:(interactive ()) id; `Ok
| VtStm (VtBack id, false), VtLater ->
- anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
+ anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
(* Query *)
| VtQuery (false,(report_id,route)), VtNow ->
@@ -2536,7 +2538,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.commit id (mkTransCmd x [] false queue);
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQuery (false,_), VtLater ->
- anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
+ anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
(* Proof *)
| VtStartProof (mode, guarantee, names), w ->
@@ -2550,10 +2552,10 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
end;
- Proof_global.activate_proof_mode mode;
+ Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtProofMode _, VtLater ->
- anomaly(str"VtProofMode must be executed VtNow")
+ anomaly(str"VtProofMode must be executed VtNow.")
| VtProofMode mode, VtNow ->
let id = VCS.new_node ~id:newtip () in
VCS.commit id (mkTransCmd x [] false `MainQueue);
@@ -2631,7 +2633,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[]));
let proof_mode = default_proof_mode () in
VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
- Proof_global.activate_proof_mode proof_mode;
+ Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
end else begin
VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
(* We hope it can be replayed, but we can't really know *)
@@ -2642,7 +2644,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
Backtrack.record (); `Ok
| VtUnknown, VtLater ->
- anomaly(str"classifier: VtUnknown must imply VtNow")
+ anomaly(str"classifier: VtUnknown 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 ")"])
@@ -2781,7 +2783,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
s
let edit_at id =
- if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy") else
+ if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else
let vcs = VCS.backup () in
let on_cur_branch id =
let rec aux cur =
@@ -2820,7 +2822,7 @@ let edit_at id =
(* Hum, this should be the real start_id in the cluster and not next *)
match VCS.visit qed_id with
| { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
- | _ -> anomaly (str "ProofTask not ending with Qed") in
+ | _ -> anomaly (str "ProofTask not ending with Qed.") in
VCS.branch ~root:master_id ~pos:id
VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
VCS.delete_boxes_of id;
@@ -2872,7 +2874,7 @@ let edit_at id =
end else if is_ancestor_of_cur_branch id then begin
backto id (Some bn)
end else begin
- anomaly(str"Cannot leave an `Edit branch open")
+ anomaly(str"Cannot leave an `Edit branch open.")
end
| true, None, _ ->
if on_cur_branch id then begin
@@ -2883,7 +2885,7 @@ let edit_at id =
end else if is_ancestor_of_cur_branch id then begin
backto id None
end else begin
- anomaly(str"Cannot leave an `Edit branch open")
+ anomaly(str"Cannot leave an `Edit branch open.")
end
| false, None, Some(_,bn) -> backto id (Some bn)
| false, None, None -> backto id None
@@ -2896,7 +2898,7 @@ let edit_at id =
| None ->
VCS.print ();
anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
- CErrors.print_no_report e)
+ CErrors.print_no_report e ++ str ".")
| Some (_, id) ->
stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index a0b08778ba..fee4f35b49 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -88,7 +88,7 @@ let broadcast { lock = m; cond = c } =
let push { queue = q; lock = m; cond = c; release } x =
if release then CErrors.anomaly(Pp.str
- "TQueue.push while being destroyed! Only 1 producer/destroyer allowed");
+ "TQueue.push while being destroyed! Only 1 producer/destroyer allowed.");
Mutex.lock m;
PriorityQueue.push q x;
Condition.broadcast c;
diff --git a/stm/vcs.ml b/stm/vcs.ml
index 88f860eb69..df3b8aa621 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -113,7 +113,7 @@ let add_node vcs id edges =
let get_branch vcs head =
try BranchMap.find head vcs.heads
- with Not_found -> anomaly (str"head " ++ str head ++ str" not found")
+ with Not_found -> anomaly (str"head " ++ str head ++ str" not found.")
let reset_branch vcs head id =
let map name h =
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c4f392f201..471e05e458 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -10,7 +10,7 @@ open Vernacexpr
open CErrors
open Pp
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
let string_of_in_script b = if b then " (inside script)" else ""
@@ -206,7 +206,7 @@ let rec classify_vernac e =
(* Plugins should classify their commands *)
| VernacExtend (s,l) ->
try List.assoc s !classifiers l ()
- with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
+ with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
let res = static_classifier e in
if Flags.is_universe_polymorphism () then
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:52:13 +0000