[isabelle-dev] Problem in the AFP

[Peter Lammich]

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