[isabelle-dev] Problem in the AFP

[Peter Lammich]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev