Re: [isabelle-dev] Issue in AFP

2017-06-18 Thread Tobias Nipkow 
I added two useful simp rules that broke (= mostly shortened) a number of 
proofs. I'll fix the slow sessions over the next few days - they are a bit of a 
challenge.


Tobias

On 18/06/2017 20:38, Florian Haftmann wrote:

isabelle: 20304512a33b tip
afp: 644957b424ee tip
JinjaThreads FAILED
(see also 
/srv/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/JinjaThreads)
***(\T.
***typeof\<^bsub>h\<^esub> v =
***\T\ \
***(\C.
***class_type_of' T =
***\C\ \
***(\Ts Tr D.
***  P \ C sees M: Ts\Tr = Native in D \
***  \external_defs D M
***then (\red0t (extTA2J0 P) P t h
***   (Val v\M(es), xs)
***   (Val v\M(es'), xs') \
***  countInitBlock (Val v\M(es1'))
***  < countInitBlock (Val v\M(es1)) \
***  Val v\M(es') =
***  Val v\M(es) \
***  xs' = xs) \
*** h' = h \
*** ta1 = \\ \
*** ta = \\
***else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \
*** (if call (Val v\M(es)) = None \
*** call1 (Val v\M(es1)) = None
***  then \e'' xs''.
***  \red0r (extTA2J0 P) P t h
*** (Val v\M(es), xs) (e'', xs'') \
***  extTA2J0
*** P,P,t \ \e'',(h, xs'')\ -ta\
***\Val v\M(es'),(h', xs')\ \
***  no_call P h e'' \
***  \ \move0 P h e''
***  else extTA2J0
***P,P,t \ \Val
***   v\M(es),
***  (h, xs)\ -ta\
*** \Val v\M(es'),(h', xs')\ \
***   no_call P h (Val v\M(es)) \
***   \ \move0 P h
*** (Val v\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



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Issue in AFP

2017-06-18 Thread 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)
> ***(\T.
> ***typeof\<^bsub>h\<^esub> v =
> ***\T\ \
> ***(\C.
> ***class_type_of' T =
> ***\C\ \
> ***(\Ts Tr D.
> ***  P \ C sees M: Ts\Tr = Native in D 
> \
> ***  \external_defs D M
> ***then (\red0t (extTA2J0 P) P t h
> ***   (Val v\M(es), xs)
> ***   (Val v\M(es'), xs') \
> ***  countInitBlock (Val v\M(es1'))
> ***  < countInitBlock (Val v\M(es1)) 
> \
> ***  Val v\M(es') =
> ***  Val v\M(es) \
> ***  xs' = xs) \
> *** h' = h \
> *** ta1 = \\ \
> *** ta = \\
> ***else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \
> *** (if call (Val v\M(es)) = None \
> *** call1 (Val v\M(es1)) = None
> ***  then \e'' xs''.
> ***  \red0r (extTA2J0 P) P t h
> *** (Val v\M(es), xs) (e'', xs'') \
> ***  extTA2J0
> *** P,P,t \ \e'',(h, xs'')\ -ta\
> ***\Val v\M(es'),(h', xs')\ \
> ***  no_call P h e'' \
> ***  \ \move0 P h e''
> ***  else extTA2J0
> ***P,P,t \ \Val
> ***   v\M(es),
> ***  (h, xs)\ -ta\
> *** \Val v\M(es'),(h', xs')\ \
> ***   no_call P h (Val v\M(es)) \
> ***   \ \move0 P h
> *** (Val v\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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev