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