From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- stm/asyncTaskQueue.ml | 7 ++--- stm/asyncTaskQueue.mli | 2 +- stm/coqworkmgrApi.ml | 2 +- stm/coqworkmgrApi.mli | 2 +- stm/dag.ml | 2 +- stm/dag.mli | 2 +- stm/lemmas.ml | 65 +++++++++++++++++++++++++---------------------- stm/lemmas.mli | 17 ++++++++----- stm/proofworkertop.ml | 2 +- stm/queryworkertop.ml | 2 +- stm/spawned.ml | 2 +- stm/spawned.mli | 2 +- stm/stm.ml | 36 +++++++++++++++++++++----- stm/stm.mli | 3 +++ stm/tQueue.ml | 2 +- stm/tQueue.mli | 2 +- stm/tacworkertop.ml | 2 +- stm/texmacspp.ml | 2 +- stm/texmacspp.mli | 2 +- stm/vcs.ml | 2 +- stm/vcs.mli | 2 +- stm/vernac_classifier.ml | 2 +- stm/vernac_classifier.mli | 2 +- stm/vio_checking.ml | 4 +-- stm/vio_checking.mli | 2 +- stm/workerPool.ml | 2 +- stm/workerPool.mli | 2 +- 27 files changed, 103 insertions(+), 71 deletions(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index e3fb0b60..cc973260 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* set_slave_opt tl - | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile" - |"-load-vernac-source" |"-compile-verbose" + | ("-async-proofs" |"-toploop" |"-vi2vo" + |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" + |"-compile" |"-compile-verbose" |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> set_slave_opt tl | x::tl -> x :: set_slave_opt tl in diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index a3fe4b8c..f140f8ed 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* exn) hook l r with e when Errors.noncritical e -> let e = Errors.push e in @@ -219,11 +220,11 @@ let compute_proof_name locality = function locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then user_err_loc (loc,"",pr_id id ++ str " already exists."); - id + id, pl | None -> - next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) + next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -276,28 +277,28 @@ let save_hook = ref ignore let set_save_hook f = save_hook := f let save_named ?export_seff proof = - let id,const,cstrs,do_guard,persistence,hook = proof in - save ?export_seff id const cstrs do_guard persistence hook + let id,const,(cstrs,pl),do_guard,persistence,hook = proof in + save ?export_seff id const cstrs pl do_guard persistence hook let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then error "This command can only be used for unnamed theorem." - let save_anonymous ?export_seff proof save_ident = - let id,const,cstrs,do_guard,persistence,hook = proof in + let id,const,(cstrs,pl),do_guard,persistence,hook = proof in check_anonymity id save_ident; - save ?export_seff save_ident const cstrs do_guard persistence hook + save ?export_seff save_ident const cstrs pl do_guard persistence hook let save_anonymous_with_strength ?export_seff proof kind save_ident = - let id,const,cstrs,do_guard,_,hook = proof in + let id,const,(cstrs,pl),do_guard,_,hook = proof in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) - save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook + save ?export_seff save_ident const cstrs pl do_guard + (Global, const.const_entry_polymorphic, Proof kind) hook (* Admitted *) -let admit (id,k,e) hook () = +let admit (id,k,e) pl hook () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in let () = match k with | Global, _, _ -> () @@ -306,6 +307,7 @@ let admit (id,k,e) hook () = str "declared as an axiom.") in let () = assumption_message id in + Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; call_hook (fun exn -> exn) hook Global (ConstRef kn) (* Starting a goal *) @@ -315,11 +317,10 @@ let set_start_hook = (:=) start_hook let get_proof proof do_guard hook opacity = - let (id,(const,cstrs,persistence)) = + let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in - (** FIXME *) - id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook + id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook let check_exist = List.iter (fun (loc,id) -> @@ -329,16 +330,16 @@ let check_exist = let universe_proof_terminator compute_guard hook = let open Proof_global in function - | Admitted (id,k,pe,ctx) -> - admit (id,k,pe) (hook (Some ctx)) (); + | Admitted (id,k,pe,(ctx,pl)) -> + admit (id,k,pe) pl (hook (Some ctx)) (); 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 (Some proof.Proof_global.universes)) is_opaque in + let proof = get_proof proof compute_guard + (hook (Some (fst proof.Proof_global.universes))) is_opaque in begin match idopt with | None -> save_named ~export_seff proof | Some ((_,id),None) -> save_anonymous ~export_seff proof id @@ -350,7 +351,7 @@ let universe_proof_terminator compute_guard hook = 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 start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = let terminator = standard_proof_terminator compute_guard hook in let sign = match sign with @@ -358,9 +359,9 @@ let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = | None -> initialize_named_context_for_proof () in !start_hook c; - Pfedit.start_proof id kind sigma sign c ?init_tac terminator + Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator -let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = let terminator = universe_proof_terminator compute_guard hook in let sign = match sign with @@ -368,11 +369,11 @@ let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = | None -> initialize_named_context_for_proof () in !start_hook c; - Pfedit.start_proof id kind sigma sign c ?init_tac terminator + Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun (id,(t,_)) -> (id,t)) thms with + match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -380,7 +381,7 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with + in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false @@ -409,7 +410,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in match thms with | [] -> anomaly (Pp.str "No proof to start") - | (id,(t,(_,imps)))::other_thms -> + | ((id,pl),(t,(_,imps)))::other_thms -> let hook ctx strength ref = let ctx = match ctx with | None -> Evd.empty_evar_universe_context @@ -428,7 +429,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard let start_proof_com kind thms hook = let env0 = Global.env () in @@ -472,14 +473,13 @@ let save_proof ?proof = function if const_entry_type = None then error "Admitted requires an explicit statement"; let typ = Option.get const_entry_type in - let ctx = Evd.evar_context_universe_context universes in + let ctx = Evd.evar_context_universe_context (fst universes) in Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) | None -> let id, k, typ = Pfedit.current_proof_statement () in (* This will warn if the proof is complete *) 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 @@ -489,7 +489,10 @@ 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),universes) + let names = Pfedit.get_universe_binders () in + let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in + Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), + (universes, Some binders)) in Proof_global.get_terminator() pe | Vernacexpr.Proved (is_opaque,idopt) -> diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 6556aa22..16e54e31 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Globnames.global_reference -> 'a) -> 'a declaration_hook @@ -24,20 +23,24 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (types -> unit) -> unit -val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - (Proof_global.proof_universes option -> unit declaration_hook) -> unit + (Evd.evar_universe_context option -> unit declaration_hook) -> unit val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit val start_proof_with_initialization : - goal_kind -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list + goal_kind -> Evd.evar_map -> + (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> + ((Id.t * universe_binders option) * + (types * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit val standard_proof_terminator : diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 0e40c345..23538a46 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ()) () +let tactic_being_run, tactic_being_run_hook = Hook.make + ~default:(fun _ -> ()) () + include Hook (* enables: Hooks.(call foo args) *) @@ -1471,6 +1474,18 @@ end = struct (* {{{ *) try Reach.known_state ~cache:`No id; let t, uc = Future.purify (fun () -> + let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in + let g = Evd.find sigma0 r_goal in + if not ( + Evarutil.is_ground_term sigma0 Evd.(evar_concl g) && + List.for_all (fun (_,bo,ty) -> + Evarutil.is_ground_term sigma0 ty && + Option.cata (Evarutil.is_ground_term sigma0) true bo) + Evd.(evar_context g)) + then + Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^ + "goals only")) + else begin vernac_interp r_state_fb r_ast; let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with @@ -1479,9 +1494,10 @@ end = struct (* {{{ *) let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then t, Evd.evar_universe_context sigma - else Errors.errorlabstrm "Stm" (str"The solution is not ground")) - () in - RespBuiltSubProof (t,uc) + else Errors.errorlabstrm "Stm" (str"The solution is not ground") + end) () + in + RespBuiltSubProof (t,uc) with e when Errors.noncritical e -> RespError (Errors.print e) let name_of_task { t_name } = t_name @@ -1787,16 +1803,21 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> reach ~cache:`Shallow view.next; + Hooks.(call tactic_being_run true); Partac.vernac_interp - cancel !Flags.async_proofs_n_tacworkers view.next id x + cancel !Flags.async_proofs_n_tacworkers view.next id x; + Hooks.(call tactic_being_run false) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel } when Flags.async_proofs_is_master () -> (fun () -> reach view.next; Query.vernac_interp cancel view.next id x ), cache, false - | `Cmd { cast = x; ceff = eff } -> (fun () -> - reach view.next; vernac_interp id x; + | `Cmd { cast = x; ceff = eff; ctac } -> (fun () -> + reach view.next; + if ctac then Hooks.(call tactic_being_run true); + vernac_interp id x; + if ctac then Hooks.(call tactic_being_run false); if eff then update_global_env ()), cache, true | `Fork ((x,_,_,_), None) -> (fun () -> reach view.next; vernac_interp id x; @@ -2577,4 +2598,5 @@ 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 +let tactic_being_run_hook = Hooks.tactic_being_run_hook (* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli index 0c05c93d..ad89eb71 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -107,6 +107,9 @@ val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> 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 +(* called with true before and with false after a tactic explicitly + * in the document is run *) +val tactic_being_run_hook : (bool -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 2dad962b..ee121c46 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] | "-schedule-vio-checking" :: rest -> filter_argv true rest - | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest) + | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest) | _ :: rest when b -> filter_argv b rest | s :: rest -> s :: filter_argv b rest in let pack = function diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli index e2da5026..c0b6d9e6 100644 --- a/stm/vio_checking.mli +++ b/stm/vio_checking.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*