[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

Lawrence Paulson lp15 at cam.ac.uk
Thu Nov 19 12:52:23 CET 2015

I am partly to blame. The changes involving the “real” function caused a lot of disruption. I needed a week to get all of Isabelle/HOL working again, and thought it a more practical option to tackle the AFP failures after they occurred. Most of them were only out of action for a day.


> On 19 Nov 2015, at 09:16, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> Thanks to all who have invested time and energy to work on those issues.
> Nevertheless I have the impression that in the last time there have have
> been lots of movements in the distribution being speculative in the
> sense that no systematic testing including the AFP had taken place.
> What is the reason for this?  No access to suitable computing machines?
> Cheers,
> 	Florian
> -- 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list