[isabelle-dev] Testing AFP at TUM

Makarius makarius at sketis.net
Mon Oct 22 20:03:28 CEST 2012

On Mon, 22 Oct 2012, Makarius wrote:

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

In Isabelle/8b50286c36d3 it is section 3.3 of the "system" manual, 
subsection "Examples".  These command lines are taken from real-life.

What I normally do for testing is this:

   isabelle build -a             # build all
   isabelle build -a -d '$AFP'   # build all with AFP

Add -j2 or -j4 or -j8 according to your hardware.

Pretty obvious?

I've developed the habit to test things both after pull and before push, 
since it saves more time than it costs.  I usually run the full AFP test 
over lunch to see about its health.

Recently AFP has become a testbed for heavy-duty interaction tests of 


More information about the isabelle-dev mailing list