Re: [isabelle] debugging Isar



Jeremy Dawson wrote:
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

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.