[isabelle] Death by tracing



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.