[isabelle-dev] AFP

[Tobias Nipkow]

Very good question. This is and has been the situation for a week or so:

[Tycon] is still on FAIL.
[Nominal2] is still on FAIL.
[Incompleteness] is still on FAIL.
[HyperCTL] is still on FAIL.
[Launchbury] is still on FAIL.

Could the parties concerned let us know what is going on?

Thanks
Tobias

On 15/05/2014 18:53, Florian Haftmann wrote:
> I am under the impression that the AFP is currently lagging behind, e.g.
> 
> isabelle: 5bee93b2020d tip afp: c677a10107a6 tip
> 
> Any changesets awaiting a push somewhere?
> 
> Florian
> 
>> Tycon FAILED (see also
>> /mnt/home/haftmann/data/isabelle/devel/heaps/polyml-5.5.2_x86-linux/log/Tycon)
>>
>>
>> 
*** Failed to load theory "Binary_Tree_Monad" (unresolved "Monad")
>> *** Failed to load theory "Lift_Monad" (unresolved "Monad") *** Failed to
>> load theory "Monad_Plus" (unresolved "Monad") *** Failed to load theory
>> "Monad_Zero" (unresolved "Monad") *** Failed to load theory
>> "Writer_Monad" (unresolved "Monad") *** Failed to load theory
>> "Error_Monad" (unresolved "Monad_Plus") *** Failed to load theory
>> "Monad_Zero_Plus" (unresolved "Monad_Plus", "Monad_Zero") *** Failed to
>> load theory "Lazy_List_Monad" (unresolved "Monad_Zero_Plus") *** Failed
>> to load theory "Maybe_Monad" (unresolved "Monad_Zero_Plus") *** Failed to
>> load theory "State_Transformer" (unresolved "Monad_Zero_Plus") *** Failed
>> to load theory "Error_Transformer" (unresolved "Error_Monad") *** Failed
>> to load theory "Writer_Transformer" (unresolved "Writer_Monad") ***
>> Failed to load theory "Resumption_Transformer" (unresolved "Monad_Plus") 
>> *** Missing outer syntax command(s) "tycondef" *** ML error (line 397 of
>> "/mnt/home/haftmann/data/afp/devel/thys/Tycon/tycondef.ML"): *** Value or
>> constructor (axiomatize_arity) has not been declared in structure
>> Axclass *** ML error (line 803 of
>> "/mnt/home/haftmann/data/afp/devel/thys/Tycon/tycondef.ML"): *** Value or
>> constructor (axiomatize_arity) has not been declared in structure
>> Axclass *** *** At command "ML_file" (line 223 of
>> "/mnt/home/haftmann/data/afp/devel/thys/Tycon/Functor.thy")
> 
> 
> 
> 
> _______________________________________________ isabelle-dev mailing list 
> isabelle-dev at in.tum.de 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>