[isabelle-dev] JinjaThreads FAILED

[Johannes Hölzl]

Sorry was my mistake, should be fixed with d5a3dbc9da17 now.

 - Johannes

Am Sonntag, den 16.11.2014, 19:48 +0100 schrieb Florian Haftmann:
> > isabelle: 059ba950a657 tip
> > afp: 0fdf8f639bb4 tip
> > Running JinjaThreads ...
> > 
> > 
> > JinjaThreads FAILED
> > (see also /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/JinjaThreads)
> > 
> > *** At command "inductive" (line 413 of "/mnt/home/haftmann/data/afp/master/thys/JinjaThreads/Framework/FWLTS.thy")
> > *** Type unification failed: No type arity prod :: floor_ceiling
> > *** 
> > *** Type error in application: incompatible operand type
> > *** 
> > *** Operator:  floor :: ??'a => int
> > *** Operand:   (x, ln) :: ??'b * (real => real)
> > *** 
> > *** Coercion Inference:
> > *** 
> > *** Local coercion insertion on the operand failed:
> > *** No type arity prod :: floor_ceiling
> > *** 
> > *** Now trying to infer coercions globally.
> > *** 
> > *** Coercion inference failed:
> > *** weak unification of subtype constraints fails
> > *** Clash of types "_ option" and "int"
> > *** 
> > *** At command "inductive" (line 413 of "/mnt/home/haftmann/data/afp/master/thys/JinjaThreads/Framework/FWLTS.thy")
> > Unfinished session(s): JinjaThreads
> > 0:13:06 elapsed time, 1:00:51 cpu time, factor 4.64
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev