[isabelle-dev] Testing AFP at TUM

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Tue Oct 23 20:24:55 CEST 2012


Hi all,

> 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?

IMHO the situation is changing too quickly to have something persistent.

> 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.

The issue is that in the long run the testboard should be available
without administrative access to TUM, e.g. via github.  Still a long way
to go.  Nevertheless it is useful to keep alive collective knowledge how
to test without further infrastructure.

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

Alas.  The mira impetus from two years ago is currently fading away…  It
will require concerted effort to set it on track again.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121023/8137f508/attachment.sig>


More information about the isabelle-dev mailing list