[isabelle-dev] isatest silence

Gerwin Klein Gerwin.Klein at nicta.com.au
Fri Dec 14 22:47:07 CET 2012

On 15/12/2012, at 12:54 AM, Makarius <makarius at sketis.net> wrote:

> The unusual isatest silence from today means that all tests finished successfully!

No news are good news :-)

> http://isabelle.in.tum.de/devel/ shows some development snapshot Isabelle_14-Dec-2012.tar.gz together with the vital statistics.
> Since "the" development snapshot has lost its purpose with the introduction of the online component management for repository clones, I shall dismantle that part of isatest eventually.  Instead there should be unconditional statistics on the web page even in the case of some failures.

Unconditional statistics are a good idea.

The development snapshot is only a byproduct and can be left out. The main reason for generating a .tar.gz was to test if the release building machinery works and to test something that is as close as possible to a release that users work with, not the repository that we all work with every day anyway. At least back in the day there were often plenty of surprises after building the release (as compared to the repo structure). This may have changed a little with the cleanup after the move to hg, but it's still work thinking about at least.



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.

More information about the isabelle-dev mailing list