Re: [isabelle] debugging Isar

Alexander Krauss 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.

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)



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