Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML
On Thu, 9 Jun 2011, Lawrence Paulson wrote: I see you are alert, as always! Just the normal process of consuming incoming mails and changesets ... :-) But here there were two reasons for extra attention: (1) suspicious keywords in the log entry (like fixed or bug) and (2) a realistic chance that I broke this myself in recent reworking of blast (a relatively simple case of the still ongoing localisation effort). In this particular case, it's pretty clear that the exception was raised here, in conv.ML: fun gconv_rule cv i th = (case try (Thm.cprem_of th) i of SOME ct = let val eq = cv ct in if Thm.is_reflexive eq then th else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th end | NONE = raise THM (gconv_rule, i, [th])); And this was in conformance with a common use of exception THM, namely to indicate that the designated subgoal did not exist. So a tactic calling this code should indeed catch the exception and indicate failure by returning the empty sequence. Yes, formally timing_depth_tac was always wrong in that sense as a tactic. I have learned the requirements for proper tactics from you many years ago (they are now documented in the implementation manual). Normally the CONVERSION tactical would convert the failure of the conversion (e.g. via exception THM) into proper Seq.empty for the tactic, but it was not used here for other reasons. Just some weeks ago I inspected the code again, and convinced myself that the DEEPEN around timing_depth_tac repairs this feature. Unfortunately I've overlooked the special side-entry Blast.depth_tac, which bypasses DEEPEN. So historically the problem was actually introduced in 1997 here http://isabelle.in.tum.de/repos/isabelle/rev/cc3e8453d7f0 when the public Blast.depth_tac was added as new feature. Did anybody actually understand the source of the problem? In summary the situation is like that: blast with explicit depth limit did not check subgoal bounds properly. The problem can be reproduced like that (e.g. in Isabelle2011): lemma True apply rule apply (blast 5) *** exception THM 1 raised (line 212 of conv.ML): gconv_rule *** At command apply (line 7 of /home/makarius/Scratch.thy) Without that extra argument it is deepened from 1 .. 20. Since Andreas had explicit 25 to get beyond that, he might consider using [[blast_depth_limit = 30]] or similar to get the incremental effect to higher limits, although there could be a general slowdown up there. See also http://isabelle.in.tum.de/repos/isabelle/rev/01f051619eee for some further cleanup of blast. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML
This fix solves the problem with the exception. I tried it with 574613b47583. Can you add it to the repository as I do not have wirte access to that. Thanks, Andreas Lawrence Paulson schrieb: Thank you for looking there! This is the most plausible culprit. But it is strange that this problem has arisen before. A possible fix is to replace the last line of the function timing_depth_tac in that file as follows: handle PROVE = Seq.empty | THM _ = Seq.empty; Andreas, do you want to try this and see if it helps? Larry On 27 May 2011, at 15:27, Stefan Berghofer wrote: Hi Larry and Andreas, there is another occurrence of gconv_rule in Provers/blast.ML (in function timing_depth_tac). Since the exception is thrown when invoking blast, this occurrence of gconv_rule may be the culprit. -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-48352 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu http://pp.info.uni-karlsruhe.de KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Fwd: [isabelle] Exception in conv.ML
It looks like this exception is raised when gconv_rule cv i th is called and the specified subgoal does not exist. The function gconv_rule is called in only four places in Pure: ./Isar/element.ML: (Conv.gconv_rule Drule.beta_eta_conversion 1 r) ./raw_simplifier.ML: then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm ./raw_simplifier.ML:Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm) ./tactical.ML:fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) Without a full trace, it is impossible to be certain which one. I looked in raw_simplifier.ML, and the two calls did the necessary check to prevent this exception from being raised. The function CONVERSION in tactical.ML does no check, but catches exception THM. This leaves the function compose_witness in Isar/element.ML, where I see neither a check that the subgoal exists nor an exception handler. But I could be wrong, as such checks may be done elsewhere. Does anybody else have a suggestion? Larry Begin forwarded message: From: Andreas Lochbihler andreas.lochbih...@kit.edu Date: 27 May 2011 14:51:27 GMT+01:00 To: isabelle-users isabelle-us...@cl.cam.ac.uk Subject: [isabelle] Exception in conv.ML Hi all, have the following weird behaviour. After having applied auto on my goal, I am left with 24 subgoals. Applying 24 copies of the following invokation of the blast method solves all 24 subgoals. However, if I try to collaspe all of them into a single invokation apply(blast 25 ...)+, I get the exception below. What is going wrong here? And how can I fix it? If need be, I can make my theories available, but I doubt that I can produce a minimal core example. apply(blast 25 intro: rtranclp_trans rtranclp_tranclp_tranclp treds1r_cons_treds1r List1Red2 treds1t_cons_treds1t dest: t) *** exception THM 1 raised (line 212 of conv.ML): *** gconv_rule *** EX es'' xs''. ***P,e # es,n,h' |- (es'', xs'') [--] (stk', loc', pc', xcp') ***(if tmoves2 (compP2 P) h stk (e # es) pc xcp *** then h' = h *** (if xcp' = Any -- pc pc' then treds1r else treds1t) P t h *** (e' # es, xs) (es'', xs'') *** else EX ta' es' xs'. *** treds1r P t h (e' # es, xs) (es', xs') *** P,t |- es',(h, xs') [-ta'-] es'',(h', xs'') *** ta_bisim wbisim1 (extTA2J1 P ta') ta *** ¬ tmoves1 P h es' *** (calls1 (e' # es) = None *** no_calls2 (e # es) pc es' = e' # es xs' = xs)) *** At command apply Best regards, Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-48352 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu http://pp.info.uni-karlsruhe.de KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML
I'll be happy to provide a trace if you tell me how to obtain one. If I turn on Debugging in the settings menu, I only get an empty exception trace in the isabelle buffer: Exception trace for exception - THM raised in conv.ML line 212 End of trace Andreas Lawrence Paulson schrieb: It looks like this exception is raised when gconv_rule cv i th is called and the specified subgoal does not exist. The function gconv_rule is called in only four places in Pure: ./Isar/element.ML: (Conv.gconv_rule Drule.beta_eta_conversion 1 r) ./raw_simplifier.ML: then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm ./raw_simplifier.ML:Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm) ./tactical.ML:fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) Without a full trace, it is impossible to be certain which one. I looked in raw_simplifier.ML, and the two calls did the necessary check to prevent this exception from being raised. The function CONVERSION in tactical.ML does no check, but catches exception THM. This leaves the function compose_witness in Isar/element.ML, where I see neither a check that the subgoal exists nor an exception handler. But I could be wrong, as such checks may be done elsewhere. Does anybody else have a suggestion? Larry Begin forwarded message: From: Andreas Lochbihler andreas.lochbih...@kit.edu Date: 27 May 2011 14:51:27 GMT+01:00 To: isabelle-users isabelle-us...@cl.cam.ac.uk Subject: [isabelle] Exception in conv.ML Hi all, have the following weird behaviour. After having applied auto on my goal, I am left with 24 subgoals. Applying 24 copies of the following invokation of the blast method solves all 24 subgoals. However, if I try to collaspe all of them into a single invokation apply(blast 25 ...)+, I get the exception below. What is going wrong here? And how can I fix it? If need be, I can make my theories available, but I doubt that I can produce a minimal core example. apply(blast 25 intro: rtranclp_trans rtranclp_tranclp_tranclp treds1r_cons_treds1r List1Red2 treds1t_cons_treds1t dest: t) *** exception THM 1 raised (line 212 of conv.ML): *** gconv_rule *** EX es'' xs''. ***P,e # es,n,h' |- (es'', xs'') [--] (stk', loc', pc', xcp') ***(if tmoves2 (compP2 P) h stk (e # es) pc xcp *** then h' = h *** (if xcp' = Any -- pc pc' then treds1r else treds1t) P t h *** (e' # es, xs) (es'', xs'') *** else EX ta' es' xs'. *** treds1r P t h (e' # es, xs) (es', xs') *** P,t |- es',(h, xs') [-ta'-] es'',(h', xs'') *** ta_bisim wbisim1 (extTA2J1 P ta') ta *** ¬ tmoves1 P h es' *** (calls1 (e' # es) = None *** no_calls2 (e # es) pc es' = e' # es xs' = xs)) *** At command apply Best regards, Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-48352 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu http://pp.info.uni-karlsruhe.de KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-48352 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu http://pp.info.uni-karlsruhe.de KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML
Quoting Lawrence Paulson l...@cam.ac.uk: But I could be wrong, as such checks may be done elsewhere. Does anybody else have a suggestion? Hi Larry and Andreas, there is another occurrence of gconv_rule in Provers/blast.ML (in function timing_depth_tac). Since the exception is thrown when invoking blast, this occurrence of gconv_rule may be the culprit. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML
Thank you for looking there! This is the most plausible culprit. But it is strange that this problem has arisen before. A possible fix is to replace the last line of the function timing_depth_tac in that file as follows: handle PROVE = Seq.empty | THM _ = Seq.empty; Andreas, do you want to try this and see if it helps? Larry On 27 May 2011, at 15:27, Stefan Berghofer wrote: Hi Larry and Andreas, there is another occurrence of gconv_rule in Provers/blast.ML (in function timing_depth_tac). Since the exception is thrown when invoking blast, this occurrence of gconv_rule may be the culprit. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
