[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
