On Thu, 21 Nov 2013, Tobias Nipkow wrote:
Some such effects may indeed play a role, although I originally did not observe
it when reloading a theory but while editing an existing theory.
Apart from timing problems there might be some internal breakdown of auto
tools that is not seen, because exceptions are absorbed. (This behaviour
is the same for the traditional TTY mode of auto tools.)
To help diagnose this possibility, the included change produces explicit
spam via warning messages. You can use "hg import --no-commit" to
experiment with it locally (based on the development repository).
If this yields any insights, we can think about doing something for the
release branch.
Makarius
# HG changeset patch
# User wenzelm
# Date 1385044067 -3600
# Node ID c22608a2df88cf5461192e14a37a623065d4b29a
# Parent 483131676087620895373bcdd5b465c8747effb2
test;
diff -r 483131676087 -r c22608a2df88 src/Tools/try.ML
--- a/src/Tools/try.ML Wed Nov 20 23:14:06 2013 +0100
+++ b/src/Tools/try.ML Thu Nov 21 15:27:47 2013 +0100
@@ -131,9 +131,11 @@
val auto_time_limit = Options.default_real @{option
auto_time_limit}
in
if auto_time_limit > 0.0 then
- (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () =>
tool true state) () of
- (true, (_, state')) =>
+ (case (Exn.interruptible_capture o TimeLimit.timeLimit
(seconds auto_time_limit))
+ (fn () => tool true state) () of
+ Exn.Res (true, (_, state')) =>
List.app Pretty.writeln (Proof.pretty_goal_messages state')
+ | Exn.Exn exn => warning (ML_Compiler.exn_message exn)
| _ => ())
else ()
end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
