On Sa, 2015-03-21 at 18:26 +0100, Peter Lammich wrote: > It's the operation identification phase of Autoref, > quite difficult to debug ... I have not yet looked at it due to > ITP-deadline.
I found the culprit: changeset: 5269:88dc498667ff user: Rene Thiemann <rene.thiem...@uibk.ac.at> date: Fri Mar 13 15:42:00 2015 +0100 summary: adapting entries to new Deriving mechanism in LTL_to_GBA-theory, this removes a linorder-constraint on create_name_igba, which causes the breakdown, because later, autoref is only given rules to refine create_name_igba for 'a::linorder, but the respective lemmas do not repeat the linorder-constraint. I fixed it by adding the linorder-constraint to the refinement, leaving the abstract version general. - definition create_name_igba :: "'a::linorder ltln \<Rightarrow> _" + definition create_name_igba :: "'a ltln \<Rightarrow> _" where See now: changeset 56d43ce6541f http://sourceforge.net/p/afp/code/ci/56d43ce6541f4602d390d1940ce69d211bd8724c/ -- Peter > > I will have look at it next week on Monday or Tuesday. Does anyone know > the changeset that introduced the failure, or is there an easy way to > find out? > > -- > Peter > > > On Sa, 2015-03-21 at 18:08 +0100, Florian Haftmann wrote: > > > isabelle: e6f0c361ac73 tip > > > afp: 2a0dc69c001b tip > > > > > Building LTL_to_GBA ... > > > > > > LTL_to_GBA FAILED > > > (see also > > > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/LTL_to_GBA) > > > > > > => ('a, 'c) node_scheme set => ('a, 'c) node_scheme set" > > > Phase "id_op" > > > Failed to identify: create_name_gba > > > Failed to identify: ti_Lcnv > > > 0.048s elapsed time, 0.288s cpu time, 0.000s GC time > > > ### theory "LTL_to_GBA_impl" > > > ### 61.088s elapsed time, 341.092s cpu time, 22.988s GC time > > > *** Failed to apply proof method (line 1156 of > > > "/mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy"): > > > *** goal (1 subgoal): > > > *** 1. (?c, > > > *** %\<phi>. > > > *** create_name_gba \<phi> >>= > > > *** (%A. gba_to_idx A >>= > > > *** (%A'. stat_set_data_nres (card (frg_V A)) (card (frg_V0 > > > A')) > > > *** (igbg_num_acc A') >>= > > > *** (%_. RETURN A')))) > > > *** : \<langle>Id\<rangle>ltln_rel \<rightarrow> > > > *** \<langle>igbav_impl_rel_ext unit_rel nat_rel > > > *** (\<langle>Id\<rangle>fun_set_rel)\<rangle>nres_rel > > > *** At command "apply" (line 1156 of > > > "/mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy") > > > CAVA_buildchain1 CANCELLED > > > CAVA_buildchain3 CANCELLED > > > CAVA_LTL_Modelchecker CANCELLED > > > Unfinished session(s): CAVA_LTL_Modelchecker, CAVA_buildchain1, > > > CAVA_buildchain3, LTL_to_GBA > > > 0:20:58 elapsed time, 0:59:35 cpu time, factor 2.84 > > > > _______________________________________________ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev