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
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/polyml-test-0a6ebca445fc"
It requires the usual
On 15/05/17 14:33, Makarius wrote:
> On 15/05/17 12:14, Makarius wrote:
>> Some results can be seen here:
>>
>> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
>> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html
>>
>> The test hardware is
On 15/05/17 14:24, Makarius wrote:
> On 15/05/17 12:29, Lawrence Paulson wrote:
>> Version 5.7 doesn’t even build on my main workstation, though it works
>> on my MacBook Pro running broadly similar software. No idea what is
>> going on here, but I’m not happy about it.
>
> There are already some
On 15/05/17 12:14, Makarius wrote:
> Some results can be seen here:
>
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html
>
> The test hardware is similar or actually the same as "Linux A
On 15/05/17 12:29, Lawrence Paulson wrote:
> Version 5.7 doesn’t even build on my main workstation, though it works
> on my MacBook Pro running broadly similar software. No idea what is
> going on here, but I’m not happy about it.
There are already some mail threads on the Poly/ML list, where vari
Version 5.7 doesn’t even build on my main workstation, though it works on my
MacBook Pro running broadly similar software. No idea what is going on here,
but I’m not happy about it.
Larry
> On 15 May 2017, at 11:14, Makarius wrote:
>
> David Matthews has made the Poly/ML 5.7 release snapshot s
David Matthews has made the Poly/ML 5.7 release snapshot some weeks ago
(see https://github.com/polyml/polyml/releases/tag/v5.7), but announced
it only last week.
I have wrapped that up as a component in Isabelle/d3c5898f1a5e, but that
is only for testing, not for production use. Some results can
There is now a Poly/ML repository test version, as regular Isabelle
component (unused by default).
See also
https://bitbucket.org/isabelle_project/isabelle-release/commits/b3ccfd59097d
-- that changeset also documents automated administrative testing in the
usual manner.
Anybody who wants to try
Poly/ML 5.5.2 was released a few days ago, see also
http://lists.inf.ed.ac.uk/pipermail/polyml/2014-May/001417.html
In Isabelle/e7bf30290627 the Isabelle component is updated accordingly.
In the coming months before the release it is important to watch out for
potential problems, and to report
Hi Sascha,
Thanks for the clarification. Since Z3 needs to be knowingly
activated, I agree this should be sufficient. I did not imply
distributing Z3 with Isabelle was not legal, merely some users may
want to know that they will be downloading software for non-commercial
use only ahead
Hi Clemens,
Please note that Z3's license explicitly allows distribution for
non-commercial purposes such as teaching, academic research or public
demonstrations. Although Isabelle's BSD-style license would allow
Isabelle to be applied to commercial applications, too, it still is a
research produ
Thank you, Jasmin and Makarius. I managed to replace my Poly/ML
installation by the one included in Isabelle2011.app. It took 15
minutes to download this, though.
I noted that the bundle contains software that is free for
non-commercial use only (z3). This might be problematic for some u
On Tue, 21 Jun 2011, Clemens Ballarin wrote:
The Isabelle download page is surprisingly silent about Poly/ML
nowadays.
The deeper reason for that is the tendency towards "no servicable parts
inside", i.e. the default bundle contains already (almost) everything one
needs, included all the add
On Tue, 21 Jun 2011, Jasmin Blanchette wrote:
Am 21.06.2011 um 23:11 schrieb Clemens Ballarin:
After updating my Isabelle repository (which I haven't done for quite a
while) Poly/ML stopped to start up. I have 5.2 and according to the
release notes this is no longer supported. Do I need to
Am 21.06.2011 um 23:11 schrieb Clemens Ballarin:
After updating my Isabelle repository (which I haven't done for
quite a while) Poly/ML stopped to start up. I have 5.2 and
according to the release notes this is no longer supported. Do I
need to build 5.4 for myself or do we provide a pre-
After updating my Isabelle repository (which I haven't done for quite
a while) Poly/ML stopped to start up. I have 5.2 and according to the
release notes this is no longer supported. Do I need to build 5.4 for
myself or do we provide a pre-built version for MacOS 10.5 somewhere?
The Isab
Am 26.05.2010 um 18:54 schrieb Makarius:
> * Some tuning of the Poly/ML runtime to shorted the (busy) wait interval
>for external processes from 100ms to 10ms. This improves reactivity
>of the ML bash/bash_output functions, at the cost of burning a few
>extra cycles.
That is excelle
For the upcoming Isabelle release there will be a repackaged version of
Poly/ML 5.3.0, see the current setup in
http://www4.in.tum.de/~wenzelm/test/polyml-5.3.0.tar.gz
The same is already installed at /home/polyml/polyml-5.3.0 locally.
There are two notable changes for improved performance:
41 matches
Mail list logo
