> You could try with a fresh build of Poly/ML:
Okay, I rebuilt Poly/ML (not libsha1 and libgmp though; apparently your
build script does not build those). The crashes still occured though. I
think I did everything correctly, because when I delete the files that
the compilation created, isabelle
See now:
changeset: 67033:09fb749d1a1e
user:wenzelm
date:Wed Nov 08 17:34:32 2017 +0100
files: src/Pure/Pure.thy
description:
formal dependency on "poly" executable;
I've myself got into problems finding odd spaces to remove from Pure ML
sources, in order to force a
On 08/11/17 15:45, Manuel Eberl wrote:
> Is there an easy way to disable that for testing purposes? Some line I
> have to remove from a .scala file or something?
It should be sufficient to remove the is_pure() here:
Is there an easy way to disable that for testing purposes? Some line I
have to remove from a .scala file or something?
Manuel
On 2017-11-08 15:44, Makarius wrote:
> On 08/11/17 15:39, Manuel Eberl wrote:
>>> If these crashes are happening at the end of the build process I would
>>> suspect that
On 08/11/17 15:39, Manuel Eberl wrote:
>> If these crashes are happening at the end of the build process I would
>> suspect that it is something to do with either the data sharing or
>> writing out the heap image.
>
> Does writing out of the heap happen also when I just do "isabelle build
> Pure"
If there are fixed-size integers in ML that raise an exception on
overflow, it should be possible to just do appropriate code_printing
setup similar to what Code_Target_Numeral does. We already have to
somehow magically map Isabelle's "int" type to ML's "IntInf" type, so
all we have to do is to
> If these crashes are happening at the end of the build process I would
> suspect that it is something to do with either the data sharing or
> writing out the heap image.
Does writing out of the heap happen also when I just do "isabelle build
Pure" as opposed to "isabelle build -b Pure"? Because
On 08/11/2017 14:13, Makarius wrote:
On 08/11/17 12:35, Tobias Nipkow wrote:
On 07/11/2017 23:13, Makarius wrote:
For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int. Thus it
On 08/11/17 09:21, Manuel Eberl wrote:
>
> After a lengthy bisection, I found that the first revision where no
> crashes occur is this one:
>
> changeset: 66920:aefaaef29c58
> user: wenzelm
> date: Thu Oct 26 13:44:41 2017 +0200
> summary: use Poly/ML 5.7.1 test version as
If these crashes are happening at the end of the build process I would
suspect that it is something to do with either the data sharing or
writing out the heap image. Writing the heap image does not involve any
concurrency but the data sharing does, so I would suspect the latter.
That has
Hi Makarius,
On 08/11/17 14:13, Makarius wrote:
On 08/11/17 12:35, Tobias Nipkow wrote:
On 07/11/2017 23:13, Makarius wrote:
For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int.
Thanks to lots of performance tuning for Poly/ML 5.7.1, both
HOL-ODE-Numerics and HOL-ODE-Examples have become non-slow (see
AFP/13b569160947).
Here is the reference timing on rather old lxbroy7, which is also a
regular test machine for http://isabelle.in.tum.de/devel/build_status/AFP:
Finished
On 08/11/17 12:35, Tobias Nipkow wrote:
>
> On 07/11/2017 23:13, Makarius wrote:
>> For Flyspeck-Tame a small performance loss remains. It might be worth
>> trying to configure the Isabelle/HOL codegen to use FixedInt instead of
>> regular (unbounded) Int. Thus it could become faster with Poly/ML
On 07/11/2017 23:13, Makarius wrote:
For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
than with 5.6.
Just as for Isabelle
I was not able to find out what exactly crashes and why, but while
trying to do that, I found out that the problem is actually not present
in the development version of Isabelle anymore.
After a lengthy bisection, I found that the first revision where no
crashes occur is this one:
changeset:
15 matches
Mail list logo
