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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev