[isabelle-dev] Testing AFP at TUM
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.
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