diff options
| -rw-r--r-- | lib/future.ml | 14 | ||||
| -rw-r--r-- | lib/future.mli | 16 | ||||
| -rw-r--r-- | stm/stm.ml | 45 | ||||
| -rw-r--r-- | test-suite/interactive/ParalITP_fail_on_qed.v | 54 | ||||
| -rw-r--r-- | vernac/declare.ml | 41 | ||||
| -rw-r--r-- | vernac/declare.mli | 9 |
6 files changed, 97 insertions, 82 deletions
diff --git a/lib/future.ml b/lib/future.ml index 661637fcd1..23d089fb6b 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -67,8 +67,8 @@ and 'a computation = 'a comput ref let unnamed = "unnamed" -let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = - ref (Ongoing (name, CEphemeron.create (uuid, f, ref x))) +let create ?(name=unnamed) ?(uuid=UUID.fresh ()) ~fix_exn x = + ref (Ongoing (name, CEphemeron.create (uuid, fix_exn, ref x))) let get x = match !x with | Finished v -> unnamed, UUID.invalid, id, ref (Val v) @@ -97,9 +97,7 @@ let peek_val kx = let _, _, _, x = get kx in match !x with let uuid kx = let _, id, _, _ = get kx in id -let from_val ?(fix_exn=id) v = create fix_exn (Val v) - -let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn +let from_val v = create ~fix_exn:id (Val v) let create_delegate ?(blocking=true) ~name fix_exn = let assignment signal ck = fun v -> @@ -116,7 +114,7 @@ let create_delegate ?(blocking=true) ~name fix_exn = let cond = Condition.create () in (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in - let ck = create ~name fix_exn (Delegated wait) in + let ck = create ~name ~fix_exn (Delegated wait) in ck, assignment signal ck (* TODO: get rid of try/catch to be stackless *) @@ -143,12 +141,12 @@ let force x = match compute x with let chain ck f = let name, uuid, fix_exn, c = get ck in - create ~uuid ~name fix_exn (match !c with + create ~uuid ~name ~fix_exn (match !c with | Closure _ | Delegated _ -> Closure (fun () -> f (force ck)) | Exn _ as x -> x | Val v -> Val (f v)) -let create fix_exn f = create fix_exn (Closure f) +let create ~fix_exn f = create ~fix_exn (Closure f) let replace kx y = let _, _, _, x = get kx in diff --git a/lib/future.mli b/lib/future.mli index 7a85c37970..612a67f962 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -47,21 +47,11 @@ type fix_exn = Exninfo.iexn -> Exninfo.iexn by forcing the computations or any computation that is chained after it. It is used by STM to attach errors to their corresponding states, and to communicate to the code catching the exception a valid state id. *) -val create : fix_exn -> (unit -> 'a) -> 'a computation +val create : fix_exn:fix_exn -> (unit -> 'a) -> 'a computation (* Usually from_val is used to create "fake" futures, to use the same API - as if a real asynchronous computations was there. In this case fixing - the exception is not needed, but *if* the future is chained, the fix_exn - argument should really be given *) -val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation - -(* To get the fix_exn of a computation and build a Lemmas.declaration_hook. - * When a future enters the environment a corresponding hook is run to perform - * some work. If this fails, then its failure has to be annotated with the - * same state id that corresponds to the future computation end. I.e. Qed - * is split into two parts, the lazy one (the future) and the eager one - * (the hook), both performing some computations for the same state id. *) -val fix_exn_of : 'a computation -> fix_exn + as if a real asynchronous computations was there. *) +val from_val : 'a -> 'a computation (* Run remotely, returns the function to assign. If not blocking (the default) it raises NotReady if forced before the diff --git a/stm/stm.ml b/stm/stm.ml index 04f08e488b..b72cee7a9d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -830,8 +830,6 @@ module State : sig ?redefine:bool -> ?cache:bool -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit - val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref - val install_cached : Stateid.t -> unit (* val install_parsing_state : Stateid.t -> unit *) val is_cached : ?cache:bool -> Stateid.t -> bool @@ -865,8 +863,6 @@ 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) - let freeze () = { id = !cur_id; vernac_state = Vernacstate.freeze_interp_state ~marshallable:false } let unfreeze st = Vernacstate.unfreeze_interp_state st.vernac_state; @@ -1001,10 +997,7 @@ end = struct (* {{{ *) try stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ if cache then "Y)" else "N)"); - let good_id = match safe_id with None -> !cur_id | Some id -> id in - fix_exn_ref := exn_on id ~valid:good_id; f (); - fix_exn_ref := (fun x -> x); if cache then cache_state ~marshallable:false id; stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; @@ -1495,7 +1488,9 @@ end = struct (* {{{ *) feedback (InProgress ~-1) let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop = - Future.create (State.exn_on id ~valid) (fun () -> + (* [~fix_exn:exn_on] here does more than amending the exn + information, it also updates the STM state *) + Future.create ~fix_exn:(State.exn_on id ~valid) (fun () -> let wall_clock1 = Unix.gettimeofday () in Reach.known_state ~doc ~cache:(VCS.is_interactive ()) eop; let wall_clock2 = Unix.gettimeofday () in @@ -1509,38 +1504,45 @@ end = struct (* {{{ *) try VCS.restore document; VCS.print (); - let proof, future_proof, time = + let proof, time = let wall_clock = Unix.gettimeofday () in let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_info stop in let proof = Future.force fp in - proof, fp, Unix.gettimeofday () -. wall_clock in + proof, Unix.gettimeofday () -. wall_clock in (* We typecheck the proof with the kernel (in the worker) to spot * the few errors tactics don't catch, like the "fix" tactic building * a bad fixpoint *) - let fix_exn = Future.fix_exn_of future_proof in (* STATE: We use the current installed imperative state *) let st = State.freeze () in if not drop then begin - let checked_proof = Future.chain future_proof (fun p -> - - (* Unfortunately close_future_proof and friends are not pure so we need - to set the state manually here *) + (* Unfortunately close_future_proof and friends are not pure so we need + to set the state manually here *) State.unfreeze st; let pobject, _info = - PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in + PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in let st = Vernacstate.freeze_interp_state ~marshallable:false in let opaque = Declare.Opaque in - stm_qed_delay_proof ~st ~id:stop - ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in - ignore(Future.join checked_proof); - end; + try + let _pstate = + stm_qed_delay_proof ~st ~id:stop + ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in + () + with exn -> + (* If [stm_qed_delay_proof] fails above we need to use the + exn callback in the same way than build_proof_here; + actually [fix_exn] there does more more than just + modifying exn info, it also updates the STM state *) + let iexn = Exninfo.capture exn in + let iexn = State.exn_on (fst exn_info) ~valid:(snd exn_info) iexn in + Exninfo.iraise iexn + end; (* STATE: Restore the state XXX: handle exn *) State.unfreeze st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> - let (e, info) = Exninfo.capture e in + let e, info = Exninfo.capture e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) let e_error_at, e_safe_id = match Stateid.get info with @@ -3310,7 +3312,6 @@ let unreachable_state_hook = Hooks.unreachable_state_hook let document_add_hook = Hooks.document_add_hook let document_edit_hook = Hooks.document_edit_hook let sentence_exec_hook = Hooks.sentence_exec_hook -let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () diff --git a/test-suite/interactive/ParalITP_fail_on_qed.v b/test-suite/interactive/ParalITP_fail_on_qed.v new file mode 100644 index 0000000000..37692ed254 --- /dev/null +++ b/test-suite/interactive/ParalITP_fail_on_qed.v @@ -0,0 +1,54 @@ +(* Some boilerplate *) +Fixpoint fib n := match n with + | O => 1 + | S m => match m with + | O => 1 + | S o => fib o + fib m end end. + +Ltac sleep n := + try (cut (fib n = S (fib n)); reflexivity). + +(* Tune that depending on your PC *) +Let time := 10. + + +(* Beginning of demo *) + +Section Demo. + +Variable i : True. + +Lemma a (n : nat) : nat. +Proof using. + revert n. + fix f 1. + apply f. +Qed. + +Lemma b : True. +Proof using i. + sleep time. + idtac. + sleep time. + (* Here we use "a" *) + exact I. +Qed. + +Lemma work_here : True /\ True. +Proof using i. +(* Jump directly here, Coq reacts immediately *) +split. + exact b. (* We can use the lemmas above *) +exact I. +Qed. + +End Demo. + +From Coq Require Import Program.Tactics. +Obligation Tactic := idtac. +Program Definition foo : nat -> nat * nat := + fix f (n : nat) := (0,_). + +Next Obligation. +intros f n; apply (f n). +Qed. diff --git a/vernac/declare.ml b/vernac/declare.ml index e3144b2d24..59922c662a 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -140,9 +140,9 @@ let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty (** [univsbody] are universe-constraints attached to the body-only, used in vio-delayed opaque constants and private poly universes *) -let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types +let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); + { proof_entry_body = Future.from_val ((body,univsbody), eff); proof_entry_secctx = section_vars; proof_entry_type = types; proof_entry_universes = univs; @@ -151,7 +151,7 @@ let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id proof_entry_inline_code = inline} let definition_entry = - definition_entry_core ?fix_exn:None ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None + definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None type proof_object = { name : Names.Id.t @@ -369,9 +369,9 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types +let pure_definition_entry ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ()); + { proof_entry_body = Future.from_val ((body,Univ.ContextSet.empty), ()); proof_entry_secctx = None; proof_entry_type = types; proof_entry_universes = univs; @@ -504,17 +504,6 @@ let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = register_constant kn kind local in kn -let get_cd_fix_exn = function - | DefinitionEntry de -> - Future.fix_exn_of de.proof_entry_body - | _ -> fun x -> x - -let declare_constant ?local ~name ~kind cd = - try declare_constant ?local ~name ~kind cd - with exn -> - let exn = Exninfo.capture exn in - Exninfo.iraise (get_cd_fix_exn cd exn) - let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de = let kn, eff = let de = @@ -1010,29 +999,22 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in dref -let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = - try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe - with exn -> - let exn = Exninfo.capture exn in - let exn = Option.cata (fun fix -> fix exn) exn fix_exn in - Exninfo.iraise exn - (* Preparing proof entries *) -let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma = +let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma = let env = Global.env () in Pretyping.check_evars_are_solved ~program_mode:false env sigma; let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in - let entry = definition_entry_core ?fix_exn ?opaque ?inline ?types ~univs body in + let entry = definition_entry ?opaque ?inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in entry, uctx let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook - ~obls ~poly ?inline ~types ~body ?fix_exn sigma = - let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in + ~obls ~poly ?inline ~types ~body sigma = + let entry, uctx = prepare_definition ~opaque ~poly ~udecl ~types ~body ?inline sigma in declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry let declare_definition = declare_definition_core ~obls:[] @@ -1454,8 +1436,6 @@ let subst_prog subst prg = ( Vars.replace_vars subst' prg.prg_body , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) -let stm_get_fix_exn = ref (fun _ x -> x) - let declare_definition prg = let varsubst = obligation_substitution true prg in let sigma = Evd.from_ctx prg.prg_ctx in @@ -1471,12 +1451,11 @@ let declare_definition prg = , Decls.(IsDefinition prg.prg_kind) , prg.prg_implicits ) in - let fix_exn = !stm_get_fix_exn () in let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) let kn = declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls - ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma + ~opaque ~poly ~udecl ~types ~body sigma in let pm = progmap_remove !State.prg_ref prg in State.prg_ref := pm; diff --git a/vernac/declare.mli b/vernac/declare.mli index ef4f8c4825..979bdd4334 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -305,13 +305,11 @@ val declare_definition -> ?inline:bool -> types:EConstr.t option -> body:EConstr.t - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> Evd.evar_map -> GlobRef.t val declare_assumption - : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> name:Id.t + : name:Id.t -> scope:locality -> hook:Hook.t option -> impargs:Impargs.manual_implicits @@ -495,11 +493,6 @@ val obl_substitution : val dependencies : Obligation.t array -> int -> Int.Set.t -(* This is a hack to make it possible for Obligations to craft a Qed - * behind the scenes. The fix_exn the Stm attaches to the Future proof - * is not available here, so we provide a side channel to get it *) -val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref - end (** Creating high-level proofs with an associated constant *) |