summaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/lemmas.ml67
-rw-r--r--stm/lemmas.mli3
-rw-r--r--stm/spawned.ml19
-rw-r--r--stm/spawned.mli2
-rw-r--r--stm/stm.ml191
-rw-r--r--stm/stm.mli17
-rw-r--r--stm/tQueue.ml20
-rw-r--r--stm/tQueue.mli3
-rw-r--r--stm/texmacspp.ml24
-rw-r--r--stm/vernac_classifier.ml24
-rw-r--r--stm/vio_checking.ml8
11 files changed, 234 insertions, 144 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6cece32e..6c183268 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -70,11 +70,12 @@ let adjust_guardness_conditions const = function
try ignore(Environ.lookup_constant c e); true
with Not_found -> false in
if exists c e then e else Environ.add_constant c cb e in
- let env = Declareops.fold_side_effects (fun env -> function
+ let env = List.fold_left (fun env { eff } ->
+ match eff with
| SEsubproof (c, cb,_) -> add c cb env
| SEscheme (l,_) ->
List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
- env (Declareops.uniquize_side_effects eff) in
+ env (Safe_typing.side_effects_of_private_constants eff) in
let indexes =
search_guard Loc.ghost env
possible_indexes fixdecls in
@@ -212,7 +213,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
let default_thm_id = Id.of_string "Unnamed_thm"
let compute_proof_name locality = function
- | Some (loc,id) ->
+ | Some ((loc,id),pl) ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
@@ -326,29 +327,10 @@ let check_exist =
user_err_loc (loc,"",pr_id id ++ str " does not exist.")
)
-let standard_proof_terminator compute_guard hook =
- let open Proof_global in function
- | Admitted (id,k,pe) ->
- admit (id,k,pe) hook ();
- Pp.feedback Feedback.AddedAxiom
- | Proved (opaque,idopt,proof) ->
- let is_opaque, export_seff, exports = match opaque with
- | Vernacexpr.Transparent -> false, true, []
- | Vernacexpr.Opaque None -> true, false, []
- | Vernacexpr.Opaque (Some l) -> true, true, l in
- let proof = get_proof proof compute_guard hook is_opaque in
- begin match idopt with
- | None -> save_named ~export_seff proof
- | Some ((_,id),None) -> save_anonymous ~export_seff proof id
- | Some ((_,id),Some kind) ->
- save_anonymous_with_strength ~export_seff proof kind id
- end;
- check_exist exports
-
let universe_proof_terminator compute_guard hook =
let open Proof_global in function
- | Admitted (id,k,pe) ->
- admit (id,k,pe) (hook None) ();
+ | Admitted (id,k,pe,ctx) ->
+ admit (id,k,pe) (hook (Some ctx)) ();
Pp.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff, exports = match opaque with
@@ -365,6 +347,9 @@ let universe_proof_terminator compute_guard hook =
end;
check_exist exports
+let standard_proof_terminator compute_guard hook =
+ universe_proof_terminator compute_guard (fun _ -> hook)
+
let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
let terminator = standard_proof_terminator compute_guard hook in
let sign =
@@ -436,7 +421,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let body,opaq = retrieve_first_recthm ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = Evd.evar_universe_context_set ctx in
+ let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in
let body = Option.map norm body in
List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
@@ -447,11 +432,15 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let start_proof_com kind thms hook =
let env0 = Global.env () in
- let evdref = ref (Evd.from_env env0) in
+ let levels = Option.map snd (fst (List.hd thms)) in
+ let evdref = ref (match levels with
+ | None -> Evd.from_env env0
+ | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
+ in
let thms = List.map (fun (sopt,(bl,t,guard)) ->
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
- check_evars_are_solved env !evdref (Evd.empty,!evdref);
+ evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
let ids = List.map pi1 ctx in
(compute_proof_name (pi1 kind) sopt,
(nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
@@ -461,8 +450,12 @@ let start_proof_com kind thms hook =
let recguard,thms,snl = look_for_possibly_mutual_statements thms in
let evd, nf = Evarutil.nf_evars_and_universes !evdref in
let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
- start_proof_with_initialization kind evd
- recguard thms snl hook
+ let evd =
+ if pi2 kind then evd
+ else (* We fix the variables to ensure they won't be lowered to Set *)
+ Evd.fix_undefined_variables evd
+ in
+ start_proof_with_initialization kind evd recguard thms snl hook
(* Saving a proof *)
@@ -480,14 +473,13 @@ let save_proof ?proof = function
error "Admitted requires an explicit statement";
let typ = Option.get const_entry_type in
let ctx = Evd.evar_context_universe_context universes in
- Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None))
+ Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
| None ->
let id, k, typ = Pfedit.current_proof_statement () in
- let ctx =
- let evd, _ = Pfedit.get_current_goal_context () in
- Evd.universe_context evd in
(* This will warn if the proof is complete *)
- let pproofs,_ = Proof_global.return_proof ~allow_partial:true () in
+ let pproofs, universes =
+ Proof_global.return_proof ~allow_partial:true () in
+ let ctx = Evd.evar_context_universe_context universes in
let sec_vars =
match Pfedit.get_used_variables(), pproofs with
| Some _ as x, _ -> x
@@ -497,14 +489,14 @@ let save_proof ?proof = function
let ids_def = Environ.global_vars_set env pproof in
Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
| _ -> None in
- Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None))
+ Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes)
in
Proof_global.get_terminator() pe
| Vernacexpr.Proved (is_opaque,idopt) ->
let (proof_obj,terminator) =
match proof with
| None ->
- Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)
+ Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
| Some proof -> proof
in
(* if the proof is given explicitly, nothing has to be deleted *)
@@ -516,4 +508,5 @@ let save_proof ?proof = function
let get_current_context () =
try Pfedit.get_current_goal_context ()
with e when Logic.catchable_exception e ->
- (Evd.empty, Global.env())
+ let env = Global.env () in
+ (Evd.from_env env, env)
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index a0ddd265..6556aa22 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -32,8 +32,7 @@ val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
(Proof_global.proof_universes option -> unit declaration_hook) -> unit
-val start_proof_com : goal_kind ->
- (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list ->
+val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
unit declaration_hook -> unit
val start_proof_with_initialization :
diff --git a/stm/spawned.ml b/stm/spawned.ml
index a8372195..66fe07db 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -11,7 +11,7 @@ open Spawn
let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s
let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
-type chandescr = AnonPipe | Socket of string * int
+type chandescr = AnonPipe | Socket of string * int * int
let handshake cin cout =
try
@@ -26,18 +26,19 @@ let handshake cin cout =
| End_of_file ->
pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
-let open_bin_connection h p =
+let open_bin_connection h pr pw =
let open Unix in
- let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in
+ let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
+ let cin, _ = open_connection (ADDR_INET (inet_addr_of_string h,pw)) in
set_binary_mode_in cin true;
set_binary_mode_out cout true;
let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in
cin, cout
-let controller h p =
+let controller h pr pw =
prerr_endline "starting controller thread";
let main () =
- let ic, oc = open_bin_connection h p in
+ let ic, oc = open_bin_connection h pr pw in
let rec loop () =
try
match CThread.thread_friendly_input_value ic with
@@ -61,8 +62,8 @@ let init_channels () =
if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
let () = match !main_channel with
| None -> ()
- | Some (Socket(mh,mp)) ->
- channels := Some (open_bin_connection mh mp);
+ | Some (Socket(mh,mpr,mpw)) ->
+ channels := Some (open_bin_connection mh mpr mpw);
| Some AnonPipe ->
let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in
let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in
@@ -74,8 +75,8 @@ let init_channels () =
in
match !control_channel with
| None -> ()
- | Some (Socket (ch, cp)) ->
- controller ch cp
+ | Some (Socket (ch, cpr, cpw)) ->
+ controller ch cpr cpw
| Some AnonPipe ->
Errors.anomaly (Pp.str "control channel cannot be a pipe")
diff --git a/stm/spawned.mli b/stm/spawned.mli
index d9e7baff..d0183e08 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -8,7 +8,7 @@
(* To link this file, threads are needed *)
-type chandescr = AnonPipe | Socket of string * int
+type chandescr = AnonPipe | Socket of string * int * int
(* Argument parsing should set these *)
val main_channel : chandescr option ref
diff --git a/stm/stm.ml b/stm/stm.ml
index 38745e22..14142aa0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -51,7 +51,7 @@ let execution_error, execution_error_hook = Hook.make
feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
let unreachable_state, unreachable_state_hook = Hook.make
- ~default:(fun _ -> ()) ()
+ ~default:(fun _ _ -> ()) ()
include Hook
@@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
| VernacResetName _ | VernacResetInitial | VernacBack _
| VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
| VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
- | VernacTime el -> List.for_all (fun (_,e) -> internal_command e) el
+ | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
| _ -> false in
if internal_command expr then begin
prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
@@ -123,6 +123,10 @@ let pr_open_cur_subgoals () =
try Printer.pr_open_subgoals ()
with Proof_global.NoCurrentProof -> str""
+let update_global_env () =
+ if Proof_global.there_are_pending_proofs () then
+ Proof_global.update_global_env ()
+
module Vcs_ = Vcs.Make(Stateid)
type future_proof = Proof_global.closed_proof_output Future.computation
type proof_mode = string
@@ -131,9 +135,11 @@ type cancel_switch = bool ref
type branch_type =
[ `Master
| `Proof of proof_mode * depth
- | `Edit of proof_mode * Stateid.t * Stateid.t * vernac_qed_type ]
+ | `Edit of
+ proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ]
type cmd_t = {
ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
+ ceff : bool; (* is a side-effecting command *)
cast : ast;
cids : Id.t list;
cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
@@ -371,7 +377,7 @@ end = struct (* {{{ *)
(try let n = Hashtbl.find clus c in from::n
with Not_found -> [from]); true in
let oc = open_out fname_dot in
- output_string oc "digraph states {\nsplines=ortho\n";
+ output_string oc "digraph states {\n";
Dag.iter graph (fun from cf _ l ->
let c1 = add_to_clus_or_ids from cf in
List.iter (fun (dest, trans) ->
@@ -423,8 +429,8 @@ end = struct (* {{{ *)
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
(match x with
- | VernacDefinition (_,(_,i),_) -> string_of_id i
- | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i
+ | VernacDefinition (_,((_,i),_),_) -> string_of_id i
+ | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
| _ -> "branch")
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -449,7 +455,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
| _ -> assert false
end else
let pl = proof_nesting () in
@@ -590,6 +596,7 @@ module State : sig
?safe_id:Stateid.t ->
?redefine:bool -> ?cache:Summary.marshallable ->
?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
+ val fix_exn_ref : (iexn -> iexn) ref
val install_cached : Stateid.t -> unit
val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
@@ -613,6 +620,7 @@ end = struct (* {{{ *)
(* cur_id holds Stateid.dummy in case the last attempt to define a state
* failed, so the global state may contain garbage *)
let cur_id = ref Stateid.dummy
+ let fix_exn_ref = ref (fun x -> x)
(* helpers *)
let freeze_global_state marshallable =
@@ -638,7 +646,7 @@ end = struct (* {{{ *)
proof,
Summary.project_summary (States.summary_of_state system) summary_pstate
- let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
+ let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
let is_cached ?(cache=`No) id =
if Stateid.equal id !cur_id then
@@ -670,11 +678,22 @@ end = struct (* {{{ *)
let assign id what =
if VCS.get_state id <> None then () else
try match what with
- | `Full s -> VCS.set_state id s
+ | `Full s ->
+ let s =
+ try
+ let prev = (VCS.visit id).next in
+ if is_cached prev
+ then { s with proof =
+ Proof_global.copy_terminators
+ ~src:(get_cached prev).proof ~tgt:s.proof }
+ else s
+ with VCS.Expired -> s in
+ VCS.set_state id s
| `Proof(ontop,(pstate,counters)) ->
if is_cached ontop then
let s = get_cached ontop in
- let s = { s with proof = pstate } in
+ let s = { s with proof =
+ Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
let s = { s with system =
States.replace_summary s.system
(Summary.surgery_summary
@@ -709,7 +728,10 @@ end = struct (* {{{ *)
try
prerr_endline("defining "^str_id^" (cache="^
if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
+ let good_id = match safe_id with None -> !cur_id | Some id -> id in
+ fix_exn_ref := exn_on id ~valid:good_id;
f ();
+ fix_exn_ref := (fun x -> x);
if cache = `Yes then freeze `No id
else if cache = `Shallow then freeze `Shallow id;
prerr_endline ("setting cur id to "^str_id);
@@ -718,13 +740,13 @@ end = struct (* {{{ *)
Hooks.(call state_computed id ~in_cache:false);
VCS.reached id true;
if Proof_global.there_are_pending_proofs () then
- VCS.goals id (Proof_global.get_open_goals ());
+ VCS.goals id (Proof_global.get_open_goals ())
with e ->
let (e, info) = Errors.push e in
let good_id = !cur_id in
cur_id := Stateid.dummy;
VCS.reached id false;
- Hooks.(call unreachable_state id);
+ Hooks.(call unreachable_state id (e, info));
match Stateid.get info, safe_id with
| None, None -> iraise (exn_on id ~valid:good_id (e, info))
| None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
@@ -846,7 +868,8 @@ end = struct (* {{{ *)
| None, _ -> anomaly(str"Backtrack: tip with no vcs_backup")
| Some vcs, _ -> vcs in
let cb, _ =
- Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in
+ try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
+ with Failure _ -> raise Proof_global.NoCurrentProof in
let n = fold_until (fun n (_,vcs,_,_,_) ->
if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
0 id in
@@ -875,9 +898,16 @@ let set_compilation_hints file =
hints := Aux_file.load_aux_file_for file
let get_hint_ctx loc =
let s = Aux_file.get !hints loc "context_used" in
- let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
- let ids = List.map (fun id -> Loc.ghost, id) ids in
- SsExpr (SsSet ids)
+ match Str.split (Str.regexp ";") s with
+ | ids :: _ ->
+ let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
+ let ids = List.map (fun id -> Loc.ghost, id) ids in
+ begin match ids with
+ | [] -> SsEmpty
+ | x :: xs ->
+ List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
+ end
+ | _ -> raise Not_found
let get_hint_bp_time proof_name =
try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
@@ -1117,7 +1147,7 @@ end = struct (* {{{ *)
when is_tac expr && State.same_env o n -> (* A pure tactic *)
Some (id, `Proof (prev, State.proof_part_of_frozen n))
| Some _, Some s ->
- msg_warning (str "Sending back a fat state");
+ msg_warning (str "STM: sending back a fat state");
Some (id, `Full s)
| _, Some s -> Some (id, `Full s) in
let rec aux seen = function
@@ -1207,7 +1237,7 @@ end = struct (* {{{ *)
(Lemmas.standard_proof_terminator []
(Lemmas.mk_hook (fun _ _ -> ())));
let proof =
- Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in
+ Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in
(* We jump at the beginning since the kernel handles side effects by also
* looking at the ones that happen to be present in the current env *)
Reach.known_state ~cache:`No start;
@@ -1472,7 +1502,7 @@ end = struct (* {{{ *)
let e, etac, time, fail =
let rec find time fail = function
| VernacSolve(_,_,re,b) -> re, b, time, fail
- | VernacTime [_,e] -> find true fail e
+ | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e
| VernacFail e -> find time true e
| _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
Hooks.call Hooks.with_fail fail (fun () ->
@@ -1564,7 +1594,8 @@ end = struct (* {{{ *)
vernac_interp r_for { r_what with verbose = true };
feedback ~state_id:r_for Feedback.Processed
with e when Errors.noncritical e ->
- let msg = string_of_ppcmds (print e) in
+ let e = Errors.push e in
+ let msg = string_of_ppcmds (iprint e) in
feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
@@ -1675,7 +1706,10 @@ let collect_proof keep cur hd brkind id =
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
let name = name ids in
`MaybeASync (parent last, None, accn, name, delegate name)
- | `Sideff _ -> `Sync (no_name,None,`NestedProof)
+ | `Sideff _ ->
+ Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^
+ "stop working in the next Coq version")));
+ `Sync (no_name,None,`NestedProof)
| _ -> `Sync (no_name,None,`Unknown) in
let make_sync why = function
| `Sync(name,pua,_) -> `Sync (name,pua,why)
@@ -1729,8 +1763,9 @@ let known_state ?(redefine_qed=false) ~cache id =
let cherry_pick_non_pstate () =
Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
Lib.freeze ~marshallable:`No in
- let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
-
+ let inject_non_pstate (s,l) =
+ Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
+ in
let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
reach id;
@@ -1757,12 +1792,12 @@ let known_state ?(redefine_qed=false) ~cache id =
), cache, true
| `Cmd { cast = x; cqueue = `QueryQueue cancel }
when Flags.async_proofs_is_master () -> (fun () ->
- reach ~cache:`Shallow view.next;
+ reach view.next;
Query.vernac_interp cancel view.next id x
), cache, false
- | `Cmd { cast = x } -> (fun () ->
- reach view.next; vernac_interp id x
- ), cache, true
+ | `Cmd { cast = x; ceff = eff } -> (fun () ->
+ reach view.next; vernac_interp id x;
+ if eff then update_global_env ()), cache, true
| `Fork ((x,_,_,_), None) -> (fun () ->
reach view.next; vernac_interp id x;
wall_clock_last_fork := Unix.gettimeofday ()
@@ -1787,7 +1822,7 @@ let known_state ?(redefine_qed=false) ~cache id =
VCS.create_cluster nodes ~qed:id ~start;
begin match brinfo, qed.fproof with
| { VCS.kind = `Edit _ }, None -> assert false
- | { VCS.kind = `Edit (_,_,_, okeep) }, Some (ofp, cancel) ->
+ | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
assert(redefine_qed = true);
if okeep != keep then
msg_error(strbrk("The command closing the proof changed. "
@@ -1824,7 +1859,6 @@ let known_state ?(redefine_qed=false) ~cache id =
Proof_global.discard_all ()
), (if redefine_qed then `No else `Yes), true
| `Sync (name, _, `Immediate) -> (fun () ->
- assert (Stateid.equal view.next eop);
reach eop; vernac_interp id x; Proof_global.discard_all ()
), `Yes, true
| `Sync (name, pua, reason) -> (fun () ->
@@ -1841,11 +1875,10 @@ let known_state ?(redefine_qed=false) ~cache id =
qed.fproof <- Some (fp, ref false); None
| VtKeep ->
Some(Proof_global.close_proof
- ~keep_body_ucst_sepatate:false
+ ~keep_body_ucst_separate:false
(State.exn_on id ~valid:eop)) in
- reach view.next;
- if keep == VtKeepAsAxiom then
- Option.iter (vernac_interp id) pua;
+ if keep != VtKeepAsAxiom then
+ reach view.next;
let wall_clock2 = Unix.gettimeofday () in
vernac_interp id ?proof x;
let wall_clock3 = Unix.gettimeofday () in
@@ -1863,7 +1896,7 @@ let known_state ?(redefine_qed=false) ~cache id =
in
aux (collect_proof keep (view.next, x) brname brinfo eop)
| `Sideff (`Ast (x,_)) -> (fun () ->
- reach view.next; vernac_interp id x;
+ reach view.next; vernac_interp id x; update_global_env ()
), cache, true
| `Sideff (`Id origin) -> (fun () ->
reach view.next;
@@ -1890,7 +1923,7 @@ let init () =
Backtrack.record ();
Slaves.init ();
if Flags.async_proofs_is_master () then begin
- prerr_endline "Initialising workers";
+ prerr_endline "Initializing workers";
Query.init ();
let opts = match !Flags.async_proofs_private_flags with
| None -> []
@@ -1921,7 +1954,7 @@ let finish ?(print_goals=false) () =
VCS.print ();
(* 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 = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
| { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
| _ -> ()
@@ -1989,7 +2022,7 @@ let merge_proof_branch ?valid ?id qast keep brname =
VCS.delete_branch brname;
if keep <> VtDrop then VCS.propagate_sideff None;
`Ok
- | { VCS.kind = `Edit (mode, qed_id, master_id, _) } ->
+ | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
let ofp =
match VCS.visit qed_id with
| { step = `Qed ({ fproof }, _) } -> fproof
@@ -2018,7 +2051,7 @@ let handle_failure (e, info) vcs tty =
end;
VCS.print ();
anomaly(str"error with no safe_id attached:" ++ spc() ++
- Errors.print_no_report e)
+ Errors.iprint_no_report (e, info))
| Some (safe_id, id) ->
prerr_endline ("Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
@@ -2104,7 +2137,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
iraise (State.exn_on report_id e)); `Ok
| VtQuery (false,(report_id,route)), VtNow ->
(try vernac_interp report_id ~route x
- with e when Errors.noncritical e ->
+ with e ->
let e = Errors.push e in
iraise (State.exn_on report_id e)); `Ok
| VtQuery (true,(report_id,_)), w ->
@@ -2113,7 +2146,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 {ctac=false;cast = x; cids = []; cqueue = queue });
+ VCS.commit id (Cmd {ctac=false;ceff=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")
@@ -2136,16 +2169,16 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
anomaly(str"VtProofMode must be executed VtNow")
| VtProofMode mode, VtNow ->
let id = VCS.new_node ~id:newtip () in
- VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue});
+ VCS.commit id (Cmd {ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
List.iter
(fun bn -> match VCS.get_branch bn with
| { VCS.root; kind = `Master; pos } -> ()
| { VCS.root; kind = `Proof(_,d); pos } ->
VCS.delete_branch bn;
VCS.branch ~root ~pos bn (`Proof(mode,d))
- | { VCS.root; kind = `Edit(_,f,q,k); pos } ->
+ | { VCS.root; kind = `Edit(_,f,q,k,ob); pos } ->
VCS.delete_branch bn;
- VCS.branch ~root ~pos bn (`Edit(mode,f,q,k)))
+ VCS.branch ~root ~pos bn (`Edit(mode,f,q,k,ob)))
(VCS.branches ());
VCS.checkout_shallowest_proof_branch ();
Backtrack.record ();
@@ -2154,7 +2187,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 {ctac = true;cast = x;cids = [];cqueue = queue });
+ VCS.commit id (Cmd {ctac = true;ceff = false;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
@@ -2170,7 +2203,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 {ctac=false;cast=x;cids=l;cqueue=`MainQueue});
+ VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue});
VCS.propagate_sideff (Some x);
VCS.checkout_shallowest_proof_branch ();
Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -2194,7 +2227,8 @@ 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 {ctac=false; cast = x; cids = []; cqueue = `MainQueue});
+ VCS.commit id (Cmd {ctac = false; ceff = true;
+ cast = x; cids = []; cqueue = `MainQueue});
VCS.propagate_sideff (Some x);
VCS.checkout_shallowest_proof_branch ();
end in
@@ -2283,6 +2317,17 @@ let edit_at id =
| { step = `Fork _ } -> false
| { next } -> aux next in
aux (VCS.get_branch_pos (VCS.current_branch ())) in
+ let rec is_pure_aux id =
+ let view = VCS.visit id in
+ match view.step with
+ | `Cmd _ -> is_pure_aux view.next
+ | `Fork _ -> true
+ | _ -> false in
+ let is_pure id =
+ match (VCS.visit id).step with
+ | `Qed (_,last_step) -> is_pure_aux last_step
+ | _ -> assert false
+ in
let is_ancestor_of_cur_branch id =
Vcs_.NodeSet.mem id
(VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in
@@ -2293,24 +2338,27 @@ let edit_at id =
let rec master_for_br root tip =
if Stateid.equal tip Stateid.initial then tip else
match VCS.visit tip with
- | { next } when next = root -> root
- | { step = `Fork _ } -> tip
- | { step = `Sideff (`Ast(_,id)|`Id id) } -> id
+ | { step = (`Fork _ | `Qed _) } -> tip
+ | { step = `Sideff (`Ast(_,id)) } -> id
+ | { step = `Sideff _ } -> tip
| { next } -> master_for_br root next in
- let reopen_branch start at_id mode qed_id tip =
+ let reopen_branch start at_id mode qed_id tip old_branch =
let master_id, cancel_switch, keep =
(* Hum, this should be the real start_id in the clusted and not next *)
match VCS.visit qed_id with
| { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
| _ -> anomaly (str "Cluster not ending with Qed") in
VCS.branch ~root:master_id ~pos:id
- VCS.edit_branch (`Edit (mode, qed_id, master_id, keep));
+ VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
VCS.delete_cluster_of id;
cancel_switch := true;
Reach.known_state ~cache:(interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`Focus { stop = qed_id; start = master_id; tip } in
- let backto id =
+ let no_edit = function
+ | `Edit (pm, _,_,_,_) -> `Proof(pm,1)
+ | x -> x in
+ let backto id bn =
List.iter VCS.delete_branch (VCS.branches ());
let ancestors = VCS.reachable id in
let { mine = brname, brinfo; others } = Backtrack.branches_of id in
@@ -2320,10 +2368,14 @@ let edit_at id =
VCS.branch ~root ~pos name k)
others;
VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id);
- VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos brname brinfo.VCS.kind;
+ VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos
+ (Option.default brname bn)
+ (no_edit brinfo.VCS.kind);
VCS.delete_cluster_of id;
VCS.gc ();
- Reach.known_state ~cache:(interactive ()) id;
+ VCS.print ();
+ if not !Flags.async_proofs_full then
+ Reach.known_state ~cache:(interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`NewTip in
try
@@ -2331,20 +2383,21 @@ let edit_at id =
let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in
let branch_info =
match snd (VCS.get_info id).vcs_backup with
- | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_,_)) }} -> Some m
+ | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn)
+ | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn)
| _ -> None in
match focused, VCS.cluster_of id, branch_info with
| _, Some _, None -> assert false
- | false, Some (qed_id,start), Some mode ->
+ | false, Some (qed_id,start), Some(mode,bn) ->
let tip = VCS.cur_tip () in
- if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch
- then reopen_branch start id mode qed_id tip
- else backto id
- | true, Some (qed_id,_), Some mode ->
+ if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
+ then reopen_branch start id mode qed_id tip bn
+ else backto id (Some bn)
+ | true, Some (qed_id,_), Some(mode,bn) ->
if on_cur_branch id then begin
assert false
end else if is_ancestor_of_cur_branch id then begin
- backto id
+ backto id (Some bn)
end else begin
anomaly(str"Cannot leave an `Edit branch open")
end
@@ -2355,11 +2408,12 @@ let edit_at id =
VCS.checkout_shallowest_proof_branch ();
`NewTip
end else if is_ancestor_of_cur_branch id then begin
- backto id
+ backto id None
end else begin
anomaly(str"Cannot leave an `Edit branch open")
end
- | false, None, _ -> backto id
+ | false, None, Some(_,bn) -> backto id (Some bn)
+ | false, None, None -> backto id None
in
VCS.print ();
rc
@@ -2376,6 +2430,9 @@ let edit_at id =
VCS.print ();
iraise (e, info)
+let backup () = VCS.backup ()
+let restore d = VCS.restore d
+
(*********************** TTY API (PG, coqtop, coqc) ***************************)
(******************************************************************************)
@@ -2430,7 +2487,7 @@ let get_script prf =
let branch, test =
match prf with
| None -> VCS.Branch.master, fun _ -> true
- | Some name -> VCS.current_branch (), List.mem name in
+ | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
let rec find acc id =
if Stateid.equal id Stateid.initial ||
Stateid.equal id Stateid.dummy then acc else
@@ -2441,7 +2498,9 @@ let get_script prf =
| `Sideff (`Ast (x,_)) ->
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
+ | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+ find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+ | `Cmd _ -> find acc view.next
| `Alias (id,_) -> find acc id
| `Fork _ -> find acc view.next
in
@@ -2517,5 +2576,5 @@ let process_error_hook = Hooks.process_error_hook
let interp_hook = Hooks.interp_hook
let with_fail_hook = Hooks.with_fail_hook
let unreachable_state_hook = Hooks.unreachable_state_hook
-
+let get_fix_exn () = !State.fix_exn_ref
(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 1d926e99..0c05c93d 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -35,7 +35,9 @@ val query :
new document tip, the document between [id] and [fo.stop] has been dropped.
The portion between [fo.stop] and [fo.tip] has been kept. [fo.start] is
just to tell the gui where the editing zone starts, in case it wants to
- graphically denote it. All subsequent [add] happen on top of [id]. *)
+ graphically denote it. All subsequent [add] happen on top of [id].
+ If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
+*)
type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
@@ -49,11 +51,11 @@ val stop_worker : string -> unit
(* Joins the entire document. Implies finish, but also checks proofs *)
val join : unit -> unit
-(* Saves on the dist a .vio corresponding to the current status:
- - if the worker prool is empty, all tasks are saved
+(* Saves on the disk a .vio corresponding to the current status:
+ - 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 failuere) *)
+ of the completed tasks is a failure) *)
val snapshot_vio : DirPath.t -> string -> unit
(* Empties the task queue, can be used only if the worker pool is empty (E.g.
@@ -81,6 +83,10 @@ val set_compilation_hints : string -> unit
(* Reorders the task queue putting forward what is in the perspective *)
val set_perspective : Stateid.t list -> unit
+type document
+val backup : unit -> document
+val restore : document -> unit
+
(** workers **************************************************************** **)
module ProofTask : AsyncTaskQueue.Task
@@ -98,7 +104,7 @@ val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
val parse_error_hook :
(Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val unreachable_state_hook : (Stateid.t -> unit) Hook.t
+val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
(* ready means that master has it at hand *)
val state_ready_hook : (Stateid.t -> unit) Hook.t
@@ -130,3 +136,4 @@ val process_error_hook : Future.fix_exn Hook.t
val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
+val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn)
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 6fef895a..2dad962b 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -15,6 +15,7 @@ module PriorityQueue : sig
val pop : ?picky:('a -> bool) -> 'a t -> 'a
val push : 'a t -> 'a -> unit
val clear : 'a t -> unit
+ val length : 'a t -> int
end = struct
type 'a item = int * 'a
type 'a rel = 'a item -> 'a item -> int
@@ -38,6 +39,7 @@ end = struct
let set_rel rel ({ contents = (xs, _) } as t) =
let rel (_,x) (_,y) = rel x y in
t := (List.sort rel xs, rel)
+ let length ({ contents = (l, _) }) = List.length l
end
type 'a t = {
@@ -92,11 +94,29 @@ let push { queue = q; lock = m; cond = c; release } x =
Condition.broadcast c;
Mutex.unlock m
+let length { queue = q; lock = m } =
+ Mutex.lock m;
+ let n = PriorityQueue.length q in
+ Mutex.unlock m;
+ n
+
let clear { queue = q; lock = m; cond = c } =
Mutex.lock m;
PriorityQueue.clear q;
Mutex.unlock m
+let clear_saving { queue = q; lock = m; cond = c } f =
+ Mutex.lock m;
+ let saved = ref [] in
+ while not (PriorityQueue.is_empty q) do
+ let elem = PriorityQueue.pop q in
+ match f elem with
+ | Some x -> saved := x :: !saved
+ | None -> ()
+ done;
+ Mutex.unlock m;
+ List.rev !saved
+
let is_empty { queue = q } = PriorityQueue.is_empty q
let destroy tq =
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 7458de51..1df52d25 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -22,9 +22,12 @@ val broadcast : 'a t -> unit
val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
val clear : 'a t -> unit
+val clear_saving : 'a t -> ('a -> 'b option) -> 'b list
val is_empty : 'a t -> bool
exception BeingDestroyed
(* Threads blocked in pop can get this exception if the queue is being
* destroyed *)
val destroy : 'a t -> unit
+
+val length : 'a t -> int
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 180f20ae..b9120804 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -244,7 +244,7 @@ and pp_local_decl_expr lde = (* don't know what it is for now *)
match lde with
| AssumExpr (_, ce) -> pp_expr ce
| DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, (l, id)), lbl, ceo, _, cl_or_rdexpr) =
+and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
(* inductive_expr *)
let b,e = Loc.unloc l in
let location = ["begin", string_of_int b; "end", string_of_int e] in
@@ -273,7 +273,7 @@ and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
| CMeasureRec (e, None) -> "mesrec", [pp_expr e]
| CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
+and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
(* fixpoint_expr *)
let start, stop = unlock loc in
let id = Id.to_string id in
@@ -286,7 +286,7 @@ and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
| Some ce -> [pp_expr ce]
| None -> []
end
-and pp_cofixpoint_expr ((loc, id), lbl, ce, ceo) = (* cofixpoint_expr *)
+and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
(* Nota: it is like fixpoint_expr without (optid, roe)
* so could be merged if there is no more differences *)
let start, stop = unlock loc in
@@ -473,7 +473,7 @@ and pp_expr ?(attr=[]) e =
xmlApply loc
(xmlOperator "fix" loc ::
List.flatten (List.map
- (fun (a,b,cl,c,d) -> pp_fixpoint_expr (a,b,cl,c,Some d))
+ (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
fel))
let pp_comment (c) =
@@ -490,6 +490,9 @@ let rec tmpp v loc =
| VernacTime l ->
xmlApply loc (Element("time",[],[]) ::
List.map (fun(loc,e) ->tmpp e loc) l)
+ | VernacRedirect (s, l) ->
+ xmlApply loc (Element("redirect",["path", s],[]) ::
+ List.map (fun(loc,e) ->tmpp e loc) l)
| VernacTimeout (s,e) ->
xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
[tmpp e loc])
@@ -506,8 +509,10 @@ let rec tmpp v loc =
| VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
| VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
- | VernacDelimiters (name,tag) ->
+ | VernacDelimiters (name,Some tag) ->
xmlScope loc "delimit" name ~attr:["delimiter",tag] []
+ | VernacDelimiters (name,None) ->
+ xmlScope loc "undelimit" name ~attr:[] []
| VernacBindScope (name,l) ->
xmlScope loc "bind" name
(List.map (function
@@ -535,7 +540,7 @@ let rec tmpp v loc =
| VernacConstraint _
| VernacPolymorphic (_, _) as x -> xmlTODO loc x
(* Gallina *)
- | VernacDefinition (ldk, (_,id), de) ->
+ | VernacDefinition (ldk, ((_,id),_), de) ->
let l, dk =
match ldk with
| Some l, dk -> (l, dk)
@@ -550,7 +555,7 @@ let rec tmpp v loc =
let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
let str_id = Id.to_string id in
(xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some (_,id), ([], statement, None) ], b) ->
+ | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
let str_tk = Kindops.string_of_theorem_kind tk in
let str_id = Id.to_string id in
(xmlThm str_tk str_id loc [pp_expr statement])
@@ -570,10 +575,11 @@ let rec tmpp v loc =
end
| VernacExactProof _ as x -> xmlTODO loc x
| VernacAssumption ((l, a), _, sbwcl) ->
+ let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
let many =
- List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in
+ List.length (List.flatten (List.map fst binders)) > 1 in
let exprs =
- List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in
+ List.flatten (List.map pp_simple_binder binders) in
let l = match l with Some x -> x | None -> Decl_kinds.Global in
let kind = string_of_assumption_kind l a many in
xmlAssumption kind loc exprs
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 783ff2e1..a898c687 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -86,7 +86,7 @@ let rec classify_vernac e =
make_polymorphic (classify_vernac e)
else classify_vernac e
| VernacTimeout (_,e) -> classify_vernac e
- | VernacTime e -> classify_vernac_list e
+ | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
@@ -116,36 +116,36 @@ let rec classify_vernac e =
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
| VernacDefinition (
- (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) ->
+ (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
- | VernacDefinition (_,(_,i),ProveBody _) ->
+ | VernacDefinition (_,((_,i),_),ProveBody _) ->
VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
| VernacStartTheoremProof (_,l,_) ->
let ids =
- CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
+ CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
| VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
| VernacFixpoint (_,l) ->
let ids, open_proof =
- List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
+ List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (_,l) ->
let ids, open_proof =
- List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
+ List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
(* Sideff: apply to all open branches. usually run on master only *)
| VernacAssumption (_,_,l) ->
- let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
+ let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
VtSideff ids, VtLater
- | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
+ | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
| VernacInductive (_,_,l) ->
- let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
+ let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
CList.map_filter (function
@@ -173,9 +173,13 @@ let rec classify_vernac e =
| VernacDeclareReduction _
| VernacDeclareClass _ | VernacDeclareInstances _
| VernacRegister _
- | VernacDeclareTacticDefinition _
| VernacNameSectionHypSet _
| VernacComments _ -> VtSideff [], VtLater
+ | VernacDeclareTacticDefinition (_,l) ->
+ let open Libnames in
+ VtSideff (List.map (function
+ | (Ident (_,r),_,_) -> r
+ | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater
(* Who knows *)
| VernacLoad _ -> VtSideff [], VtNow
(* (Local) Notations have to disappear *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index b2072221..06bf955c 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -10,7 +10,7 @@ open Util
let check_vio (ts,f) =
Dumpglob.noglob ();
- let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
+ 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
@@ -30,7 +30,7 @@ let schedule_vio_checking j fs =
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
+ let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
@@ -104,9 +104,7 @@ let schedule_vio_compilation j fs =
let f =
if Filename.check_suffix f ".vio" then Filename.chop_extension f
else f in
- let paths = Loadpath.get_paths () in
- let _, long_f_dot_v =
- System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") 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
let eta =
try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 05:04:16 +0000