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
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?
On 2016-12-06 13:33, Andreas Lochbihler wrote:
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
This expression evaluates in Isabelle/ML almost immediately:
map (fn _ => tracing "Foo") (1 upto 1000)
This one apparently take forever:
map (fn _ => tracing "Foo") (1 upto 1001)
This archive was generated by a fusion of
Pipermail (Mailman edition) and