[isabelle-dev] AFP: Session AVL-Trees broken

Tobias Nipkow nipkow at in.tum.de
Thu Nov 8 11:59:04 CET 2012

This is exactly why I am against SMT certificates in AFP entries. Ondrej, can
you possibly remove them?


Am 08/11/2012 11:55, schrieb Jasmin Christian Blanchette:
> Hi Gerwin,
> Am 07.11.2012 um 22:41 schrieb Gerwin Klein:
>> *** Bad certificate cache: missing certificate
>> *** At command "by" (line 169 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/AVL-Trees/AVL.thy")
>> (real error)
> OK, this is related to my Isabelle change 34b0464d7eef, which slightly affects the SMT problems generated (more specifically, it affects a comment in the SMT problems). This is enough to change the hasked key that's used to look up certificates. I hadn't realized that the "AVL-Trees" example also uses certificates. I'll regenerate them.
> Sorry for the trouble.
> Jasmin
> _______________________________________________
> 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