On 28/01/2019 09:20, Bertram Felgenhauer wrote:
I've made sure that the machine is mostly idle; things will be much
different if several processes start competing for the ressources.
I intended to experiment with smaller numbers but have not yet done so.
On another, similar machine, --gcthreads=
Makarius wrote:
> There was indeed something odd with sharing: David Matthews has changed
> that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46).
I may give it another try later...
> > Hardware:
> > i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD
> >
> > Common build flag
On 25/01/2019 20:29, Bertram Felgenhauer wrote:
>
> - While most heap images are about 40% smaller with x86_64_32, this is
> not always the case; some heap images ended up being even larger in
> this experiment. Could there be a problem with the sharing pass on
> x86_64_32?
There was indeed
Bertram Felgenhauer wrote:
> Makarius wrote:
> > So this is the right time for further testing of applications:
> > Isabelle2018 should work as well, but I have not done any testing beyond
> > "isabelle build -g main" -- Isabelle development only moves forward in
> > one direction on a single branc
Great, thanks for looking into this!
Fabian
On 1/23/2019 4:24 PM, David Matthews wrote:
On 23/01/2019 21:08, Makarius wrote:
On 23/01/2019 12:05, David Matthews wrote:
I've had a look at this under Windows and the problem seems to be with
calls to IntInf.divMod from generated code, not from I
On 23/01/2019 23:44, Makarius wrote:
> Isabelle/20bc1d26c932 now provides an updated polyml-test-a444f281ccec
> (active by default).
>
> It performs slightly better than the previous test version -- I have
> also removed old workarounds for integer arithmetic in
> Isabelle/4591221824f6.
One more
This is really phantastic - at last I can build HOL-Analysis on my terrible new
Mac without having to put it in the freezer and it does not fall over at the
very end. It is also 20% faster.
Great work!
Tobias
On 19/01/2019 21:43, Makarius wrote:
Thanks to great work by David Matthews, there i
Isabelle/20bc1d26c932 now provides an updated polyml-test-a444f281ccec
(active by default).
It performs slightly better than the previous test version -- I have
also removed old workarounds for integer arithmetic in
Isabelle/4591221824f6.
It is important to check that obsolete entries in
$ISASEL
On 23/01/2019 21:08, Makarius wrote:
On 23/01/2019 12:05, David Matthews wrote:
I've had a look at this under Windows and the problem seems to be with
calls to IntInf.divMod from generated code, not from IntInf.pow. The
underlying RTS call used by IntInf.quotRem has changed in the 32-in-64
ver
On 23/01/2019 12:05, David Matthews wrote:
>
> I've had a look at this under Windows and the problem seems to be with
> calls to IntInf.divMod from generated code, not from IntInf.pow. The
> underlying RTS call used by IntInf.quotRem has changed in the 32-in-64
> version. It previously returned
On 23/01/2019 14:14, Bertram Felgenhauer wrote:
> Makarius wrote:
>> On 22/01/2019 12:31, Bertram Felgenhauer wrote:
>>> Makarius wrote:
So this is the right time for further testing of applications:
Isabelle2018 should work as well, but I have not done any testing beyond
"isabelle b
Makarius wrote:
> On 22/01/2019 12:31, Bertram Felgenhauer wrote:
> > Makarius wrote:
> >> So this is the right time for further testing of applications:
> >> Isabelle2018 should work as well, but I have not done any testing beyond
> >> "isabelle build -g main" -- Isabelle development only moves fo
On 22/01/2019 23:01, Makarius wrote:
On 22/01/2019 23:08, Fabian Immler wrote:
On 1/22/2019 4:00 PM, Fabian Immler wrote:
On 1/22/2019 2:28 PM, Makarius wrote:
On 22/01/2019 20:05, Fabian Immler wrote:
These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (
On 22/01/2019 23:08, Fabian Immler wrote:
> On 1/22/2019 4:00 PM, Fabian Immler wrote:
>> On 1/22/2019 2:28 PM, Makarius wrote:
>>> On 22/01/2019 20:05, Fabian Immler wrote:
These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
it se
On 1/22/2019 4:00 PM, Fabian Immler wrote:
On 1/22/2019 2:28 PM, Makarius wrote:
On 22/01/2019 20:05, Fabian Immler wrote:
These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
it seems to be the case with polyml-test-0a6ebca445fc).
The follow
On 1/22/2019 2:28 PM, Makarius wrote:
On 22/01/2019 20:05, Fabian Immler wrote:
These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
it seems to be the case with polyml-test-0a6ebca445fc).
The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead3
On 22/01/2019 20:05, Fabian Immler wrote:
> These numbers look quite extreme:
> The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
> it seems to be the case with polyml-test-0a6ebca445fc).
>
> The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:
>
> ML_PLATFORM=
These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
it seems to be the case with polyml-test-0a6ebca445fc).
The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:
ML_PLATFORM="x86-linux"
ML_OPTIONS="--minheap 2000 --maxheap 4000
On 19/01/2019 21:43, Makarius wrote:
> Thanks to great work by David Matthews, there is now an Isabelle
> component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be
> enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this:
>
> init_component "$HOME/.isabelle/contrib/p
On 22/01/2019 12:31, Bertram Felgenhauer wrote:
> Makarius wrote:
>> So this is the right time for further testing of applications:
>> Isabelle2018 should work as well, but I have not done any testing beyond
>> "isabelle build -g main" -- Isabelle development only moves forward in
>> one direction
Looks impressive. Thanks!
Larry
> On 22 Jan 2019, at 11:27, Makarius wrote:
>
> Here are some performance measurements on the best hardware that I have
> presently access to (not at TUM):
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://ma
Makarius wrote:
> So this is the right time for further testing of applications:
> Isabelle2018 should work as well, but I have not done any testing beyond
> "isabelle build -g main" -- Isabelle development only moves forward in
> one direction on a single branch.
I have tried this with Isabelle20
On 19/01/2019 21:43, Makarius wrote:
> Thanks to great work by David Matthews, there is now an Isabelle
> component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be
> enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this:
>
> init_component "$HOME/.isabelle/contrib/p
23 matches
Mail list logo