*To*: "Mark A. Hillebrand" <mah at dfki.de>*Subject*: Re: [isabelle] Problem with recdef (permissive)*From*: Norbert Schirmer <schirmer at in.tum.de>*Date*: Thu, 5 Jul 2007 10:06:44 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20070627083941.GA23889@wjp-dhcp241.cs.uni-sb.de>*References*: <20070627083941.GA23889@wjp-dhcp241.cs.uni-sb.de>

Hi Mark,

and hence the error reaches the toplevel. Norbert On 27.06.2007, at 10:40, Mark A. Hillebrand wrote:

Hi all, I have a really big and quite old Isabelle heap, which I use regularly for regression testing a large collection of theories. Usingthis heap, my attempt to load a specific theory breaks at a(permissive)recdef with an exception trace and an error message [1]. If I startwitha fresh HOL heap and try to load the same theory, the permissiverecdefworks without the exception trace and just leaves the error message inthe form of the (to-be-expected) warning [2] in the log. (In thetheory,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 additionaltheories inthe big heap cause this behaviour. Also, the big heap might havedifferent global options set than the new one (like, as you see,[1] hasshow_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 (notjustthose with [simp] via `print_simpset (the_context());', but alsofor theless 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! -- Dr. Mark A. Hillebrand German Research Center for Artificial Intelligence Saarbruecken, Germany Building E1 1, Room 4.06 Phone: +49 (0)681 302 57379 Fax: +49 (0)681 302 4290 Email: mah at dfki.de -------------------------------------------------------------Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbHTrippstadterStrasse 122, D-67663 Kaiserslautern, Germany Geschaeftsfuehrung: Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender) Dr. Walter Olthoff Vorsitzender des Aufsichtsrats: Prof. Dr. h.c. Hans A. Aukes Amtsgericht Kaiserslautern, HRB 2313 -------------------------------------------------------------

- Previous by Date: [isabelle] Extended Deadline of VerAS Workshop: 14 July 2007
- Next by Date: Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution
- Previous by Thread: [isabelle] Extended Deadline of VerAS Workshop: 14 July 2007
- Next by Thread: [isabelle] Segmentation faults when running PolyML
- Cl-isabelle-users July 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list