[isabelle-dev] Isabelle repository broken

[Johannes Hölzl]

Sorry this was my fault.

"isabelle build -a" does not guarantee that the current changes are
actually committed...

BTW, can the predicate_compiler setup s.t. typedefs are ignored
automatically?

 - Johannes


Am Montag, den 13.04.2015, 11:28 +0200 schrieb Makarius:
> In current 7ff7fdfbb9a0 there is this breakdown:
> 
> HOL-Quickcheck_Examples FAILED
> *** No specification for Abs_filter
> *** At command "quickcheck" (line 150 of "~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy")
> *** No specification for Abs_filter
> *** At command "quickcheck" (line 145 of "~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy")
> 
> 
> Since there is no way around a full "isabelle build -a" before pushing 
> anything, such incidents can't happen, at least in theory.
> 
> 
>  	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev