[isabelle-dev] AFP failures near 7f7ca3a43026

[Gerwin Klein]

In the first instance, it is the authors/maintainers of the entry that we will ask for help. In this case, Peter has promised to look at this set of new entries (CAVA etc), but it will take him some time.

We usually have this state of affairs close to new Isabelle releases when too many incompatibilities have accumulated. I don’t have a good solution either, but I’m open to ideas.

Cheers,
Gerwin

On 12.06.2014, at 7:56 am, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

> Unfinished session(s): CAVA_Automata, CAVA_Base, CAVA_LTL_Modelchecker,
> CAVA_buildchain1, CAVA_buildchain3, Gabow_SCC, LTL_to_GBA,
> MonoBoolTranAlgebra, Promela
>
> I have a suspicion that the dropout in MonoBoolTranAlgebra is due to
> http://isabelle.in.tum.de/repos/isabelle/rev/4cf607675df8
>
> Concerning the others – in recent times there has been a tendency for
> new AFP entries to lay around with no observable activity even a few
> days later.  From a maintaince point of view this is quite
> unsatisfactory, although I have no convincing proposal at hand what the
> way of doing should be in that case.  Surely this cannot be duty of the
> AFP publishers themselves, but the current approach seems to me like
> muchroom engineering: cut off the first head sprouting off the ground…
> any ideas?
>
>       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


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.