On 17.05.2013 17:24, Makarius wrote:
On Thu, 16 May 2013, Lars Noschinski wrote:
-
ML_PLATFORM=x86-linux
ML_HOME="/home/polyml/polyml-svn/x86-linux"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="-H 1000"
ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"
--
On Thu, 16 May 2013, Lars Noschinski wrote:
-
ML_PLATFORM=x86-linux
ML_HOME="/home/polyml/polyml-svn/x86-linux"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="-H 1000"
ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"
-
and I would simplify this
On 16.05.2013 00:43, Gerwin Klein wrote:
On 16.05.2013, at 1:25 AM, Lars Noschinski wrote:
@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.
Not that I am aware of.
On Wed, 15 May 2013, Gerwin Klein wrote:
On 16.05.2013, at 1:25 AM, Lars Noschinski wrote:
@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.
Not that I am aware of
On 16.05.2013, at 1:25 AM, Lars Noschinski wrote:
> @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.
Not that I am aware of. The main reason there was an explicit
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
On 15.05.2013 16:34, Makarius wrote:
I am using the mira results on http://isabelle.in.tum.de/reports/Isabelle
myself a lot to navigate quickly to points where Isabelle and AFP diverge.
Is that already testboard? I thought that would be a slightly different
mode of operation to check quasi-inter
Am 15.05.2013 16:34, schrieb Makarius:
On Wed, 15 May 2013, Dmitriy Traytel wrote:
Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how
it actually used in practice. I just do "isabelle build -j4 -a -d
'$AFP'" to see immediately how everyt
On Wed, 15 May 2013, Dmitriy Traytel wrote:
Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how it
actually used in practice. I just do "isabelle build -j4 -a -d '$AFP'" to
see immediately how everything works out. It is also possible to
Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how it
actually used in practice. I just do "isabelle build -j4 -a -d
'$AFP'" to see immediately how everything works out. It is also
possible to make a quick integrity check via "isabelle b
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
e
On Thu, 25 Apr 2013, Dmitriy Traytel wrote:
Hi all,
since "Containers" are in the AFP mira results in global crashes of the build
tool
(http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694).
By global I mean that no session is built at all due to an outdated (
Hi all,
since "Containers" are in the AFP mira results in global crashes of the
build tool
(http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694).
By global I mean that no session is built at all due to an outdated (wrt
Isabelle repository, e.g. 916271d52466) i
13 matches
Mail list logo
