Re: [isabelle] Death by tracing



> Well, I now understand that it makes sense that no more than 1000
> tracing messages are output, but is it also intended behaviour that I
> never actually get any result in ML, i.e. that too much tracing seems to
> stop evaluation?

Yes.

> I noticed this problem when I proved 1024 theorems with the
> âapproximationâ method, which outputs one line of tracing information
> every time. Does this mean that âapproximationâ shouldn't be using
> âtracingâ to output this information?

Probably not by default, or at least with the option to disable it.

Cheers
Lars




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