Email Gateway (Aug 18 2022 at 10:36): Email Gateway (Aug 18 2022 at 10:36):From: "Mark A. Hillebrand" <mah@dfki.de>
Hi all,
I have a really big and quite old Isabelle heap, which I use
regularly for regression testing a large collection of theories. Using
this heap, my attempt to load a specific theory breaks at a (permissive)
recdef with an exception trace and an error message [1]. If I start with
a fresh HOL heap and try to load the same theory, the permissive recdef
works without the exception trace and just leaves the error message in
the form of the (to-be-expected) warning [2] in the log. (In the theory,
just after the recdef, the termination condition is shown via
recdef_tc, but I do not think that matters here).
Naturally, while I could start out with a fresh heap to avoid the
error at least for some time, I would like to understand (and debug)
the reasons leading to this behaviour in the first place.
My guess is that side effects from loading the additional theories in
the big heap cause this behaviour. Also, the big heap might have
different global options set than the new one (like, as you see, [1] has
show_types turned on). I have tried to check the obvious things
(simpsets, quick_and_dirty, etc.), but now I am a bit at a loss how to
investigate further.
What other global settings might influence RecdefPackage in the
described way? How can I compare these settings easily for my two
heaps?
Are there any trace options for RecdefPackage which I could turn on?
Is it possible to print a list of all lemmas with attributes (not just
those with [simp] via `print_simpset (the_context());', but also for the
less used attributes)?
I use PolyML-5-based Isabelle-2005 on a 64-bit machine; system
resources should not be a problem in this case. Also, my experience is
that Isabelle works reliably with large heaps; so, I would for the
moment also exclude plain bit rot for my old heap.
Thanks for any hints!
Best regards,
Mark
1. ### Trying full Presburger arithmetic ...
Exception trace for exception - ERROR
Rules.prove(3)
Prim.postprocess(9)simplify_tc(3)
Prim.postprocess(9)loop(5)
Prim.postprocess(9)
Prim.postprocess(9)
Prim.postprocess(9)
Prim.postprocess(9)
Prim.postprocess(1)(1)(1)(1)
Tfl.proof_stage(11)
Tfl.simplify_defn(10)
Tfl.define_i(10)
Tfl.define(9)
RecdefPackage.gen_add_recdef(10)
o(2)(1)
Toplevel.theory(1)(1)
History.apply_copy(1)(1)(1)
End of trace
*** Bad final proof state:
*** ALL (T::nat) new_init_T::nat.
*** (EX (tinit::tom_conft) tinp::nat => tom_conf_inputt.
*** new_init_T = Suc (last_JISR_before T tinit tinp) &
*** exists_JISR_below T tinit tinp) -->
*** new_init_T < Suc T
*** 1. ALL (T::nat) new_init_T::nat.
*** (EX (tinit::tom_conft) tinp::nat => tom_conf_inputt.
*** new_init_T = Suc (last_JISR_before T tinit tinp) &
*** exists_JISR_below T tinit tinp) -->
*** new_init_T < Suc T
*** 1 unsolved goals!
*** Proof failed!
*** At command "recdef" (line 1086 of "/tmp/mah/TP2/verification/proof/VAMP/tomasulo_invs_with_interrupts.thy").
2. ### Trying full Presburger arithmetic ...
### Bad final proof state:
### ALL T new_init_T.
### (EX tinit tinp.
### new_init_T = Suc (last_JISR_before T tinit tinp) &
### exists_JISR_below T tinit tinp) -->
### new_init_T < Suc T
### 1. ALL T new_init_T.
### (EX tinit tinp.
### new_init_T = Suc (last_JISR_before T tinit tinp) &
### exists_JISR_below T tinit tinp) -->
### new_init_T < Suc T
### 1 unsolved goals!
### Proof failed!
Email Gateway (Aug 18 2022 at 10:40):From: Norbert Schirmer <schirmer@in.tum.de>
Hi Mark,
the problem is the debug-flag. If the debug flag is true, recdef does
no longer convert the exception to a warning (don't ask me why)
and hence the error reaches the toplevel.
Norbert
Last updated: May 03 2024 at 04:19 UTC