[isabelle-dev] auto raises a TYPE exception
Johannes Hölzl
hoelzl at in.tum.de
Wed Apr 10 15:34:39 CEST 2013
Am Freitag, den 05.04.2013, 14:16 +0200 schrieb Makarius:
> On Fri, 5 Apr 2013, Johannes Hölzl wrote:
>
> > It looks like the problem is somewhere in the call to
> > Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML):
> >
> > ---- clasimp.ML ----
> >
> > fun nodup_depth_tac ctxt m i st =
> > SELECT_GOAL
> > (Classical.safe_steps_tac ctxt 1 THEN_ELSE
> > (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
> > Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
> > (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
> >
> > -----------------------
> >
> > Dmitriy and I tried to simplify the testcase by replicating the goal on
> > which inst0_step_tac is called but could not replicated the failure.
>
> > * How can I activate backtraces in ML to get an better understand of the
> > problem? I tried declare [[ML_trace = true]] but I didn't get a
> > backtrace.
>
> ML_trace is only for the static phase, to say what is the actual ML source
> after expanding antiquotations.
>
> In principle ML "Toplevel.debug := true" gives you an exception trace
> (only visible on "Raw Output"), but it is hidden behind lazy sequence
> evaluation here. So you should try the exception_trace combinator in the
> deeper parts of the ML code, where you suspect a problem.
Ah that's good to know!
Unfortunately, as you mentioned the excpetion_trace output is not very
helpful, all I see is Seq.make / .copy / .append. The inner functions
which call Envir.var_clash is not shown.
I checked Isabelle2012 and Isabelle2011, the exception happens also
there, so it is not special to Isabelle2013 or the development
repository.
- Johannes
---------------- 8< ----------------------------
theory Scratch
imports Main
begin
consts P :: "'a set => bool"
lemma P_Int [intro]: "P A ==> P B ==> P (A Int B)" sorry
lemma P_UNIV [intro]: "P UNIV" sorry
lemma P_INT [intro]: "ALL x : A. P (B x) ==> P (INT x : A. B x)" sorry
lemma P_UNION [intro]: "ALL x : A. P (B x) ==> P (UN x : A. B x)" sorry
lemma
fixes x :: "'a" and Q :: "'b => bool" and f :: "'a => 'b"
shows "EX S. P S & x : S & (ALL xa : S. Q (f xa))"
apply (auto simp only: )
More information about the isabelle-dev
mailing list