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,
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
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
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
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
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
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
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
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
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
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
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
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
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:
>
>
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
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
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
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
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
23 matches
Mail list logo
