[isabelle-dev] Jenkins maintenance

Makarius makarius at sketis.net
Thu Oct 6 16:04:23 CEST 2016


On 06/10/16 15:22, Lawrence Paulson wrote:
> I have a Mac Pro, and I just use “isabelle build -a”.  Maybe I could use multithreading more (the machine supports 12 cores).

There is a certain art to combine build options -j N and -o threads=M,
depending on the hardware (based on manual experiments).

On my own 2 * 6 core machine, I usually use this:

  isabelle build -j4 -a -o threads=6

and settings as follows:

  ML_OPTIONS="-H 1500 --gcthreads 6"


> If I know that my changes affect specific AFP entries, I run
> them manually.

I've also found myself doing the prediction in my head. Some tool
support for that would be nice, but I have no concrete ideas right now.


> A full test takes a couple of hours, and it is a pain.

What I often do is

  isabelle build -j4 -a -d '$AFP' -X slow

It takes approx. 1h, but is changing quickly recently, due to massive
inflow of new AFP entries (which is a very good thing).


	Makarius




More information about the isabelle-dev mailing list