On Thu, 9 Jun 2011, Lawrence Paulson wrote:
I see you are alert, as always!
Just the normal process of consuming incoming mails and changesets ... :-)
But here there were two reasons for extra attention: (1) suspicious
keywords in the log entry (like "fixed" or "bug") and (2) a realistic
chance that I broke this myself in recent reworking of blast (a relatively
simple case of the still ongoing "localisation" effort).
In this particular case, it's pretty clear that the exception was raised
here, in conv.ML:
fun gconv_rule cv i th =
(case try (Thm.cprem_of th) i of
SOME ct =>
let val eq = cv ct in
if Thm.is_reflexive eq then th
else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
end
| NONE => raise THM ("gconv_rule", i, [th]));
And this was in conformance with a common use of exception THM, namely
to indicate that the designated subgoal did not exist. So a tactic
calling this code should indeed catch the exception and indicate failure
by returning the empty sequence.
Yes, formally timing_depth_tac was always wrong in that sense as a tactic.
I have learned the requirements for proper tactics from you many years ago
(they are now documented in the implementation manual). Normally the
CONVERSION tactical would convert the failure of the conversion (e.g. via
exception THM) into proper Seq.empty for the tactic, but it was not used
here for other reasons.
Just some weeks ago I inspected the code again, and convinced myself that
the DEEPEN around timing_depth_tac "repairs" this feature. Unfortunately
I've overlooked the special side-entry Blast.depth_tac, which bypasses
DEEPEN. So historically the problem was actually introduced in 1997 here
http://isabelle.in.tum.de/repos/isabelle/rev/cc3e8453d7f0 when the public
Blast.depth_tac was added as new feature.
Did anybody actually understand the source of the problem?
In summary the situation is like that: blast with explicit depth limit did
not check subgoal bounds properly. The problem can be reproduced like
that (e.g. in Isabelle2011):
lemma True
apply rule
apply (blast 5)
*** exception THM 1 raised (line 212 of "conv.ML"): gconv_rule
*** At command "apply" (line 7 of "/home/makarius/Scratch.thy")
Without that extra argument it is deepened from 1 .. 20. Since Andreas
had explicit 25 to get beyond that, he might consider using
[[blast_depth_limit = 30]] or similar to get the incremental effect to
higher limits, although there could be a general slowdown up there.
See also http://isabelle.in.tum.de/repos/isabelle/rev/01f051619eee for
some further cleanup of blast.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
