[isabelle-dev] Testing AFP at TUM

Makarius makarius at sketis.net
Mon Oct 22 15:14:31 CEST 2012

On Mon, 22 Oct 2012, Tjark Weber wrote:

> On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote:
>> Btw. whenever I'm testing the AFP these days without relying on the
>> testboard I use the following [...]
> In the last few months I've seen several emails with testing advice on
> this list (occasionally motivated by commits that apparently hadn't
> been tested very thoroughly). Perhaps it would be useful to distill
> these into a concise description of current best practice; either as
> part of README_REPOSITORY or in the Isabelle Wiki?

This raises again a whole bunch of unsettled questions, like "What is the 
Isabelle community wiki anyway?"  So far there have been mainly 
semi-official explanations on administrative processes, nothing relevant 
to a genuine Isabelle community.  Professional use of professional systems 
means you use a stable release, not arbitrary snapshots.

Apart from that we have a split into old-school manual testing (what used 
to be "makeall all" and is now "build -a" as shown in the System manual, 
vs. newer mira/testboard.  Old isatest also has some purpose left -- I 
have recently started some tiny renovations here and there.

So just the usual administrative chaos of the past few years ...


More information about the isabelle-dev mailing list