Re: [isabelle] Death by tracing



Interesting. Thanks.

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?

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?

Cheers,

Manuel


On 2016-12-06 13:33, Andreas Lochbihler wrote:
Hi Manuel,

This is not a death. Isabelle/jEdit suspends tracing after 1000 messages (you can request more with a button in the output buffer) unless you've changed the settings in the Isabelle plugin.

Andreas

On 06/12/16 12:34, Manuel Eberl wrote:
I should probably add that this is not a regression. Isabelle2015 and
Isabelle2016 show the exact same behaviour.

On 06/12/16 12:32, Manuel Eberl wrote:
Hallo,

I just noticed some odd behaviour and tracked it down to the following
minimal example:

This expression evaluates in Isabelle/ML almost immediately:

ML â
  map (fn _ => tracing "Foo") (1 upto 1000)
â

This one apparently take forever:

ML â
  map (fn _ => tracing "Foo") (1 upto 1001)
â

Cheers,

Manuel






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