Email Gateway (Aug 22 2022 at 14:47): Email Gateway (Aug 22 2022 at 14:47):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 14:47):From: Manuel Eberl <eberlm@in.tum.de>
I should probably add that this is not a regression. Isabelle2015 and
Isabelle2016 show the exact same behaviour.
Email Gateway (Aug 22 2022 at 14:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 14:48):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 14:48):From: Lars Hupel <hupel@in.tum.de>
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
Email Gateway (Aug 22 2022 at 14:48):From: Manuel Eberl <eberlm@in.tum.de>
I spoke to Johannes about it and he agreed it would be best to just
remove that output. Since I have an AFP entry in preparation that relies
on approximation_tac, it would be good if this could make it into the
release.
The attached patch should take care of it. (I also attached a bundle,
but I never used those before so I don't know if I did it correctly)
Cheers,
Manuel
approximation.diff
isabelle_release_approximation.bundle
Email Gateway (Aug 22 2022 at 14:48):From: Makarius <makarius@sketis.net>
Tracing is in some sense debugging, and that should have an option to
enable it, i.e. it should be disabled by default.
We have a long record of really strange effects caused by tools
producing "potentially useful output" by default. I put that phrase into
quotes, because it is a technical term of Isabelle lore.
These effects might be technical (e.g. bombing the front-end) or
psychological (e.g. tons of irrelevant messages hiding one important
message that indicates an error, which is then overlooked).
Makarius
Email Gateway (Aug 22 2022 at 14:48):From: Makarius <makarius@sketis.net>
OK, see
https://bitbucket.org/isabelle_project/isabelle-release/commits/a955511171a8
(It will come back to isabelle-dev within a few days.)
Makarius
Last updated: Apr 27 2024 at 01:05 UTC