We are approaching the point at which the current version of Git master
is ready for release as Poly/ML 5.7.1. Version 5.7 introduced a number
of significant changes and it has taken quite a bit of work since then
to fix various bugs and sort out performance issues. I've been working
with Mak
Dear David,
> We are approaching the point at which the current version of Git master
> is ready for release as Poly/ML 5.7.1. Version 5.7 introduced a number
> of significant changes and it has taken quite a bit of work since then
> to fix various bugs and sort out performance issues. I've been
On 08/11/17 15:23, Lars Hupel wrote:
>
> since Isabelle/8905114fd23b, I'm seeing intermittent problems in the
> session "Iptables_Semantics_Examples_Big":
>
> The relevant environment settings are:
>
> ML_PLATFORM="x86_64-linux"
> ML_OPTIONS="-H 4000 --maxheap 10G"
I've been using --minheap 300
> I've been using --minheap 3000 --maxheap 3 for that recently and it
> performs quite well (after months of not working at all).
I'll try bumping the memory. Although the "months of not working" is not
quite correct, because it worked fine with 10 GB in 5.6.
__
On 08/11/17 15:49, Lars Hupel wrote:
>> I've been using --minheap 3000 --maxheap 3 for that recently and it
>> performs quite well (after months of not working at all).
>
> I'll try bumping the memory. Although the "months of not working" is not
> quite correct, because it worked fine with 10
> I'll try bumping the memory. Although the "months of not working" is not
> quite correct, because it worked fine with 10 GB in 5.6.
After a strange crash yesterday that didn't even print an error message
[0,1] it seems we're back to normal now.
I still don't quite understand why the memory need
On 10/11/17 10:38, Lars Hupel wrote:
>
> I still don't quite understand why the memory needs to be increased so
> much. I thought that that's not necessarily a good thing because it
> means heap compactification occurs less often and hence might increase
> GC runtime etc.
Iptables_Semantics_Examp
David,
> On 8 Nov 2017, at 14:10, David Matthews
> wrote:
>
> We are approaching the point at which the current version of Git master is
> ready for release as Poly/ML 5.7.1. Version 5.7 introduced a number of
> significant changes and it has taken quite a bit of work since then to fix
> va
Rob,
Thanks for doing that. I've pushed a commit that seems to have fixed it.
Regards,
David
On 11/11/2017 18:47, Rob Arthan wrote:
David,
On 8 Nov 2017, at 14:10, David Matthews wrote:
We are approaching the point at which the current version of Git master is
ready for release as Poly/ML
David,
Thanks. Unfortunately, after pulling your fix, I get the same assertion failure
2 files further
on in the ProofPower build. The attached tarball contains files similar to the
ones I sent
yesterday to exhibit the problem.
Regards,
Rob.
> On 12 Nov 2017, at 15:41, David Matthews
> wrot
David,
I also get a failure building ProofPower but not the same as Rob:
pp-ml: savestate.cpp:881: void LoadRelocate::AddTreeRange(SpaceBTree**,
unsigned int, uintptr_t, uintptr_t): Assertion `s >= r && s <= 256' failed.
This is on a Linux x86_64 machine and occurs with commit 524fe72 (I
hav
Thanks, both of you for your contributions. I've had another look at it
and I've applied another fix. The problem was really that it was
reading beyond the end of an array which meant that whether and how it
failed depended on the values it found. Hopefully the latest fix
(e968c38) will solv
David,
Thanks again, but I've got two ProofPower source files further on and then I
get a different assertion failure:
Assertion failed: (val.AsAddress() > descr->originalAddress && val.AsAddress()
<= (char*)descr->originalAddress + descr->segmentSize), function
RelocateAddressAt, file savesta
Without having looked at the code in question, that assertion seems somewhat
unusual; a typical in-range check has >= and <. Perhaps it's a bit naive, but
have you tried that?
James
> On 13 Nov 2017, at 16:32, Rob Arthan wrote:
>
> David,
>
> Thanks again, but I've got two ProofPower source
Rob,
Thank you for putting up with this. We're gradually making progress.
I've pushed a further change and this example now seems to work. I
didn't actually get that assertion fault but something similar.
Regards,
David
On 13/11/2017 16:32, Rob Arthan wrote:
David,
Thanks again, but I've
Actually, no. Each cell has a length word and pointers always point
after this so the assertion check is correct. However the bug was
related to there being a zero-sized cell, i.e. a cell that only has a
length word, at the top of a segment. The cell address looks as though
it is at the star
David,
> On 13 Nov 2017, at 20:47, David Matthews
> wrote:
>
> Rob,
> Thank you for putting up with this.
No problem. Thank you for all your hard work with Poly/ML.
> We're gradually making progress. I've pushed a further change and this
> example now seems to work. I didn't actually get t
Hi David,
I just wanted to add that the latest git master (26c678b6) still fails to
build HOL4 with the following:
Fail "Exception- InternalError: codeToPRegRev raised while compiling"
similar to as we have discussed on other threads.
Cheers,
Ramana
On 14 November 2017 at 09:32, Rob Arthan wro
David,
I've done my other tests and it's working fine. I have just a couple of
observations.
1) On Mac OS (and presumably any system with clang as the C compiler), the
configure script gives a warning. (I just let this go by and nothing seems to
have gone wrong.)
checking for C compiler vendor
Rob,
On 15/11/2017 17:10, Rob Arthan wrote:
1) On Mac OS (and presumably any system with clang as the C compiler), the
configure script gives a warning. (I just let this go by and nothing seems to
have gone wrong.)
checking for C compiler vendor... clang
**
On 15/11/17 09:58, David Matthews wrote:
On 15/11/2017 17:10, Rob Arthan wrote:
1) On Mac OS (and presumably any system with clang as the C compiler), the
configure script gives a warning. (I just let this go by and nothing seems to
have gone wrong.)
checking for C compiler vendor... clang
**
David,
> On 15 Nov 2017, at 17:58, David Matthews
> wrote:
> I did a search and came up with this:
> https://www.gnu.org/software/autoconf/manual/autoconf-2.68/html_node/Option-Checking.html
> .
> Poly/ML's autoconf script uses AC_CONFIG_SUBDIRS to build libffi so that will
> disable all opti
This actually looks like a weakness that libffi doesn't explicitly support Clang [0]. Swimming further upstream, this
support is missing in the Autoconf Archive [1]. Whether this is worth fixing is debatable as even the GCC options in
this script don't seem particularly well chosen for a modern t
David,
That also fixed the issue for me.
I have been using the latest commit (g44b7b88) without issue. My only
observation is that there is a significant increase in the ProofPower
build times:
Poly/ML 5.7
real1m37.832s
user1m33.262s
sys 0m15.108s
Poly/ML 5.7.1g44b7b88
real
I have just realized what is probably accounting for the delay below. I
have noticed recently that there is a slight delay when exiting the poly
session.
echo | time poly
gives 0.49 s elapsed time on my machine. After a build of ProofPower
there are 262 SML files and most are processed in
That's odd. When I run it it exits immediately. Exactly what platform
are you running it on?
When a thread calls OS.Process.exit, which is what happens when
end-of-stream is detected by the compiler, it marks all the other
threads to exit and then starts a "crow-bar" thread. That waits for
David,
Knowing Phil he will be using some version of Linux, but I see similar results
on Mac OS:
E.g., on Mac OS High Sierra 10.13.1:
rda]- echo | time /usr/local/poly/5.7-inf/bin/poly
Poly/ML 5.7 Release
0.00 real 0.00 user 0.00 sys
rda]- echo | time /usr/local/poly/5.7.
Rob,
I've had a better look and I found that I was seeing this as well. I've
pushed a fix and it no longer seems to be doing it. It's a very small
change so I would be very surprised if it has broken anything but I'll
give it a couple of days and then release 5.7.1.
Regards,
David
On 25/11
On 25/11/17 18:44, David Matthews wrote:
> I've had a better look and I found that I was seeing this as well. I've
> pushed a fix and it no longer seems to be doing it. It's a very small
> change so I would be very surprised if it has broken anything but I'll
> give it a couple of days and then
I don't see that myself but it's certainly possible. A delay followed
by Error 1 suggests that it is relying on the crow-bar thread to stop.
The fact that this only happens on some platforms suggests a race
condition.
In view of this I'm inclined to release the version without this change
(4
On 26/11/17 10:14, David Matthews wrote:
>
> In view of this I'm inclined to release the version without this change
> (44b7b88) as 5.7.1 and investigate the problem later. Are you certain
> the problem you've identified doesn't happen in that version?
Yes, 44b7b88 works on these Ubuntu 12.04 LT
On 25/11/17 22:45, Makarius wrote:
> On 25/11/17 18:44, David Matthews wrote:
>
>> I've had a better look and I found that I was seeing this as well. I've
>> pushed a fix and it no longer seems to be doing it. It's a very small
>> change so I would be very surprised if it has broken anything but
I tried it on Ubuntu 16.04 and indeed it showed the problem. I had been
testing on Debian stable. It seems to be a race condition which only
showed up because this latest change removed the delay which was
"fixing" the race. I don't know why it only showed up in Ubuntu but the
answer seems t
David,
> On 26 Nov 2017, at 09:14, David Matthews
> wrote:
>
> I don't see that myself but it's certainly possible. A delay followed by
> Error 1 suggests that it is relying on the crow-bar thread to stop. The fact
> that this only happens on some platforms suggests a race condition.
>
> In
David,
As Rob says, I am using Linux (4.13.12-100.fc25.x86_64 from Fedora 25
updates).
I have tried the updated version (ga24f39a) and this fixes the issue.
ProofPower builds in the expected time. However, I have tried a few
more tests and find that some compiled applications are very delay
Phil,
I've released 5.7.1 now using 44b7b88. That means the 400ms delay
remains in that version but everything else should work.
The crow-bar thread has been removed in current master (01482bf) so that
should no longer show the 40s delay. The problem was that the 400ms
delay was masking a r
36 matches
Mail list logo
