From 297b0cb44bbe8ec7304ca635c566815167266d4a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Jun 2015 11:28:44 +0200 Subject: Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again. --- stm/texmacspp.ml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index aaa6c2c07d..af506015de 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -513,13 +513,6 @@ let rec tmpp v loc = 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 - | ByNotation(loc,name,None) -> xmlNotation [] name loc [] - | ByNotation(loc,name,Some d) -> - xmlNotation ["delimiter",d] name loc [] - | AN ref -> xmlReference ref) l) | VernacInfix (_,((_,name),sml),ce,sn) -> let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in let sc_attr = @@ -535,6 +528,7 @@ let rec tmpp v loc = | Some scope -> ["scope", scope] | None -> [] in xmlNotation (sc_attr @ attrs) name loc [pp_expr ce] + | VernacBindScope _ as x -> xmlTODO loc x | VernacNotationAddFormat _ as x -> xmlTODO loc x | VernacUniverse _ | VernacConstraint _ -- cgit v1.2.3 From 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 14 Sep 2015 18:35:48 +0200 Subject: Univs: Add universe binding lists to definitions ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. --- stm/lemmas.ml | 8 ++++++-- stm/stm.ml | 4 ++-- stm/texmacspp.ml | 12 ++++++------ stm/vernac_classifier.ml | 14 +++++++------- 4 files changed, 21 insertions(+), 17 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index a7ef96c668..7679b1a662 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -212,7 +212,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) @@ -431,7 +431,11 @@ 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 diff --git a/stm/stm.ml b/stm/stm.ml index e6271f6089..4a303f036e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -424,8 +424,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 diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index aaa6c2c07d..fb41bb7bea 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) = @@ -540,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) @@ -555,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]) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2b5eb86834..a2b7795166 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -116,25 +116,25 @@ 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 @@ -143,9 +143,9 @@ let rec classify_vernac e = | VernacAssumption (_,_,l) -> let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd 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 -- cgit v1.2.3 From f5e0f609c8c2c77205fcfb296535a7d8856db584 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Sep 2015 15:20:47 +0200 Subject: STM: Reset takes Ltac into account (Close #4316) --- stm/vernac_classifier.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index a2b7795166..8aa2a59177 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -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 *) -- cgit v1.2.3 From f20fce1259563f2081fadc62ccab1304bb8161d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 19:00:59 +0200 Subject: Rich printing of messages. --- stm/asyncTaskQueue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index e3fb0b607a..e525031e63 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -297,7 +297,7 @@ module Make(T : Task) = struct let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback fb) []; flush oc in Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); - Pp.log_via_feedback (); + Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg)); Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with -- cgit v1.2.3 From f52826877059858fb3fcd4314c629ed63d90a042 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Sep 2015 19:50:41 +0200 Subject: Hardening the API of evarmaps. The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap. --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 4a303f036e..f178c3ae4a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -166,7 +166,7 @@ type visit = { step : step; next : Stateid.t } (* Parts of the system state that are morally part of the proof state *) let summary_pstate = [ Evarutil.meta_counter_summary_name; - Evarutil.evar_counter_summary_name; + Evd.evar_counter_summary_name; "program-tcc-table" ] type state = { system : States.state; -- cgit v1.2.3 From da4d0b0e3d82621fe8338dd313b788472fc31bb2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 10:26:08 +0200 Subject: Remove some uses of Loadpath.get_paths. The single remaining use is in library/states.ml. This use should be reviewed, as it is most certainly broken. The other uses of Loadpath.get_paths did not disappear by miracle though. They were replaced by a new function Loadpath.locate_file which factors all the uses of the function. This function should not be used as it is as broken as Loadpath.get_paths, by definition. Vernac.load_vernac now takes a complete path rather than looking up for the file. That is the way it was used most of the time, so the lookup was unnecessary. For instance, Vernac.compile was calling Library.start_library which already expected a complete path. Another consequence is that System.find_file_in_path is almost no longer used (except for Loadpath.locate_file, obviously). The two remaining uses are System.intern_state (used by States.intern_state, cf above) and Mltop.dir_ml_load for dynamically loading compiled .ml files. --- stm/vio_checking.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 4df9603dca..06bf955c82 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -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") -- cgit v1.2.3 From 91b1808056602f3e26d1eb1bdf7be1e791cb742d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:35:07 +0200 Subject: Univs: fix many evar_map initializations and leaks. --- stm/lemmas.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 7679b1a662..2bd1c54519 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -503,4 +503,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) -- cgit v1.2.3 From 11cdf7c2ca0017f6bae906f9c9d9eef41972affe Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 24 Sep 2015 15:16:06 +0200 Subject: Univs: fix handling of side effects/delayed proofs - When there are side effects which might enrich the initial universes of a proof, keep the initial and refined universe contexts apart like for delayed proofs, ensuring universes are declared before they are used in the right order. - Fix undefined levels in proof statements so that they can't be lowered to Set by a subsequent, delayed proof. --- stm/lemmas.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 2bd1c54519..16444fda05 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,7 +449,7 @@ 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 + start_proof_with_initialization kind (Evd.fix_undefined_variables evd) recguard thms snl hook -- cgit v1.2.3 From b8a85b65432a974d6a6f1fe5165e05d7196c9321 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 30 Sep 2015 18:33:27 +0200 Subject: Univs: fix semantics of Type in proof mode in universe-polymorphic mode Allowing universes to be instantiated if the body of the proof requires it (the levels stay flexible). Not allowed for non-polymorphic cases, to be compatible with the stm's invariant that the type should not change. --- stm/lemmas.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 16444fda05..5cbe152b55 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,8 +449,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.fix_undefined_variables 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 *) -- cgit v1.2.3 From 0de499ab4702708ddfae162389617869b170c7d7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Sep 2015 16:33:46 +0200 Subject: STM: fix backtrace handling --- stm/stm.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 4a303f036e..ed7c234c1e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1577,7 +1577,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) -- cgit v1.2.3 From f7e9e6428842dd80549a0dcd20bf872c2dd7fa8c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2015 22:18:56 +0200 Subject: STM: for PIDE based UIs, edit_at requires no Reach.known_state --- stm/stm.ml | 3 ++- stm/stm.mli | 10 ++++++---- 2 files changed, 8 insertions(+), 5 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index ed7c234c1e..d25466e089 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2342,7 +2342,8 @@ let edit_at id = VCS.delete_cluster_of id; VCS.gc (); VCS.print (); - Reach.known_state ~cache:(interactive ()) id; + if not !Flags.async_proofs_full then + Reach.known_state ~cache:(interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try diff --git a/stm/stm.mli b/stm/stm.mli index 1d926e998e..4bad7f0a6d 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. -- cgit v1.2.3 From 188ab7f76459ab46e0ea139da8b4331d958c7102 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Oct 2015 18:39:06 +0200 Subject: Spawn: use each socket exclusively for writing or reading According to http://caml.inria.fr/mantis/view.php?id=5325 you can't use the same socket for both writing and reading. The result is lockups (may be fixed in 4.03). --- stm/spawned.ml | 19 ++++++++++--------- stm/spawned.mli | 2 +- 2 files changed, 11 insertions(+), 10 deletions(-) (limited to 'stm') diff --git a/stm/spawned.ml b/stm/spawned.ml index a8372195d4..66fe07dbc4 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 d9e7baff3b..d0183e081d 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 -- cgit v1.2.3 From 9ea8867a0fa8f2a52df102732fdc1a931c659826 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2015 22:12:25 +0200 Subject: Proof using: let-in policy, optional auto-clear, forward closure* - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using . - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. --- stm/stm.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index d25466e089..acbb5f646d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -888,9 +888,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) -- cgit v1.2.3 From 33d153a01f2814c6e5486c07257667254b91fa0c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 7 Oct 2015 15:08:27 +0200 Subject: Axioms now support the universe binding syntax. We artificially restrict the syntax though, because it is unclear of what the semantics of several axioms in a row is, in particular about the resolution of remaining evars. --- stm/texmacspp.ml | 5 +++-- stm/vernac_classifier.ml | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index fb41bb7bea..b912080413 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -575,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 8aa2a59177..a898c687be 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -141,7 +141,7 @@ let rec classify_vernac e = 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 | VernacInductive (_,_,l) -> -- cgit v1.2.3 From b2007e86b4a28570eee52439ad8b9fee603443b8 Mon Sep 17 00:00:00 2001 From: Alec Faithfull Date: Tue, 6 Oct 2015 13:50:59 +0200 Subject: STM: Pass exception information to unreachable_state_hook functions This lets hooks treat different exceptions in different ways; in particular, user interrupts can now be safely ignored --- stm/stm.ml | 4 ++-- stm/stm.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index acbb5f646d..e96c396bae 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 @@ -736,7 +736,7 @@ end = struct (* {{{ *) 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)) diff --git a/stm/stm.mli b/stm/stm.mli index 4bad7f0a6d..2453f258c5 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -100,7 +100,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 -- cgit v1.2.3 From ce0c536b4430711db1e30cd7ac35ae8d71d34e64 Mon Sep 17 00:00:00 2001 From: Alec Faithfull Date: Tue, 6 Oct 2015 13:58:50 +0200 Subject: STM: Added functions for saving and restoring the internal state PIDEtop needs these to implement its new transaction mechanism --- stm/stm.ml | 3 +++ stm/stm.mli | 4 ++++ 2 files changed, 7 insertions(+) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index e96c396bae..c0d71dc933 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2405,6 +2405,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) ***************************) (******************************************************************************) diff --git a/stm/stm.mli b/stm/stm.mli index 2453f258c5..18ed6fc2e8 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -83,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 -- cgit v1.2.3 From 56ca108e63191e90c3d4169c37a4c97017e3c6ae Mon Sep 17 00:00:00 2001 From: Alec Faithfull Date: Tue, 6 Oct 2015 14:19:34 +0200 Subject: TQueue: Expose the length of TQueues --- stm/tQueue.ml | 8 ++++++++ stm/tQueue.mli | 2 ++ 2 files changed, 10 insertions(+) (limited to 'stm') diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 6fef895ae8..2a43cd7d13 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,6 +94,12 @@ 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; diff --git a/stm/tQueue.mli b/stm/tQueue.mli index 7458de510f..f54af4df47 100644 --- a/stm/tQueue.mli +++ b/stm/tQueue.mli @@ -28,3 +28,5 @@ 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 -- cgit v1.2.3 From f6b3704391de97ee544da9ae7316685cd2d9fae3 Mon Sep 17 00:00:00 2001 From: Alec Faithfull Date: Tue, 6 Oct 2015 14:20:22 +0200 Subject: TQueue: Allow some tasks to be saved when clearing a TQueue --- stm/tQueue.ml | 12 ++++++++++++ stm/tQueue.mli | 1 + 2 files changed, 13 insertions(+) (limited to 'stm') diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 2a43cd7d13..2dad962bec 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -105,6 +105,18 @@ let clear { queue = q; lock = m; cond = c } = 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 f54af4df47..1df52d2523 100644 --- a/stm/tQueue.mli +++ b/stm/tQueue.mli @@ -22,6 +22,7 @@ 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 -- cgit v1.2.3 From 41ac12062858d3b8b82b0ed736b3800d052f34b8 Mon Sep 17 00:00:00 2001 From: Alec Faithfull Date: Tue, 6 Oct 2015 15:23:02 +0200 Subject: STM: Work around an occasional crash in dot (debug output) The splines=ortho option seems to make dot crash sometimes, so this commit removes it from the STM debugging output --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index c0d71dc933..5bb46fd368 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -372,7 +372,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) -> -- cgit v1.2.3 From 5009be2f117a5ef27733b7d6895503af91e9aa34 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Oct 2015 15:57:42 +0200 Subject: When typechecking a lemma statement, try to resolve typeclasses before failing for unresolved evars (regression). --- stm/lemmas.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5cbe152b55..c49ddfd8ec 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -439,7 +439,7 @@ let start_proof_com kind thms hook = 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), -- cgit v1.2.3 From d558bf5289e87899a850dda410a3a3c4de1ce979 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 17 Oct 2015 18:55:42 +0200 Subject: Clarifying and documenting the UState API. --- stm/lemmas.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index d26af04baa..5f034e361e 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -428,7 +428,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 (*FIXME*) Univ.UContext.empty ctx in + let ctx = UState.context_set (*FIXME*) 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 -- cgit v1.2.3 From c8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Oct 2015 11:40:22 +0200 Subject: Miscellaneous typos, spacing, US spelling in comments or variable names. --- stm/stm.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 5bb46fd368..88a1fbbf48 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -639,7 +639,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 @@ -1912,7 +1912,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 -> [] -- cgit v1.2.3 From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- stm/lemmas.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index c49ddfd8ec..6c18326882 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 -- cgit v1.2.3 From a3a17b514a2ffaba54cd182fdf27b7e84366ab44 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 29 Oct 2015 15:11:29 -0400 Subject: Handle side-effects of Vernacular commands inside proofs better, so that universes are declared correctly in the enclosing proofs evar_map's. --- stm/stm.ml | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 88a1fbbf48..02361c738d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -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 @@ -135,6 +139,7 @@ type branch_type = 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 ] } @@ -721,6 +726,7 @@ end = struct (* {{{ *) try prerr_endline("defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); + (* set id and good id *) f (); if cache = `Yes then freeze `No id else if cache = `Shallow then freeze `Shallow id; @@ -730,7 +736,7 @@ 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 @@ -1753,8 +1759,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; @@ -1784,9 +1791,9 @@ let known_state ?(redefine_qed=false) ~cache id = 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 () @@ -1885,7 +1892,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; @@ -2135,7 +2142,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") @@ -2158,7 +2165,7 @@ 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 } -> () @@ -2176,7 +2183,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 @@ -2192,7 +2199,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 @@ -2216,7 +2223,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 -- cgit v1.2.3 From 77cf18eb844b45776b2ec67be9f71e8dd4ca002c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 30 Oct 2015 11:48:40 -0400 Subject: Add a way to get the right fix_exn in external vernacular commands involving Futures. --- stm/stm.ml | 8 ++++++-- stm/stm.mli | 1 + 2 files changed, 7 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 02361c738d..42be4fca71 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -596,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 @@ -619,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 = @@ -726,8 +728,10 @@ end = struct (* {{{ *) try prerr_endline("defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); - (* set id and good id *) + 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); @@ -2559,5 +2563,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 18ed6fc2e8..0c05c93d4d 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -136,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) -- cgit v1.2.3 From 559c0a4a40410745f73822e893b3d1581056ea7a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Nov 2015 15:01:15 +0100 Subject: STM: never reopen a branch containing side effects --- stm/stm.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 42be4fca71..a6a64f2094 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2317,6 +2317,12 @@ let edit_at id = | { step = `Fork _ } -> false | { next } -> aux next in aux (VCS.get_branch_pos (VCS.current_branch ())) in + let rec is_pure id = + let view = VCS.visit id in + match view.step with + | `Cmd _ -> is_pure view.next + | `Fork _ -> true + | _ -> false in let is_ancestor_of_cur_branch id = Vcs_.NodeSet.mem id (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in @@ -2377,7 +2383,7 @@ let edit_at id = | _, Some _, None -> assert false | 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 + if has_failed qed_id && is_pure (VCS.visit qed_id).next && 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) -> -- cgit v1.2.3 From 6e376c8097d75b6e63a7e52332a721f7928992e9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Nov 2015 15:01:58 +0100 Subject: STM: fix undo into a branch containing side effects The "master" label used to be reset to the wrong id --- stm/stm.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index a6a64f2094..89034706a4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2333,7 +2333,9 @@ 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 - | { step = (`Fork _ | `Sideff _ | `Qed _) } -> tip + | { 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 old_branch = let master_id, cancel_switch, keep = -- cgit v1.2.3 From 5a5f2b4253b5834e09f43cb36a81ce6f53cc2da3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 2 Nov 2015 16:39:03 +0100 Subject: Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico. --- stm/stm.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 89034706a4..14142aa0c5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2317,12 +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 id = + let rec is_pure_aux id = let view = VCS.visit id in match view.step with - | `Cmd _ -> is_pure view.next + | `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 @@ -2385,7 +2390,7 @@ let edit_at id = | _, Some _, None -> assert false | false, Some (qed_id,start), Some(mode,bn) -> let tip = VCS.cur_tip () in - if has_failed qed_id && is_pure (VCS.visit qed_id).next && not !Flags.async_proofs_never_reopen_branch + 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) -> -- cgit v1.2.3 From 90fef3ffd236f2ed5575b0d11a47185185abc75b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 28 Nov 2015 19:41:17 +0100 Subject: Univs: correctly register universe binders for lemmas. --- stm/lemmas.ml | 63 ++++++++++++++++++++++++++++++---------------------------- stm/lemmas.mli | 15 ++++++++------ 2 files changed, 42 insertions(+), 36 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 6c18326882..5f4e4deb47 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -186,7 +186,7 @@ let look_for_possibly_mutual_statements = function (* Saving a goal *) -let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook = +let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in try let const = adjust_guardness_conditions const do_guard in @@ -205,6 +205,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook = declare_constant ?export_seff id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in definition_message id; + Option.iter (Universes.register_universe_binders r) pl; call_hook (fun exn -> 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 6556aa2297..376374cb85 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -14,7 +14,6 @@ open Vernacexpr open Pfedit type 'a declaration_hook - val mk_hook : (Decl_kinds.locality -> 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 : -- cgit v1.2.3 From 315aac9ae0d411c10849c421d5dfd8e134919233 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Dec 2015 11:30:35 +0100 Subject: vio: fix argument parsing (progress on #4442) --- stm/vio_checking.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 06bf955c82..ce930cacb7 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -43,7 +43,7 @@ let schedule_vio_checking j fs = let rec filter_argv b = function | [] -> [] | "-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 -- cgit v1.2.3 From 153d77d00ccbacf22aa5d70ca2c1cacab2749339 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Dec 2015 21:46:12 +0100 Subject: Specializing the Dyn module to each usecase. Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point. --- stm/stm.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 6236297459..ea669b1596 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -631,10 +631,9 @@ end = struct (* {{{ *) States.unfreeze system; Proof_global.unfreeze proof (* hack to make futures functional *) - let in_t, out_t = Dyn.create "state4future" let () = Future.set_freeze - (fun () -> in_t (freeze_global_state `No, !cur_id)) - (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) + (fun () -> Obj.magic (freeze_global_state `No, !cur_id)) + (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i) type frozen_state = state type proof_part = -- cgit v1.2.3 From e181c9b043e64342c1e51763f4fe88c78bc4736d Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 12:20:47 +0100 Subject: CLEANUP: Vernacexpr.vernac_expr Originally, "VernacTime" and "VernacRedirect" were defined like this: type vernac_expr = ... | VernacTime of vernac_list | VernacRedirect of string * vernac_list ... where type vernac_list = located_vernac_expr list Currently, that list always contained one and only one element. So I propose changing the definition of these two variants in the following way: | VernacTime of located_vernac_expr | VernacRedirect of string * located_vernac_expr which covers all our current needs and enforces the invariant related to the number of commands that are part of the "VernacTime" and "VernacRedirect" variants. --- stm/stm.ml | 4 ++-- stm/texmacspp.ml | 8 ++++---- stm/vernac_classifier.ml | 11 ++--------- 3 files changed, 8 insertions(+), 15 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index ea669b1596..e0e7875036 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -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 | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el + | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e | _ -> false in if internal_command expr then begin prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) @@ -1501,7 +1501,7 @@ end = struct (* {{{ *) let e, etac, time, fail = let rec find time fail = function | VernacSolve(_,_,re,b) -> re, b, time, fail - | VernacTime [_,e] | VernacRedirect (_,[_,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 () -> diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index b912080413..95aaea6f00 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -487,12 +487,12 @@ let rec tmpp v loc = (* Control *) | VernacLoad (verbose,f) -> xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] [] - | VernacTime l -> + | VernacTime (loc,e) -> xmlApply loc (Element("time",[],[]) :: - List.map (fun(loc,e) ->tmpp e loc) l) - | VernacRedirect (s, l) -> + [tmpp e loc]) + | VernacRedirect (s, (loc,e)) -> xmlApply loc (Element("redirect",["path", s],[]) :: - List.map (fun(loc,e) ->tmpp e loc) l) + [tmpp e loc]) | VernacTimeout (s,e) -> xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index a898c687be..32358c592b 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 | VernacRedirect (_, e) -> classify_vernac_list e + | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ @@ -175,7 +175,7 @@ let rec classify_vernac e = | VernacRegister _ | VernacNameSectionHypSet _ | VernacComments _ -> VtSideff [], VtLater - | VernacDeclareTacticDefinition (_,l) -> + | VernacDeclareTacticDefinition l -> let open Libnames in VtSideff (List.map (function | (Ident (_,r),_,_) -> r @@ -217,13 +217,6 @@ let rec classify_vernac e = | VernacExtend (s,l) -> try List.assoc s !classifiers l () with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)) - and classify_vernac_list = function - (* spiwack: It would be better to define a monoid on classifiers. - So that the classifier of the list would be the composition of - the classifier of the individual commands. Currently: special - case for singleton lists.*) - | [_,c] -> static_classifier c - | l -> VtUnknown,VtNow in let res = static_classifier e in if Flags.is_universe_polymorphism () then -- cgit v1.2.3 From 493b5d18971c8c19eaeccfc992d1212c6479d227 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:38:19 +0100 Subject: CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular command is mapped. --- stm/texmacspp.ml | 1 - stm/vernac_classifier.ml | 1 - 2 files changed, 2 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 95aaea6f00..2a09143940 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -724,7 +724,6 @@ let rec tmpp v loc = | VernacRegister _ as x -> xmlTODO loc x | VernacComments (cl) -> xmlComment loc (List.flatten (List.map pp_comment cl)) - | VernacNop as x -> xmlTODO loc x (* Stm backdoor *) | VernacStm _ as x -> xmlTODO loc x diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 32358c592b..90490c38bd 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -208,7 +208,6 @@ let rec classify_vernac e = | VernacResetName _ | VernacResetInitial | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e (* What are these? *) - | VernacNop | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtUnknown, VtNow -- cgit v1.2.3 From 20641795624dbb03da0401e4dc503660e5e73df6 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:50:40 +0100 Subject: CLEANUP: Vernacexpr.VernacDeclareTacticDefinition The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that. --- stm/vernac_classifier.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 90490c38bd..58e26de841 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -177,9 +177,11 @@ let rec classify_vernac e = | VernacComments _ -> VtSideff [], VtLater | VernacDeclareTacticDefinition l -> let open Libnames in + let open Vernacexpr in VtSideff (List.map (function - | (Ident (_,r),_,_) -> r - | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater + | TacticDefinition ((_,r),_) -> r + | TacticRedefinition (Ident (_,r),_) -> r + | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) -- cgit v1.2.3 From 1b5f85d38db7a0d7cb9a4b9491a5563461373182 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 17:31:25 +0100 Subject: CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified --- stm/texmacspp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 2a09143940..1996d35259 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -347,7 +347,7 @@ and pp_cases_pattern_expr cpe = xmlApply loc (xmlOperator "delimiter" ~attr:["name", delim] loc :: [pp_cases_pattern_expr cpe]) -and pp_case_expr (e, (name, pat)) = +and pp_case_expr (e, name, pat) = match name, pat with | None, None -> xmlScrutinee [pp_expr e] | Some (loc, name), None -> -- cgit v1.2.3 From 97c1dfa2f76a61992e600be4f07babb5be9c521e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:23:14 +0100 Subject: Remove useless recursive flags. --- stm/vernac_classifier.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 58e26de841..dcb6700941 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -60,7 +60,7 @@ let undo_classifier = ref (fun _ -> assert false) let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = - let rec static_classifier e = match e with + let static_classifier e = match e with (* PG compatibility *) | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) -- cgit v1.2.3 From bfdf6d2db29972ff52a1870524a230fdecb636dc Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:31:47 +0100 Subject: Remove unused functions. --- stm/texmacspp.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 1996d35259..b18e35a472 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -20,9 +20,6 @@ let unlock loc = let start, stop = Loc.unloc loc in (string_of_int start, string_of_int stop) -let xmlNoop = (* almost noop *) - PCData "" - let xmlWithLoc loc ename attr xml = let start, stop = unlock loc in Element(ename, [ "begin", start; "end", stop ] @ attr, xml) -- cgit v1.2.3 From 5129c5b02bcab1426636d18583ec7a4a46195f0a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 16:55:03 +0100 Subject: Reduce dependencies of interface files. --- stm/lemmas.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.mli b/stm/lemmas.mli index e2ddf79df8..93f24b42cb 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -9,8 +9,6 @@ open Names open Term open Decl_kinds -open Constrexpr -open Vernacexpr open Pfedit type 'a declaration_hook -- cgit v1.2.3 From 3049b2930ec2bd4adf886fc90bf01a478b318477 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:01:28 +0100 Subject: Remove some useless module opening. --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index e0e7875036..96f127aa24 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1616,7 +1616,7 @@ end = struct (* {{{ *) let vernac_interp switch prev id q = assert(TaskQueue.n_workers (Option.get !queue) > 0); TaskQueue.enqueue_task (Option.get !queue) - QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch) + QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch) let init () = queue := Some (TaskQueue.create (if !Flags.async_proofs_full then 1 else 0)) -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- stm/asyncTaskQueue.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index e525031e63..863bab7cc9 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -60,9 +60,7 @@ module Make(T : Task) = struct type more_data = | MoreDataUnivLevel of Univ.universe_level list - - let request_expiry_of_task (t, c) = T.request_of_task t, c - + let slave_respond (Request r) = let res = T.perform r in Response res -- cgit v1.2.3 From e5f5ea2da95297fefe1afebfe303c5d5ba7d41aa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jan 2016 15:38:34 +0100 Subject: workers: purge short version of -load-vernac too (fix #4458) --- stm/asyncTaskQueue.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index e3fb0b607a..222f02c007 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -125,8 +125,9 @@ module Make(T : Task) = struct "-async-proofs-worker-priority"; Flags.string_of_priority !Flags.async_proofs_worker_priority] | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> 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 -- cgit v1.2.3 From d2b468a87cc50b1558feffc6cd3e1b866205c684 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jan 2016 16:00:11 +0100 Subject: par: check if the goal is not ground and fail (fix #4465) --- stm/stm.ml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 14142aa0c5..3d007004e2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1471,17 +1471,29 @@ 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 | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") | Evd.Evar_defined t -> - 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 -- cgit v1.2.3 From 08fdf3c7361c75037e12c5cd0e9f965165fed498 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jan 2016 21:19:50 +0100 Subject: fixup d2b468a, evar normalization is needed --- stm/stm.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 3d007004e2..168d8bf084 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1488,6 +1488,7 @@ end = struct (* {{{ *) match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") | Evd.Evar_defined t -> + 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") -- cgit v1.2.3 From a1aff01d16bad2f44392fd5cb804092e12e558ed Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:19:51 +0100 Subject: CLEANUP: removing unused field I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around. --- stm/texmacspp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index b18e35a472..70eccc2403 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -457,7 +457,7 @@ and pp_expr ?(attr=[]) e = (return @ [Element ("scrutinees", [], List.map pp_case_expr cel)] @ [pp_branch_expr_list bel])) - | CRecord (_, _, _) -> assert false + | CRecord (_, _) -> assert false | CLetIn (loc, (varloc, var), value, body) -> xmlApply loc (xmlOperator "let" loc :: -- cgit v1.2.3 From 51b2581d027528c8e4a347f157baf51a71b9d613 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:39:57 +0100 Subject: CLEANUP: removing unnecessary wrapper --- stm/stm.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.mli b/stm/stm.mli index 0c05c93d4d..2c9b983ec1 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -9,6 +9,7 @@ open Vernacexpr open Names open Feedback +open Loc (** state-transaction-machine interface *) @@ -19,7 +20,7 @@ open Feedback The sentence [s] is parsed in the state [ontop]. If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) -val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) -> +val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) -> bool -> edit_id -> string -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] @@ -123,7 +124,7 @@ val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] (* Adds a new line to the document. It replaces the core of Vernac.interp. [finish] is called as the last bit of this function is the system is running interactively (-emacs or coqtop). *) -val interp : bool -> located_vernac_expr -> unit +val interp : bool -> vernac_expr located -> unit (* Queries for backward compatibility *) val current_proof_depth : unit -> int -- cgit v1.2.3 From 74a5cfa8b2f1a881ebf010160421cf0775c2a084 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Jan 2016 17:49:49 +0100 Subject: Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. --- stm/stm.ml | 15 ++++++++++++--- stm/stm.mli | 3 +++ 2 files changed, 15 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 168d8bf084..5a34e81114 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -53,6 +53,9 @@ let execution_error, execution_error_hook = Hook.make let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () +let tactic_being_run, tactic_being_run_hook = Hook.make + ~default:(fun _ -> ()) () + include Hook (* enables: Hooks.(call foo args) *) @@ -1800,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; @@ -2590,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 0c05c93d4d..ad89eb71f3 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 -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- stm/asyncTaskQueue.ml | 2 +- stm/asyncTaskQueue.mli | 2 +- stm/coqworkmgrApi.ml | 2 +- stm/coqworkmgrApi.mli | 2 +- stm/dag.ml | 2 +- stm/dag.mli | 2 +- stm/lemmas.ml | 2 +- stm/lemmas.mli | 2 +- stm/proofworkertop.ml | 2 +- stm/queryworkertop.ml | 2 +- stm/spawned.ml | 2 +- stm/spawned.mli | 2 +- stm/stm.ml | 2 +- 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 | 2 +- stm/vio_checking.mli | 2 +- stm/workerPool.ml | 2 +- stm/workerPool.mli | 2 +- 26 files changed, 26 insertions(+), 26 deletions(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 222f02c007..cc97326047 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- stm/lemmas.ml | 11 +++++++---- stm/stm.ml | 6 ++---- 2 files changed, 9 insertions(+), 8 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 845f83a401..ac54028eb7 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -31,6 +31,7 @@ open Reductionops open Constrexpr open Constrintern open Impargs +open Context.Rel.Declaration type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a let mk_hook hook = hook @@ -44,7 +45,8 @@ let call_hook fix_exn hook l c = let retrieve_first_recthm = function | VarRef id -> - (pi2 (Global.lookup_named id),variable_opacity id) + let open Context.Named.Declaration in + (get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in (Global.body_of_constant_body cb, is_opaque cb) @@ -107,11 +109,12 @@ let find_mutually_recursive_statements thms = (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) (Global.env()) hyps in let ind_hyps = - List.flatten (List.map_i (fun i (_,b,t) -> + List.flatten (List.map_i (fun i decl -> + let t = get_type decl in match kind_of_term t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b -> + mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl -> [ind,x,i] | _ -> []) 0 (List.rev whnf_hyp_hds)) in @@ -450,7 +453,7 @@ let start_proof_com kind thms hook = let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); - let ids = List.map pi1 ctx in + let ids = List.map get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), diff --git a/stm/stm.ml b/stm/stm.ml index e8b500a620..1503c0f8ab 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1477,10 +1477,8 @@ end = struct (* {{{ *) 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)) + List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) + Evd.(evar_context g)) then Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^ "goals only")) -- cgit v1.2.3 From 22ab7fff908c259d6e433da246bebac519009905 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 10 Feb 2016 17:54:25 +0100 Subject: STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530 --- stm/stm.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index d8b2de4a2c..5ad1aead61 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1686,6 +1686,13 @@ let collect_proof keep cur hd brkind id = | _ -> false in let may_pierce_opaque = function | { expr = VernacPrint (PrintName _) } -> true + (* These do not exactly pierce opaque, but are anyway impossible to properly + * delegate *) + | { expr = (VernacDeclareModule _ + | VernacDefineModule _ + | VernacDeclareModuleType _ + | VernacInclude _) } -> true + | { expr = (VernacRequire _ | VernacImport _) } -> true | _ -> false in let parent = function Some (p, _) -> p | None -> assert false in let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in -- cgit v1.2.3 From df6bb883920e3a03044d09f10b57a44a2e7c5196 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 10 Feb 2016 17:59:14 +0100 Subject: STM: always stock in vio files the first node (state) of a proof It used not to be the case when the proof contains Sideff, since the code was picking the last known state and not necessarily the first one. Because of side effects the last known state could be the one corresponding to the side effect (that was executed to, say, change the parser). This is also related to bug #4530 --- stm/stm.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 5ad1aead61..56dcda6a4a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -513,7 +513,10 @@ end = struct (* {{{ *) let rec fill id = if (get_info id).state = None then fill (Vcs_aux.visit v id).next else copy_info_w_state v id in - fill stop + let v = fill stop in + (* We put in the new dag the first state (since Qed shall run on it, + * see check_task_aux) *) + copy_info_w_state v start let nodes_in_slice ~start ~stop = List.rev (List.map fst (nodes_in_slice ~start ~stop)) -- cgit v1.2.3 From 4f640bb24dfc45699670f41441355cdf71c83130 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 15 Feb 2016 16:11:11 +0100 Subject: STM: classify some variants of Instance as regular `Fork nodes. "Instance name : Type." is like "Lemma name : Type", i.e. it starts a proof. Unfortunately sometimes it does not, so we say VtUnknown. Still, if there is an open proof, we classify it as a regular Lemma, i.e. the opacity depends only on the terminator. This makes CoqIDE and PIDE based UI way more responsive when processing files containing Instance that are proved by tactics, since they are now correctly delegated to workers. Bug reported privately by Alec Faithfull. --- stm/stm.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 56dcda6a4a..f2855d5087 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2254,7 +2254,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[])); + let opacity_of_produced_term = + match x.expr with + | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | _ -> Doesn'tGuaranteeOpacity in + VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode "Classic"; end else begin -- cgit v1.2.3 From 9aa2d99fb1ad6b348142fce244f277b9dd25017f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Feb 2016 11:51:04 +0100 Subject: STM: Print/Extraction have to be skipped if -quick Print and Extraction commands may pierce opacity: if the task producing the proof term is not finished, we wait for its completion. In -quick mode no worker is going to process a task, since tasks are simply stored to disk (and resumed later in -vio2vo mode). This commit avoids coqc waits forever for a task in order to Print/Extract the corresponding term. Bug reported privately by Alec Faithfull. --- stm/stm.ml | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index f2855d5087..a6d119f0cd 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -83,6 +83,18 @@ let async_proofs_workers_extra_env = ref [||] type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr } let pr_ast { expr } = pr_vernac expr +(* Commands piercing opaque *) +let may_pierce_opaque = function + | { expr = VernacPrint (PrintName _) } -> true + | { expr = VernacExtend (("Extraction",_), _) } -> true + | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true + | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true + | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true + | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true + | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true + | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true + | _ -> false + (* Wrapper for Vernacentries.interp to set the feedback id *) let vernac_interp ?proof id ?route { verbose; loc; expr } = let rec internal_command = function @@ -145,7 +157,7 @@ type cmd_t = { ceff : bool; (* is a side-effecting command *) cast : ast; cids : Id.t list; - cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] } + cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] } type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list type qed_t = { qast : ast; @@ -1665,7 +1677,7 @@ let delegate name = let time = get_hint_bp_time name in time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio || !Flags.async_proofs_full - + let collect_proof keep cur hd brkind id = prerr_endline ("Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -1687,23 +1699,20 @@ let collect_proof keep cur hd brkind id = let has_proof_no_using = function | Some (_, { expr = VernacProof(_,None) }) -> true | _ -> false in - let may_pierce_opaque = function - | { expr = VernacPrint (PrintName _) } -> true - (* These do not exactly pierce opaque, but are anyway impossible to properly - * delegate *) + let too_complex_to_delegate = function | { expr = (VernacDeclareModule _ | VernacDefineModule _ | VernacDeclareModuleType _ | VernacInclude _) } -> true | { expr = (VernacRequire _ | VernacImport _) } -> true - | _ -> false in + | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in let rec collect last accn id = let view = VCS.visit id in match view.step with | (`Sideff (`Ast(x,_)) | `Cmd { cast = x }) - when may_pierce_opaque x -> `Sync(no_name,None,`Print) + when too_complex_to_delegate x -> `Sync(no_name,None,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) @@ -1811,6 +1820,8 @@ let known_state ?(redefine_qed=false) ~cache id = | `Alias (id,_) -> (fun () -> reach view.next; reach id ), cache, true + | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () -> + reach view.next), cache, true | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> reach ~cache:`Shallow view.next; Hooks.(call tactic_being_run true); @@ -2176,6 +2187,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let id = VCS.new_node ~id:newtip () in let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) + else if Flags.(!compilation_mode = BuildVio) && + VCS.((get_branch head).kind = `Master) && + may_pierce_opaque x + then `SkipQueue else `MainQueue in VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok -- cgit v1.2.3 From b98e4857a13a4014c65882af5321ebdb09f41890 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 17:40:10 +0100 Subject: Rename Ephemeron -> CEphemeron. Fixes compilation of Coq with OCaml 4.03 beta 1. --- stm/asyncTaskQueue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index cc97326047..5f018ec39d 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -314,7 +314,7 @@ module Make(T : Task) = struct let response = slave_respond request in report_status "Idle"; marshal_response (Option.get !slave_oc) response; - Ephemeron.clear () + CEphemeron.clear () with | MarshalError s -> pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 -- cgit v1.2.3 From d868820ad1f00b896c5f44f18678fac2f8e0f720 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 13:18:10 +0100 Subject: Supporting "(@foo) args" in patterns, where "@foo" has no arguments. --- stm/texmacspp.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 5bd1569ce5..3c4b8cb71e 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -304,7 +304,13 @@ and pp_cases_pattern_expr cpe = xmlApply loc (xmlOperator "alias" ~attr:["name", string_of_id id] loc :: [pp_cases_pattern_expr cpe]) - | CPatCstr (loc, ref, cpel1, cpel2) -> + | CPatCstr (loc, ref, None, cpel2) -> + xmlApply loc + (xmlOperator "reference" + ~attr:["name", Libnames.string_of_reference ref] loc :: + [Element ("impargs", [], []); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatCstr (loc, ref, Some cpel1, cpel2) -> xmlApply loc (xmlOperator "reference" ~attr:["name", Libnames.string_of_reference ref] loc :: -- cgit v1.2.3 From 45e43916a7ce756b617b7ba3f8062f7956872fb3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Mar 2016 17:10:16 +0100 Subject: Tentative fix for bug #4614: "Fully check the document" is uninterruptable. The SIGINT sent to the master coqtop process was lost in a watchdog thread, so that the STM resulted in an inconsistent state. This patch catches gracefully the exception and kills the task as if it were normally cancelled. Note that it probably won't work on non-POSIX architectures, but it does not really matter because interrupt was already badly handled anyway. --- stm/asyncTaskQueue.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 5f018ec39d..8649a14c54 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -184,6 +184,13 @@ module Make(T : Task) = struct let () = Unix.sleep 1 in kill_if () in + let kill_if () = + try kill_if () + with Sys.Break -> + let () = stop_waiting := true in + let () = TQueue.broadcast queue in + Worker.kill proc + in let _ = Thread.create kill_if () in try while true do -- cgit v1.2.3 From a11dd2209f47b6b79ace3d32071d29bd5652e07a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Mar 2016 15:16:02 +0100 Subject: Relying on Vernac classifier to flag tactics in the STM. --- stm/stm.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 07262ef68f..1d16d99b32 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1140,9 +1140,10 @@ end = struct (* {{{ *) let perform_states query = if query = [] then [] else - let is_tac = function - | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true - | _ -> false in + let is_tac e = match classify_vernac e with + | VtProofStep _, _ -> true + | _ -> false + in let initial = let rec aux id = try match VCS.visit id with { next } -> aux next -- cgit v1.2.3 From 5bce635ad876bde78a7ffabc3e781112e5418a65 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Mar 2016 23:56:22 +0100 Subject: Removing the dependency in VernacSolve in the STM. Instead of mangling the AST in order to interpret par: we remember the goal position to focus on it first and evaluate then the underlying vernacular expression. --- stm/stm.ml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 1d16d99b32..92032e9bc3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1414,7 +1414,7 @@ and TacTask : sig t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : ast; + t_ast : int * ast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1431,7 +1431,7 @@ end = struct (* {{{ *) t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : ast; + t_ast : int * ast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1440,7 +1440,7 @@ end = struct (* {{{ *) r_state : Stateid.t; r_state_fb : Stateid.t; r_document : VCS.vcs option; - r_ast : ast; + r_ast : int * ast; r_goal : Goal.goal; r_name : string } @@ -1484,6 +1484,9 @@ end = struct (* {{{ *) | Some { t_kill } -> t_kill () | _ -> () + let command_focus = Proof.new_focus_kind () + let focus_cond = Proof.no_cond command_focus + let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = Option.iter VCS.restore vcs; try @@ -1499,7 +1502,9 @@ end = struct (* {{{ *) Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin - vernac_interp r_state_fb r_ast; + let (i, ast) = r_ast in + Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); + vernac_interp r_state_fb ast; let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") @@ -1528,12 +1533,11 @@ end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } = - let e, etac, time, fail = + let e, time, fail = let rec find time fail = function - | VernacSolve(_,_,re,b) -> re, b, time, fail | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e | VernacFail e -> find time true e - | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in + | _ -> e, time, fail in find false false e in Hooks.call Hooks.with_fail fail (fun () -> (if time then System.with_time false else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> @@ -1545,8 +1549,7 @@ end = struct (* {{{ *) Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i) (State.exn_on id ~valid:safe_id) in - let t_ast = - { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in + let t_ast = (i, { verbose; loc; expr = e }) in let t_name = Goal.uid g in TaskQueue.enqueue_task queue ({ t_state = safe_id; t_state_fb = id; -- cgit v1.2.3 From ce2ffd090bd64963279cbbb84012d1b266ed9918 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 01:43:29 +0100 Subject: Moving VernacSolve to an EXTEND-based definition. --- stm/texmacspp.ml | 2 +- stm/vernac_classifier.ml | 2 -- 2 files changed, 1 insertion(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 3c4b8cb71e..a459cd65f8 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -671,7 +671,7 @@ let rec tmpp v loc = (* Solving *) - | (VernacSolve _ | VernacSolveExistential _) as x -> + | (VernacSolveExistential _) as x -> xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] (* Auxiliary file and library management *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f9f08f7afb..97d6e1fb71 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -102,12 +102,10 @@ let rec classify_vernac e = | VernacCheckMayEval _ -> VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater (* ProofStep *) - | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater | VernacProof _ | VernacBullet _ | VernacFocus _ | VernacUnfocus | VernacSubproof _ | VernacEndSubproof - | VernacSolve _ | VernacCheckGuard | VernacUnfocused | VernacSolveExistential _ -> VtProofStep false, VtLater -- cgit v1.2.3 From 0af598b77a6242d796c66884477a046448ef1e21 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 01:31:43 +0100 Subject: Moving Tactic Notation to an EXTEND based command. --- stm/texmacspp.ml | 3 --- stm/vernac_classifier.ml | 1 - 2 files changed, 4 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index a459cd65f8..e83313aa8e 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -503,9 +503,6 @@ let rec tmpp v loc = | VernacError _ -> xmlWithLoc loc "error" [] [] (* Syntax *) - | VernacTacticNotation _ as x -> - xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] - | VernacSyntaxExtension (_, ((_, name), sml)) -> let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in xmlReservedNotation attrs name loc diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 97d6e1fb71..41b753fb8b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -195,7 +195,6 @@ let rec classify_vernac e = | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ - | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -- cgit v1.2.3 From 4f52bd681ad9bbcbbd68406a58b47d8e962336ed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 02:23:21 +0100 Subject: Moving the Ltac definition command to an EXTEND based command. --- stm/texmacspp.ml | 1 - stm/vernac_classifier.ml | 7 ------- 2 files changed, 8 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index e83313aa8e..2d2ea1f8b0 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -694,7 +694,6 @@ let rec tmpp v loc = | VernacBackTo _ -> PCData "VernacBackTo" (* Commands *) - | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x | VernacCreateHintDb _ as x -> xmlTODO loc x | VernacRemoveHints _ as x -> xmlTODO loc x | VernacHints _ as x -> xmlTODO loc x diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 41b753fb8b..ecaf0fb7c5 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -173,13 +173,6 @@ let rec classify_vernac e = | VernacRegister _ | VernacNameSectionHypSet _ | VernacComments _ -> VtSideff [], VtLater - | VernacDeclareTacticDefinition l -> - let open Libnames in - let open Vernacexpr in - VtSideff (List.map (function - | TacticDefinition ((_,r),_) -> r - | TacticRedefinition (Ident (_,r),_) -> r - | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) -- cgit v1.2.3 From 7e7b5684d8f8066b90fca3395104af7241b8aed6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 25 Mar 2016 16:46:50 +0100 Subject: Univs: fix get_current_context (bug #4603, part I) Return an evar_map with the right universes, when there are no focused subgoals or the proof is finished. --- stm/lemmas.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index f06abfcce7..fb64a10c6c 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -511,5 +511,11 @@ let save_proof ?proof = function let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> - let env = Global.env () in - (Evd.from_env env, env) + try (* No more focused goals ? *) + let p = Pfedit.get_pftreestate () in + let evd = Proof.in_proof p (fun x -> x) in + (evd, Global.env ()) + with Proof_global.NoCurrentProof -> + let env = Global.env () in + (Evd.from_env env, env) + -- cgit v1.2.3