[isabelle-dev] auto raises a TYPE exception

[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.


 	Makarius