From b253e31a22024a5bb73b6fa707e6582b4034621b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Sep 2016 16:24:37 +0200 Subject: feedback: support multiple feedback listeners So that a module can add his own and look at the traffic --- stm/asyncTaskQueue.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 2d1f725ef0..49b51b1715 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -299,10 +299,12 @@ module Make(T : Task) = struct Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) let main_loop () = + (* We pass feedback to master *) let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback fb) []; flush oc in - Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); + Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); Feedback.set_logger Feedback.feedback_logger; + (* We ask master to allocate universe identifiers *) 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 47a2da7326ed975039f9e94780aeb9b1079f4854 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 5 Sep 2016 17:50:27 +0200 Subject: Fix #5065: Anomaly: Not a proof by induction Using abstract can create beta-redexes or let-ins in the head of the proof terms. The code projecting out mutual lemmas was not robust enough. --- stm/lemmas.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 40dbe2190b..ef304af3fe 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -249,10 +249,14 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, | Some body -> let body = norm body in let k = Kindops.logical_kind_of_goal_kind kind in - let body_i = match kind_of_term body with + let rec body_i t = match kind_of_term t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) + | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) + | App (t, args) -> mkApp (body_i t, args) | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in + let body_i = body_i body in match locality with | Discharge -> let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p -- cgit v1.2.3 From 5d25643afe3fe0428932e073a23ce3bafb3cb1b1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Sep 2016 12:57:59 +0200 Subject: STM: nested Abort is like nested Qed (fix #4756) There was an "optimization", since Abort is an empty side effect. But that optimization had an impact on the DAG shape. Now a nested proof, no matter if it is kept or dropped, is handled the same. --- 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 9f86597dce..160ca3b6a5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2358,7 +2358,7 @@ let merge_proof_branch ?valid ?id qast keep brname = let id = VCS.new_node ?id () in VCS.merge id ~ours:(Qed (qed None)) brname; VCS.delete_branch brname; - if keep <> VtDrop then VCS.propagate_sideff None; + VCS.propagate_sideff None; `Ok | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = -- cgit v1.2.3 From ea71f4d2abefd0c26c247268250aa9396f717ea8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Sep 2016 13:23:48 +0200 Subject: STM: sideff: report safe_id correctly (fix #4968) --- stm/stm.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 160ca3b6a5..e5902c0535 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2089,13 +2089,13 @@ let known_state ?(redefine_qed=false) ~cache id = 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 -> + let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); - reach id; + reach ~safe_id id; cherry_pick_non_pstate ()) id (* traverses the dag backward from nodes being already calculated *) - and reach ?(redefine_qed=false) ?(cache=cache) id = + and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin Hooks.(call state_computed id ~in_cache:true); @@ -2240,13 +2240,13 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true | `Sideff (`Id origin) -> (fun () -> reach view.next; - inject_non_pstate (pure_cherry_pick_non_pstate origin); + inject_non_pstate (pure_cherry_pick_non_pstate view.next origin); ), cache, true in let cache_step = if !Flags.async_proofs_cache = Some Flags.Force then `Yes else cache_step in - State.define + State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id -- cgit v1.2.3 From 83ec679e785f5313f088be77bcd652a29783623b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Sep 2016 15:07:43 +0200 Subject: STM: queries give back a dummy safe_id in case of error (#5041) --- 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 e5902c0535..ac24bfc492 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2471,12 +2471,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty {x with verbose = true } with e when CErrors.noncritical e -> let e = CErrors.push e in - iraise (State.exn_on report_id e)); `Ok + iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> (try vernac_interp report_id ~route x with e -> let e = CErrors.push e in - iraise (State.exn_on report_id e)); `Ok + iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (true,(report_id,_)), w -> assert(Stateid.equal report_id Stateid.dummy); let id = VCS.new_node ~id:newtip () in -- cgit v1.2.3 From 07db1a05ffc69a41687466da03ac04cb33348303 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Sep 2016 11:26:25 +0200 Subject: STM: if_verbose on "Checking task ..." (fix #4058) --- 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 ac24bfc492..cf9fa54922 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1437,8 +1437,8 @@ end = struct (* {{{ *) let check_task_aux extra name l i = let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in - msg_info( - str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); + Flags.if_verbose msg_info + (str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); VCS.restore document; let start = let rec aux cur = -- cgit v1.2.3