It's the operation identification phase of Autoref,
quite difficult to debug ... I have not yet looked at it due to
ITP-deadline.
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
