asmrefine: improve initial debugging experience.
Adds a 'debug' configuration type to the main ProveSimplToGraphGoals functions. Configuration lets the user control which functions will be tested, and logs which functions fail testing. Adds a 'single step' debug tactic for use in TestGraphRefine, and demonstrates a few useful initial ML tactic for e.g. narrowing down which subgoals are failing, and how to inspect a successful subgoal.
This commit is contained in:
parent
67bba7edc3
commit
f067068a88
|
@ -68,8 +68,17 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]:
|
||||||
(* If this fails, it can be debugged with the assistance of the
|
(* If this fails, it can be debugged with the assistance of the
|
||||||
script in TestGraphRefine.thy *)
|
script in TestGraphRefine.thy *)
|
||||||
|
|
||||||
ML \<open>ProveSimplToGraphGoals.test_all_graph_refine_proofs_parallel
|
ML \<open>
|
||||||
funs (csenv ()) @{context}\<close>
|
val dbg = ProveSimplToGraphGoals.new_debug [] [];
|
||||||
|
|
||||||
|
ProveSimplToGraphGoals.test_all_graph_refine_proofs_parallel
|
||||||
|
funs (csenv ()) @{context} dbg;
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
ML \<open>
|
||||||
|
ProveSimplToGraphGoals.print dbg #failures
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
|
@ -63,28 +63,6 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]:
|
||||||
"snd (snd ((if P then f else g) gs)) = (if P then snd (snd (f gs)) else snd (snd (g gs)))"
|
"snd (snd ((if P then f else g) gs)) = (if P then snd (snd (f gs)) else snd (snd (g gs)))"
|
||||||
by (simp_all add: gs_new_frames_def gs_new_cnodes_def gs_clear_region_def)
|
by (simp_all add: gs_new_frames_def gs_new_cnodes_def gs_clear_region_def)
|
||||||
|
|
||||||
(* ML {* ProveSimplToGraphGoals.test_all_graph_refine_proofs_after
|
|
||||||
funs (csenv ()) @{context} NONE *} *)
|
|
||||||
|
|
||||||
ML \<open>val nm = "Kernel_C.idle_thread"\<close>
|
|
||||||
|
|
||||||
local_setup \<open>define_graph_fun_short funs nm\<close>
|
|
||||||
|
|
||||||
ML \<open>
|
|
||||||
val hints = SimplToGraphProof.mk_hints funs @{context} nm
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
ML \<open>
|
|
||||||
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs hints nm
|
|
||||||
@{context}
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
declare [[show_types]]
|
|
||||||
|
|
||||||
ML \<open>
|
|
||||||
ProveSimplToGraphGoals.simpl_to_graph_thm funs (csenv ()) @{context} nm;
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
ML \<open>
|
ML \<open>
|
||||||
val tacs = ProveSimplToGraphGoals.graph_refine_proof_tacs (csenv ())
|
val tacs = ProveSimplToGraphGoals.graph_refine_proof_tacs (csenv ())
|
||||||
#> map snd
|
#> map snd
|
||||||
|
@ -94,12 +72,70 @@ val full_goal_tac = ProveSimplToGraphGoals.graph_refine_proof_full_goal_tac
|
||||||
(csenv ())
|
(csenv ())
|
||||||
val debug_tac = ProveSimplToGraphGoals.debug_tac
|
val debug_tac = ProveSimplToGraphGoals.debug_tac
|
||||||
(csenv ())
|
(csenv ())
|
||||||
|
val debug_step_tac = ProveSimplToGraphGoals.debug_step_tac
|
||||||
|
(csenv ())
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
\<comment>\<open> Name of the C function to investigate. \<close>
|
||||||
|
ML \<open>
|
||||||
|
val nm = "Kernel_C.merge_regions"
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
local_setup \<open>define_graph_fun_short funs nm\<close>
|
||||||
|
|
||||||
|
ML \<open>
|
||||||
|
val hints = SimplToGraphProof.mk_hints funs @{context} nm
|
||||||
|
val init_thm =
|
||||||
|
SimplToGraphProof.simpl_to_graph_upto_subgoals funs hints nm @{context}
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
declare [[show_types]]
|
||||||
|
declare [[goals_limit = 100]]
|
||||||
|
|
||||||
|
\<comment>\<open>
|
||||||
|
Investigate the failure.
|
||||||
|
\<close>
|
||||||
schematic_goal "PROP ?P"
|
schematic_goal "PROP ?P"
|
||||||
apply (tactic \<open>resolve_tac @{context} [init_thm] 1\<close>)
|
apply (tactic \<open>resolve_tac @{context} [init_thm] 1\<close>)
|
||||||
|
|
||||||
apply (tactic \<open>ALLGOALS (debug_tac @{context})\<close>)
|
\<comment>\<open>
|
||||||
|
Apply the "all steps" debug tactic to every goal, but restore any
|
||||||
|
unproven goals.
|
||||||
|
\<close>
|
||||||
|
apply (all \<open>(solves \<open>tactic \<open>HEADGOAL (debug_tac @{context})\<close>\<close>)?\<close>)
|
||||||
|
|
||||||
|
\<comment>\<open> Lets us edit the next lines without re-running the above line. \<close>
|
||||||
|
apply (tactic \<open>all_tac\<close>)
|
||||||
|
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 1)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 2)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 3)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 4)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 5)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 6)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 7)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 8)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 9)\<close>)
|
||||||
|
oops
|
||||||
|
|
||||||
|
\<comment>\<open>
|
||||||
|
Extract a "working" part of the proof, to get a feel for what each step does.
|
||||||
|
\<close>
|
||||||
|
schematic_goal "PROP ?P"
|
||||||
|
apply (tactic \<open>resolve_tac @{context} [init_thm] 1\<close>)
|
||||||
|
|
||||||
|
\<comment>\<open> `Goal.restrict x 1` selects subgoal `x`. \<close>
|
||||||
|
apply (tactic \<open>PRIMITIVE (Goal.restrict 43 1)\<close>)
|
||||||
|
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 1)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 2)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 3)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 4)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 5)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 6)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 7)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 8)\<close>)
|
||||||
|
apply (tactic \<open>HEADGOAL (debug_step_tac @{context} 9)\<close>)
|
||||||
oops
|
oops
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -847,6 +847,13 @@ fun debug_tac csenv ctxt = let
|
||||||
| SOME t' => ((fn _ => fn _ => all_tac t') THEN_ALL_NEW wrap_tacs tacs) i t
|
| SOME t' => ((fn _ => fn _ => all_tac t') THEN_ALL_NEW wrap_tacs tacs) i t
|
||||||
in wrap_tacs tacs end
|
in wrap_tacs tacs end
|
||||||
|
|
||||||
|
fun debug_step_tac csenv ctxt step = let
|
||||||
|
val tac = nth (graph_refine_proof_tacs csenv ctxt) (step - 1)
|
||||||
|
fun wrap_tac (nms, tac) i t = case try (tac i #> Seq.hd) t
|
||||||
|
of NONE => (warning ("step failed: " ^ commas nms); all_tac t)
|
||||||
|
| SOME t' => all_tac t'
|
||||||
|
in wrap_tac tac end
|
||||||
|
|
||||||
fun simpl_to_graph_thm funs csenv ctxt nm = let
|
fun simpl_to_graph_thm funs csenv ctxt nm = let
|
||||||
val hints = SimplToGraphProof.mk_hints funs ctxt nm
|
val hints = SimplToGraphProof.mk_hints funs ctxt nm
|
||||||
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs hints nm
|
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs hints nm
|
||||||
|
@ -870,29 +877,76 @@ fun test_graph_refine_proof funs csenv ctxt nm = case
|
||||||
in (succ ^ nm, res_thm) end handle TERM (s, ts) => raise TERM ("test_graph_refine_proof: " ^ nm
|
in (succ ^ nm, res_thm) end handle TERM (s, ts) => raise TERM ("test_graph_refine_proof: " ^ nm
|
||||||
^ ": " ^ s, ts)
|
^ ": " ^ s, ts)
|
||||||
|
|
||||||
|
\<comment>\<open>
|
||||||
|
Utility for configuring SimplToGraphProof with debugging failures.
|
||||||
|
\<close>
|
||||||
|
type debug = {
|
||||||
|
\<comment>\<open> Functions with these names won't be tested. \<close>
|
||||||
|
skips: string list,
|
||||||
|
\<comment>\<open> If non-empty, *only* functions with these names will be tested. \<close>
|
||||||
|
only: string list,
|
||||||
|
|
||||||
fun test_graph_refine_proof_with_def funs csenv ctxt nm = case
|
\<comment>\<open>
|
||||||
Symtab.lookup funs nm of SOME (_, _, NONE) => "skipped " ^ nm
|
Logs the names of functions when they pass or fail tests, or are
|
||||||
| _ => let
|
skipped because they don't have a definition.
|
||||||
val ctxt = define_graph_fun_short funs nm ctxt
|
\<close>
|
||||||
val (time, _) = Timing.timing (simpl_to_graph_thm funs csenv ctxt) nm
|
new_skips: (string list) Unsynchronized.ref,
|
||||||
in "success on " ^ nm ^ " [" ^ Timing.message time ^ "]" end
|
successes: (string list) Unsynchronized.ref,
|
||||||
|
failures: (string list) Unsynchronized.ref
|
||||||
|
}
|
||||||
|
|
||||||
fun test_all_graph_refine_proofs_after funs csenv ctxt nm = let
|
fun new_debug skips only: debug = {
|
||||||
|
skips = skips,
|
||||||
|
only = only,
|
||||||
|
new_skips = Unsynchronized.ref [],
|
||||||
|
successes = Unsynchronized.ref [],
|
||||||
|
failures = Unsynchronized.ref []
|
||||||
|
}
|
||||||
|
|
||||||
|
fun insert (dbg: debug) field x = change (field dbg) (curry (op ::) x)
|
||||||
|
|
||||||
|
fun filter_fns (dbg: debug) =
|
||||||
|
(if null (#only dbg) then I else filter (member (op =) (#only dbg))) #>
|
||||||
|
(if null (#skips dbg) then I else filter_out (member (op =) (#skips dbg)))
|
||||||
|
|
||||||
|
fun has_failures (dbg: debug) = not (null (! (#failures dbg)))
|
||||||
|
|
||||||
|
fun print (dbg: debug) field = (writeln "failures:"; map writeln (! (field dbg)))
|
||||||
|
|
||||||
|
fun test_graph_refine_proof_with_def funs csenv ctxt dbg nm =
|
||||||
|
case Symtab.lookup funs nm of
|
||||||
|
SOME (_, _, NONE) => (insert dbg #new_skips nm; "skipped " ^ nm)
|
||||||
|
| _ =>
|
||||||
|
let
|
||||||
|
val ctxt = define_graph_fun_short funs nm ctxt
|
||||||
|
fun try_proof nm =
|
||||||
|
(simpl_to_graph_thm funs csenv ctxt nm; insert dbg #successes nm)
|
||||||
|
handle TERM (message, data) =>
|
||||||
|
(insert dbg #failures nm; raise TERM ("failure for " ^ nm ^ ": " ^ message, data));
|
||||||
|
val (time, _) = Timing.timing try_proof nm
|
||||||
|
in "success on " ^ nm ^ " [" ^ Timing.message time ^ "]" end
|
||||||
|
|
||||||
|
fun test_all_graph_refine_proofs_after funs csenv ctxt dbg nm = let
|
||||||
val ss = Symtab.keys funs
|
val ss = Symtab.keys funs
|
||||||
val n = case nm of NONE => ~1 | SOME nm' => find_index (fn s => s = nm') ss
|
val n = case nm of NONE => ~1 | SOME nm' => find_index (fn s => s = nm') ss
|
||||||
val ss = if n = ~1 then ss else drop (n + 1) ss
|
val ss = if n = ~1 then ss else drop (n + 1) ss
|
||||||
val err = prefix "ERROR for: " #> error
|
val err = prefix "ERROR for: " #> error
|
||||||
val _ = map (fn s => (writeln ("testing: " ^ s);
|
val _ = map (fn s => (writeln ("testing: " ^ s);
|
||||||
writeln (test_graph_refine_proof_with_def funs csenv ctxt s))
|
writeln (test_graph_refine_proof_with_def funs csenv ctxt dbg s))
|
||||||
handle TERM _ => err s | TYPE _ => err s | THM _ => err s) ss
|
handle TERM _ => err s | TYPE _ => err s | THM _ => err s) ss
|
||||||
in "success" end
|
in "success" end
|
||||||
|
|
||||||
fun test_all_graph_refine_proofs_parallel funs csenv ctxt = let
|
fun test_all_graph_refine_proofs_parallel funs csenv ctxt dbg = let
|
||||||
val ss = Symtab.keys funs
|
val ss = Symtab.keys funs |> filter_fns dbg
|
||||||
val _ = Par_List.map (test_graph_refine_proof_with_def funs csenv ctxt
|
fun test_and_log nm =
|
||||||
#> writeln) ss
|
(test_graph_refine_proof_with_def funs csenv ctxt dbg nm |> writeln)
|
||||||
in "success" end
|
handle TERM (msg, _) => warning msg
|
||||||
|
val _ = Par_List.map test_and_log ss
|
||||||
|
in
|
||||||
|
if has_failures dbg
|
||||||
|
then error "Failures! Check the ProveSimplToGraphGoals.failures variable."
|
||||||
|
else "success!"
|
||||||
|
end
|
||||||
|
|
||||||
end
|
end
|
||||||
\<close>
|
\<close>
|
||||||
|
|
Loading…
Reference in New Issue