Re: [isabelle] Death by tracing

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.


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:

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)



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