[isabelle-dev] Build Problem in JinjaThreads

[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 \<and>
>> ***       (case lnth stls n of
>> ***        (s, tl, s') \<Rightarrow> \<not> \<tau>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 \<Rightarrow> 'tl llist
>> *** Operand:
>> ***   {n. enat n < llength stls \<and>
>> ***       (case lnth stls n of
>> ***        (s, tl, s') \<Rightarrow> \<not> \<tau>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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170601/bca4e722/attachment-0002.html>