[isabelle-dev] Global build failures of the AFP in the testboard

[Lars Noschinski]

On 15.05.2013 15:55, Makarius wrote:
> On Thu, 25 Apr 2013, Dmitriy Traytel wrote:
>
>> http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694
>
> Side-remark about mira configuration: the log says
>
> ML_HOME="/home/polyml/polyml-svn/x86-linux"
>
> but that SVN version is often fluctuating, depending on current
> experiments with the SVN, and usually lagging behind.
>
> The latest official release version is here: /home/polyml/polyml-5.5.0
> or even just what Admin/components/main specifies.

> For best performance on hardware with many cores, ML options like this
> usually help:
>
> ML_OPTIONS="-H 1000 --gcthreads 4"
>
> or
>
> ML_OPTIONS="-H 1000 --gcthreads 8"
>
>
> Where are these mira/testboard options anyway? Normally the entry points
> for anything like that is Admin/ within the Isabelle repository, such as
> Admin/isatest/.

The basic configuration of the Mira system is at

  ~isatest/testbench/mira/settings/settings.py (for testboard), resp.
  ~isatest/testbench-main/mira/settings/settings.py (for reports)

and includes the configurations from the repositories (e.g. 
Isabelle:Admin/mira.py or AFP:admin/mira.py). The latter overrides the 
ML settings.

@Alex, Gerwin: Is there any reason remaining why the AFP should not use 
the default PolyML version?  I remember Alex and I dropped a similar 
override from the Isabelle tests.

Caveat: The settings (both global and repository-specific) are only 
loaded once when the mira daemon is started. If they change it is 
necessary to restart the daemon.

   -- Lars