aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/proofBlockDelimiter.ml24
-rw-r--r--stm/stm.ml98
-rw-r--r--stm/stm.mli6
-rw-r--r--stm/vernac_classifier.ml21
-rw-r--r--stm/vio_checking.ml3
5 files changed, 80 insertions, 72 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 129444c3b3..a487799b74 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -77,17 +77,18 @@ include Util
(* ****************** - foo - bar - baz *********************************** *)
let static_bullet ({ entry_point; prev_node } as view) =
+ let open Vernacexpr in
assert (not (Vernacprop.has_Fail entry_point.ast));
- match Vernacprop.under_control entry_point.ast with
- | Vernacexpr.VernacBullet b ->
+ match entry_point.ast.CAst.v.expr with
+ | VernacBullet b ->
let base = entry_point.indentation in
let last_tac = prev_node entry_point in
crawl view ~init:last_tac (fun prev node ->
if node.indentation < base then `Stop else
if node.indentation > base then `Cont node else
if Vernacprop.has_Fail node.ast then `Stop
- else match Vernacprop.under_control node.ast with
- | Vernacexpr.VernacBullet b' when b = b' ->
+ else match node.ast.CAst.v.expr with
+ | VernacBullet b' when b = b' ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = of_bullet_val b }
| _ -> `Stop) entry_point
@@ -99,7 +100,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
+ recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacBullet (to_bullet_val b)})
}
| `Not -> `Leaks
@@ -109,16 +110,17 @@ let () = register_proof_block_delimiter
(* ******************** { block } ***************************************** *)
let static_curly_brace ({ entry_point; prev_node } as view) =
- assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
+ let open Vernacexpr in
+ assert(entry_point.ast.CAst.v.expr = VernacEndSubproof);
crawl view (fun (nesting,prev) node ->
if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
- else match Vernacprop.under_control node.ast with
- | Vernacexpr.VernacSubproof _ when nesting = 0 ->
+ else match node.ast.CAst.v.expr with
+ | VernacSubproof _ when nesting = 0 ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = unit_val }
- | Vernacexpr.VernacSubproof _ ->
+ | VernacSubproof _ ->
`Cont (nesting - 1,node)
- | Vernacexpr.VernacEndSubproof ->
+ | VernacEndSubproof ->
`Cont (nesting + 1,node)
| _ -> `Cont (nesting,node)) (-1, entry_point)
@@ -128,7 +130,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
+ recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacEndSubproof })
}
| `Not -> `Leaks
diff --git a/stm/stm.ml b/stm/stm.ml
index 69dbebbc57..c399b69a77 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -571,7 +571,7 @@ 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 Vernacprop.under_control x with
+ (match x.CAst.v.Vernacexpr.expr 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
@@ -1054,9 +1054,9 @@ end = struct (* {{{ *)
end (* }}} *)
(* Wrapper for the proof-closing special path for Qed *)
-let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc pending : Vernacstate.t =
+let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t =
set_id_for_feedback ?route dummy_doc id;
- Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc pending
+ Vernacinterp.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending)
(* Wrapper for Vernacentries.interp to set the feedback id *)
(* It is currently called 19 times, this number should be certainly
@@ -1078,12 +1078,12 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t =
| _ -> false
in
(* XXX unsupported attributes *)
- let cmd = Vernacprop.under_control expr in
+ let cmd = expr.CAst.v.expr in
if is_filtered_command cmd then
(stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
else begin
stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
- Vernacentries.interp ?verbosely:(Some verbose) ~st expr
+ Vernacinterp.interp ?verbosely:(Some verbose) ~st expr
end
(****************************** CRUFT *****************************************)
@@ -1141,7 +1141,7 @@ end = struct (* {{{ *)
| { step = `Fork ((_,_,_,l),_) } -> l, false,0
| { step = `Cmd { cids = l; ctac } } -> l, ctac,0
| { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) ->
- begin match Vernacprop.under_control expr with
+ begin match expr.CAst.v.expr with
| VernacUndo n -> [], false, n
| _ -> [],false,0
end
@@ -1171,7 +1171,7 @@ end = struct (* {{{ *)
if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force
then undo_costly_in_batch_mode v;
try
- match Vernacprop.under_control v with
+ match v.CAst.v.expr with
| VernacResetInitial ->
Stateid.initial
| VernacResetName {CAst.v=name} ->
@@ -1532,7 +1532,7 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_qed_delay_proof ~st ~id:stop
- ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc (Proved (opaque,None))) in
+ ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in
ignore(Future.join checked_proof);
end;
(* STATE: Restore the state XXX: handle exn *)
@@ -1683,7 +1683,7 @@ end = struct (* {{{ *)
*)
(* STATE We use the state resulting from reaching start. *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc (Proved (opaque,None)));
+ ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None)));
`OK proof
end
with e ->
@@ -1743,9 +1743,9 @@ end = struct (* {{{ *)
assert (Univ.ContextSet.is_empty uctx)
in
let pr = Constr.hcons pr in
- let (ci, dummy) = p.(bucket) in
+ let dummy = p.(bucket) in
let () = assert (Option.is_empty dummy) in
- p.(bucket) <- ci, Some (pr, priv);
+ p.(bucket) <- Some (pr, priv);
Univ.ContextSet.union cst uc, false
let check_task name l i =
@@ -1970,20 +1970,21 @@ end = struct (* {{{ *)
let stm_fail ~st fail f =
if fail then
- Vernacentries.with_fail ~st f
+ Vernacinterp.with_fail ~st f
else
f ()
let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id
{ indentation; verbose; expr = e; strlen } : unit
=
- let e, time, batch, fail =
- 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 cl, time, batch, fail =
+ let rec find ~time ~batch ~fail cl = match cl with
+ | ControlTime batch :: cl -> find ~time:true ~batch ~fail cl
+ | ControlRedirect _ :: cl -> find ~time ~batch ~fail cl
+ | ControlFail :: cl -> find ~time ~batch ~fail:true cl
+ | cl -> cl, time, batch, fail in
+ find ~time:false ~batch:false ~fail:false e.CAst.v.control in
+ let e = CAst.map (fun cmd -> { cmd with control = cl }) e in
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 () ->
@@ -2151,14 +2152,14 @@ let collect_proof keep cur hd brkind id =
| VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
| _ -> false in
let is_defined = function
- | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
+ | _, { expr = e } -> is_defined_expr e.CAst.v.expr
&& (not (Vernacprop.has_Fail e)) in
let proof_using_ast = function
| VernacProof(_,Some _) -> true
| _ -> false
in
let proof_using_ast = function
- | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr)
+ | Some (_, v) when proof_using_ast v.expr.CAst.v.expr
&& (not (Vernacprop.has_Fail v.expr)) -> Some v
| _ -> None in
let has_proof_using x = proof_using_ast x <> None in
@@ -2167,14 +2168,14 @@ let collect_proof keep cur hd brkind id =
| _ -> assert false
in
let proof_no_using = function
- | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v
+ | Some (_, v) -> proof_no_using v.expr.CAst.v.expr, v
| _ -> assert false in
let has_proof_no_using = function
| VernacProof(_,None) -> true
| _ -> false
in
let has_proof_no_using = function
- | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr)
+ | Some (_, v) -> has_proof_no_using v.expr.CAst.v.expr
&& (not (Vernacprop.has_Fail v.expr))
| _ -> false in
let too_complex_to_delegate = function
@@ -2191,7 +2192,7 @@ let collect_proof keep cur hd brkind id =
let view = VCS.visit id in
match view.step with
| (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
- when too_complex_to_delegate (Vernacprop.under_control x.expr) ->
+ when too_complex_to_delegate x.expr.CAst.v.expr ->
`Sync(no_name,`Print)
| `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
| `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
@@ -2212,7 +2213,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 <- CAst.map (fun _ -> VernacExpr([], VernacProof(t, Some hint))) v.expr;
+ v.expr <- CAst.map (fun _ -> { control = []; attrs = []; expr = VernacProof(t, Some hint)}) v.expr;
`ASync (parent last,accn,name,delegate name)
with Not_found ->
let name = name ids in
@@ -2235,7 +2236,7 @@ let collect_proof keep cur hd brkind id =
| _ -> false
in
match cur, (VCS.visit id).step, brkind with
- | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr)
+ | (parent, x), `Fork _, _ when is_vernac_exact x.expr.CAst.v.expr
&& (not (Vernacprop.has_Fail x.expr)) ->
`Sync (no_name,`Immediate)
| _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id)
@@ -2350,8 +2351,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
term.` could also fail in this case, however that'd be a bug I do
believe as proof injection shouldn't happen here. *)
let extract_pe (x : aast) =
- match Vernacprop.under_control x.expr with
- | VernacEndProof pe -> pe
+ match x.expr.CAst.v.expr with
+ | VernacEndProof pe -> x.expr.CAst.v.control, pe
| _ -> CErrors.anomaly Pp.(str "Non-qed command classified incorrectly") in
(* ugly functions to process nested lemmas, i.e. hard to reproduce
@@ -2486,7 +2487,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
if not delegate then ignore(Future.compute fp);
reach view.next;
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x));
+ let control, pe = extract_pe x in
+ ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe);
feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
@@ -2526,7 +2528,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
let _st = match proof with
| None -> stm_vernac_interp id st x
| Some (proof, info) ->
- stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x)
+ let control, pe = extract_pe x in
+ stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe
in
let wall_clock3 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
@@ -2614,13 +2617,10 @@ let dirpath_of_file f =
let new_doc { doc_type ; iload_path; require_libs; stm_options } =
- let load_objs libs =
- let rq_file (dir, from, exp) =
- let mp = Libnames.qualid_of_string dir in
- let mfrom = Option.map Libnames.qualid_of_string from in
- Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
- List.(iter rq_file (rev libs))
- in
+ let require_file (dir, from, exp) =
+ let mp = Libnames.qualid_of_string dir in
+ let mfrom = Option.map Libnames.qualid_of_string from in
+ Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
(* Set the options from the new documents *)
AsyncOpts.cur_opt := stm_options;
@@ -2659,7 +2659,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
end;
(* Import initial libraries. *)
- load_objs require_libs;
+ List.iter require_file require_libs;
(* We record the state at this point! *)
State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
@@ -2801,13 +2801,21 @@ let handle_failure (e, info) vcs =
VCS.print ();
Exninfo.iraise (e, info)
-let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo =
+let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo =
let doc = finish ~doc in
if List.length (VCS.branches ()) > 1 then
CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
- Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects
- ldir long_f_dot_vo
- (Global.opaque_tables ());
+ (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers,
+ below, [snapshot] gets computed even if [create_vos] is true. *)
+ let (tasks,counters) = dump_snapshot() in
+ let except = List.fold_left (fun e (r,_) ->
+ Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in
+ let todo_proofs =
+ if create_vos
+ then Library.ProofsTodoSomeEmpty except
+ else Library.ProofsTodoSome (except,tasks,counters)
+ in
+ Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
doc
let reset_task_queue = Slaves.reset_task_queue
@@ -2873,7 +2881,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
let queue =
if VCS.is_vio_doc () &&
VCS.((get_branch head).kind = `Master) &&
- may_pierce_opaque (Vernacprop.under_control x.expr)
+ may_pierce_opaque x.expr.CAst.v.expr
then `SkipQueue
else `MainQueue in
VCS.commit id (mkTransCmd x [] false queue);
@@ -2891,7 +2899,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
|> Exninfo.iraise
else
- let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in
+ let proof_mode = Some (Vernacinterp.get_default_proof_mode ()) in
let id = VCS.new_node ~id:newtip proof_mode () in
let bname = VCS.mk_branch_name x in
VCS.checkout VCS.Branch.master;
@@ -2939,7 +2947,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
VCS.commit id (mkTransCmd x l true `MainQueue);
(* We can't replay a Definition since universes may be differently
* inferred. This holds in Coq >= 8.5 *)
- let action = match Vernacprop.under_control x.expr with
+ let action = match x.expr.CAst.v.expr with
| VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
| _ -> ReplayCommand x in
VCS.propagate_sideff ~action
diff --git a/stm/stm.mli b/stm/stm.mli
index 29e4b02e3f..841adcf05b 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -159,8 +159,10 @@ val join : doc:doc -> doc
- if the worker pool is empty, all tasks are saved
- if the worker proof is not empty, then it waits until all workers
are done with their current jobs and then dumps (or fails if one
- of the completed tasks is a failure) *)
-val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
+ of the completed tasks is a failure).
+ Note: the create_vos argument is used in the "-vos" mode, where the
+ proof tasks are not dumped into the output file. *)
+val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
(* Empties the task queue, can be used only if the worker pool is empty (E.g.
* after having built a .vio in batch mode *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 5af576dad2..24976d8c1f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -51,7 +51,7 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
let options_affecting_stm_scheduling =
[ Attributes.universe_polymorphism_option_name;
stm_allow_nested_proofs_option_name;
- Vernacentries.proof_mode_opt_name;
+ Vernacinterp.proof_mode_opt_name;
Attributes.program_mode_option_name;
Proof_using.proof_using_opt_name;
]
@@ -202,18 +202,17 @@ 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 v = v |> CAst.with_val (function
- | VernacExpr (atts, e) ->
- static_classifier ~atts e
- | VernacTimeout (_,e) -> static_control_classifier e
- | VernacTime (_,e) | VernacRedirect (_, e) ->
- static_control_classifier e
- | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
- (* XXX why is Fail not always Query? *)
- (match static_control_classifier e with
+ let static_control_classifier ({ CAst.v ; _ } as cmd) =
+ (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ (* XXX why is Fail not always Query? *)
+ if Vernacprop.has_Fail cmd then
+ (match static_classifier ~atts:v.attrs v.expr with
| VtQuery | VtProofStep _ | VtSideff _
| VtMeta as x -> x
| VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None }
- | VtStartProof _ | VtProofMode _ -> VtQuery))
+ | VtStartProof _ | VtProofMode _ -> VtQuery)
+ else
+ static_classifier ~atts:v.attrs v.expr
+
in
static_control_classifier e
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index fab6767beb..baa7b3570c 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -11,7 +11,6 @@
open Util
let check_vio (ts,f_in) =
- Dumpglob.noglob ();
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
@@ -142,5 +141,3 @@ let schedule_vio_compilation j fs =
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-05-04 09:58:58 +0000