Re: [isabelle-dev] Build Problem in JinjaThreads

2017-06-01 Thread Manuel Eberl 
That was due to my reforms of the sublist/subseq stuff and should be 
repaired by this afternoon. Tomorrow's slow tests should run through 
fine again. Unfortunately, these slow sessions don't have the same rapid 
testing cycle as the normal sessions.


Manuel


On 2017-06-01 16:19, Florian Haftmann wrote:

isabelle: 3bec939bd808 tip
afp: 09eedef13195 tip


***   {n. enat n < llength stls \
***   (case lnth stls n of
***(s, tl, s') \ \ \move s tl s')} ::
***   nat set
***
*** Coercion Inference:
***
*** Local coercion insertion on the operand failed:
*** Cannot generate coercion from "??'a26 set" to "'a"
***
*** Now trying to infer coercions globally.
***
*** Coercion inference failed:
*** weak unification of subtype constraints fails
***
***
*** At command "hence" (line 512 of 
"/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")
*** Type unification failed
***
*** Type error in application: incompatible operand type
***
*** Operator:  lsublist tls :: 'a \ 'tl llist
*** Operand:
***   {n. enat n < llength stls \
***   (case lnth stls n of
***(s, tl, s') \ \ \move s tl s')} ::
***   nat set
***
*** Coercion Inference:
***
*** Local coercion insertion on the operand failed:
*** Cannot generate coercion from "??'a26 set" to "'a"
***
*** Now trying to infer coercions globally.
***
*** Coercion inference failed:
*** weak unification of subtype constraints fails
***
***
*** At command "hence" (line 512 of 
"/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")

Any suggestion what is going on here?

Cheers,
Florian



___
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

[isabelle-dev] Build Problem in JinjaThreads

2017-06-01 Thread Florian Haftmann 
isabelle: 3bec939bd808 tip
afp: 09eedef13195 tip

> ***   {n. enat n < llength stls \
> ***   (case lnth stls n of
> ***(s, tl, s') \ \ \move s tl s')} ::
> ***   nat set
> *** 
> *** Coercion Inference:
> *** 
> *** Local coercion insertion on the operand failed:
> *** Cannot generate coercion from "??'a26 set" to "'a"
> *** 
> *** Now trying to infer coercions globally.
> *** 
> *** Coercion inference failed:
> *** weak unification of subtype constraints fails
> *** 
> *** 
> *** At command "hence" (line 512 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")
> *** Type unification failed
> *** 
> *** Type error in application: incompatible operand type
> *** 
> *** Operator:  lsublist tls :: 'a \ 'tl llist
> *** Operand:
> ***   {n. enat n < llength stls \
> ***   (case lnth stls n of
> ***(s, tl, s') \ \ \move s tl s')} ::
> ***   nat set
> *** 
> *** Coercion Inference:
> *** 
> *** Local coercion insertion on the operand failed:
> *** Cannot generate coercion from "??'a26 set" to "'a"
> *** 
> *** Now trying to infer coercions globally.
> *** 
> *** Coercion inference failed:
> *** weak unification of subtype constraints fails
> *** 
> *** 
> *** At command "hence" (line 512 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")

Any suggestion what is going on here?

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