Email Gateway (Aug 18 2022 at 11:25): Email Gateway (Aug 18 2022 at 11:25):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
I have a long and complex tactic (long and complex meaning I started
work on it over a year ago, and I don't yet know whether it works on
more than one example).
But it does work on one example, in ML
(as in
Goal "..." ; byall ...tacs ; )
When I package it up as an Isar method, it doesn't work.
If it didn't work in ML I would do
val state = topthm()
and then go through the code step-by-step, to see where it fails.
Trying this in Isar, with the obligatory ML {* ... *} around each step,
gives
ML {* val state = topthm () *}
val state =
"PROP No_goal_has_been_supplied ==> PROP No_goal_has_been_supplied"
which obviously won't help.
How do I debug such a thing in Isar?
Jeremy
Email Gateway (Aug 18 2022 at 11:25):From: Alexander Krauss <krauss@in.tum.de>
Jeremy Dawson wrote:
I personally debug tactics consisting of several smaller tactics (all
written in ML) like this:
lemma "Some Goal"
apply (tactic "first_step_tac")
apply (tactic "next_step_tac")
apply (tactic "and_so_on")
...
Then I can step forward and back and modify the individual steps until I
get it right. Then I gradually compose the steps to larger parts until I
end up with a single tactic, which can be wrapped into a proper Isar method.
Alex
Email Gateway (Aug 18 2022 at 11:28):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Alexander Krauss wrote:
Dear Alex,
Thanks for your reply - as a matter of fact I did something like that,
to the point where I found the problem is in len_ty_tac. But len_ty_tac
isn't composed of smaller tactics, rather it looks at the subgoal and
goes from there, thus
fun len_ty_tac sg st =
let val cg = List.nth (cprems_of st, sg - 1) ;
val len_st = thin_len RSN (sg, st) ;
val len_cp = List.nth (cprems_of len_st, sg - 1) ;
(and so on)
regards,
Jeremy
Email Gateway (Aug 18 2022 at 11:28):From: Makarius <makarius@sketis.net>
For debugging you may use ML {* Isar.state () } or ML { Isar.goal () *}
to get full access to whatever state the toplevel is presently in.
Also note that the above List.nth method to access a particular subgoal is
a bit fragile, it just breaks if "sg" is out of range, while the usual
convention is to make the tactic fail with an empty result sequence. The
existing tacticals SUBGOAL and the newer CSUBGOAL will do the job for you.
Makarius
Last updated: May 03 2024 at 01:09 UTC