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