OK, I'll respond to these points in-line.
A discussion without sources to look at is difficult.
OK, I attach my working version. Colleagues of mine were told off
recently for producing patches without the relevant authority, so these
days I begin these discussions in abstract. Feel free to tell me that
I'm doing it wrong some new way.
Generally, these hooks are rather old, predating the managed
evaluation of the PIDE document model. There used to be more hooks in
ancient times, but we have managed to get rid of most of them.
OK. I'm not familiar with the history. What I'm proposing is somewhat
orthogonal to the document model as I understand it though. Sure,
essential parts of the system/protocol should be built in rather than
"hooked" in. But rarely used add-on features can be more cleanly
supported by small "hooks" than by building e.g. mirabelle directly into
the system toplevel.
The general plan (for many years already) is to unify the batch build
mode further with the managed evaluation of PIDE interaction. In
particular there should be proper ways to fork (and maybe ignore)
proofs in the document model. Odd flags like skip_proofs or
quick_and_dirty/sorry might eventually disappear.
Such a consolidation might be nice, though obviously the performance
implications have to be managed. Some of these add-ons could perhaps
observe the proofs being done from the Isabelle/Scala side. Is that what
you're getting at? It sounds a bit involved.
As usual there is a conflict of proper principles done right, and
small adhoc patches to an already complex system.
However, doing things right seems to take a long time. Empirically,
fiddling with skip_proofs etc allows some users to see a 2-3x
improvement in their productivity. The question is just how official
this fiddling is allowed to be.
Cheers,
Thomas.
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
diff --git a/src/Pure/Isar/proof.ML b/src/Pure/Isar/proof.ML
index 961a582..9b158be 100644
--- a/src/Pure/Isar/proof.ML
+++ b/src/Pure/Isar/proof.ML
@@ -504,7 +504,11 @@ fun conclude_goal ctxt goal propss =
val finished_goal_error = "Failed to finish proof";
fun finished_goal pos state =
- let val (ctxt, (_, goal)) = get_goal state in
+ let
+ val (ctxt, (_, goal)) = get_goal state
+ val _ = if Thm.no_prems goal then Goal.run_finish_hooks
+ "Proof.finished_goal" ctxt goal else ()
+ in
if Thm.no_prems goal then Seq.Result state
else
Seq.Error (fn () =>
diff --git a/src/Pure/Isar/toplevel.ML b/src/Pure/Isar/toplevel.ML
index c31e3ce..b889b6f 100644
--- a/src/Pure/Isar/toplevel.ML
+++ b/src/Pure/Isar/toplevel.ML
@@ -459,7 +459,9 @@ fun begin_proof init = transaction (fn int =>
(fn Theory (gthy, _) =>
let
val (finish, prf) = init int gthy;
- val skip = Goal.skip_proofs_enabled ();
+ val skip = case try Proof.goal prf of NONE => false
+ | SOME goal => Goal.skip_goal "Toplevel.begin_proof"
+ (#context goal) (#goal goal)
val schematic_goal = try Proof.schematic_goal prf;
val _ =
if skip andalso schematic_goal = SOME true then
diff --git a/src/Pure/goal.ML b/src/Pure/goal.ML
index d0d3d74..fddbf5e 100644
--- a/src/Pure/goal.ML
+++ b/src/Pure/goal.ML
@@ -23,6 +23,10 @@ sig
val finish: Proof.context -> thm -> thm
val norm_result: Proof.context -> thm -> thm
val skip_proofs_enabled: unit -> bool
+ val skip_goal: string -> Proof.context -> thm -> bool
+ val add_skip_hook: (string -> Proof.context -> thm -> bool) -> unit
+ val add_finish_hook: (string -> Proof.context -> thm -> unit) -> unit
+ val run_finish_hooks: string -> Proof.context -> thm -> unit
val future_enabled: int -> bool
val future_enabled_timing: Time.time -> bool
val future_result: Proof.context -> thm future -> term -> thm
@@ -122,6 +126,24 @@ fun future_enabled_timing t =
future_enabled 1 andalso
Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
+val skip_hooks = Synchronized.var "Goal.skip_hooks"
+ ([] : (string -> Proof.context -> thm -> bool) list)
+
+fun add_skip_hook h = Synchronized.change skip_hooks (cons h)
+
+fun skip_goal nm ctxt thm = skip_proofs_enabled ()
+ orelse exists (fn h => try (h nm ctxt) thm = SOME true)
+ (Synchronized.value skip_hooks)
+
+val finish_hooks = Synchronized.var "Goal.finish_hooks"
+ ([] : (string -> Proof.context -> thm -> unit) list)
+
+fun add_finish_hook h = Synchronized.change finish_hooks (cons h)
+
+fun run_finish_hooks nm ctxt thm = List.app (fn f => (try (f nm ctxt) thm; ()))
+ (Synchronized.value finish_hooks)
+
+fun finish_hook_tac nm ctxt t = (run_finish_hooks nm ctxt t; Seq.single t)
(* future_result *)
@@ -181,7 +203,8 @@ fun prove_common ctxt fork_pri xs asms props tac =
val schematic = exists is_schematic props;
val immediate = is_none fork_pri;
val future = future_enabled 1;
- val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
+ fun skip ctxt goal = not immediate andalso not schematic andalso future
+ andalso skip_goal "Goal.prove" ctxt goal;
val pos = Position.thread_data ();
fun err msg =
@@ -204,8 +227,9 @@ fun prove_common ctxt fork_pri xs asms props tac =
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops);
fun tac' args st =
- if skip then ALLGOALS (Skip_Proof.cheat_tac ctxt) st before Skip_Proof.report ctxt
- else tac args st;
+ if skip (#context args) st
+ then ALLGOALS (Skip_Proof.cheat_tac ctxt) st before Skip_Proof.report ctxt
+ else (tac args THEN finish_hook_tac "Goal.prove" (#context args)) st
fun result () =
(case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of
NONE => err "Tactic failed"
@@ -226,7 +250,8 @@ fun prove_common ctxt fork_pri xs asms props tac =
else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
end);
val res =
- if immediate orelse schematic orelse not future orelse skip then result ()
+ if immediate orelse schematic orelse not future
+ orelse skip_proofs_enabled () then result ()
else
future_result ctxt'
(Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri}
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
