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: ) _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
