[isabelle-dev] Issue in AFP

[Florian Haftmann]

> isabelle: 20304512a33b tip
> afp: 644957b424ee tip
> JinjaThreads FAILED
> (see also /srv/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/JinjaThreads)
> ***                            (\<forall>T.
> ***                                typeof\<^bsub>h\<^esub> v =
> ***                                \<lfloor>T\<rfloor> \<longrightarrow>
> ***                                (\<forall>C.
> ***                                    class_type_of' T =
> ***                                    \<lfloor>C\<rfloor> \<longrightarrow>
> ***                                    (\<forall>Ts Tr D.
> ***  P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow>
> ***  \<tau>external_defs D M))))
> ***                        then (\<tau>red0t (extTA2J0 P) P t h
> ***                               (Val v\<bullet>M(es), xs)
> ***                               (Val v\<bullet>M(es'), xs') \<or>
> ***                              countInitBlock (Val v\<bullet>M(es1'))
> ***                              < countInitBlock (Val v\<bullet>M(es1)) \<and>
> ***                              Val v\<bullet>M(es') =
> ***                              Val v\<bullet>M(es) \<and>
> ***                              xs' = xs) \<and>
> ***                             h' = h \<and>
> ***                             ta1 = \<lbrace>\<rbrace> \<and>
> ***                             ta = \<lbrace>\<rbrace>
> ***                        else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and>
> ***                             (if call (Val v\<bullet>M(es)) = None \<or>
> ***                                 call1 (Val v\<bullet>M(es1)) = None
> ***                              then \<exists>e'' xs''.
> ***                                      \<tau>red0r (extTA2J0 P) P t h
> *** (Val v\<bullet>M(es), xs) (e'', xs'') \<and>
> ***                                      extTA2J0
> *** P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow>
> ***                    \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and>
> ***                                      no_call P h e'' \<and>
> ***                                      \<not> \<tau>move0 P h e''
> ***                              else extTA2J0
> ***                                    P,P,t \<turnstile> \<langle>Val
> ***                           v\<bullet>M(es),
> ***                  (h, xs)\<rangle> -ta\<rightarrow>
> ***                 \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and>
> ***                                   no_call P h (Val v\<bullet>M(es)) \<and>
> ***                                   \<not> \<tau>move0 P h
> ***     (Val v\<bullet>M(es))))
> *** At command "apply" (line 911 of "/srv/data/tum/afp/master/thys/JinjaThreads/Compiler/Correctness1.thy")

Any hint what is going on?

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170618/2464cdf9/attachment.asc>