[isabelle-dev] JinjaThreads

[Gerwin Klein]

On 19/12/2010, at 8:16 AM, Alexander Krauss wrote:

> Clemens Ballarin wrote:
>> JinjaThreads doesn't seem to run out of the box (on macbroy2, with Poly/ML 5.3.0).  It seems to run out of memory.
>> I use ML_OPTIONS="-H 500", but I would assume the AFP sets this appropriately.
>> Probably this is a known issue, but I don't know where to check for the automatic AFP logs.
> 
> The logs are in ~isatest/afp-log. I would assume that you do not need special settings on macbroy2. On smaller machines one must turn off parallelism, I was told.

Specifically for JinjaThreads, the IsaMakefile allows you to set an environment variable JINJATHREADS_OPTIONS (to for instance "-M 1"). 


> I am not sure where the settings for the AFP tests come from, though...

In general, there are no special settings. If you run testall it will use whatever your environment is.

The nightly regression tests uses whatever is set as $SHORT (short name for settings) in admin/regression. Currently this is mac-poly64-M4, which in turn you can look up in isabelle/Admin/isatest/settings (-M 4, mac platform, 64 bit, poly 5.3).

Cheers,
Gerwin