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 40s
(it was 20s in 5.7 and earlier) which forces an process exit if the
other threads haven't finished in that time. There were issues with
race conditions in earlier versions of Poly/ML which meant that
sometimes the main thread would not correctly detect that the threads
had exited but I thought all that had been fixed.
Regards,
David
On 25/11/2017 09:24, Phil Clayton wrote:
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 separate poly sessions
that update the saved the state. That would give an expected delay of
at most
262 * 0.49 s
=
128 s
which is not far off the 117 s extra delay below. I think that explains
it.
Phil
On 23/11/17 19:46, Phil Clayton wrote:
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
real 1m37.832s
user 1m33.262s
sys 0m15.108s
Poly/ML 5.7.1g44b7b88
real 3m34.839s
user 1m38.777s
sys 0m19.593s
I have kept all other things equal: the only change is the version of
Poly/ML. This suggests that Poly/ML is waiting for something.
Unfortunately I haven't had time to investigate this.
Regards,
Phil
On 13/11/17 20:47, David Matthews wrote:
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 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 savestate.cpp,
line 929.
I've attached a tarball with the evidence. This time it doesn't seem
to be deterministic, sometimes it
gets further than others.
Regards,
Rob.
On 13 Nov 2017, at 13:33, David Matthews
<[email protected]> wrote:
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 solve it but let me know if there are
still problems.
Regards,
David
On 13/11/2017 09:12, Phil Clayton wrote:
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 haven't tested 04d3c95). Rob's second example (20171112)
should reproduce this but doesn't. I modified the example as
attached to use a single session and it gives the following error
message but I don't know if this error is related:
pp-ml: gc_mark_phase.cpp:743: void CheckMarksOnCodeTask(GCTaskId*,
void*, void*): Assertion `obj->ContainsNormalLengthWord()' failed.
Regards,
Phil
On 12/11/17 19:21, Rob Arthan wrote:
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
<[email protected]> wrote:
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
<[email protected]> 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 various bugs and sort
out performance issues. I've been working with Makarius on
dealing with those that affect Isabelle and we now seem to
have dealt with everything. I'd like to ask everyone to try
out the current version and let me know if there is anything
that would stand in the way of a release.
The ProofPower build fails with an assertion failure:
Assertion failed: (t->tree[r] == 0), function AddTreeRange,
file savestate.cpp, line 896.
This is on Mac OS Sierra 10.12.6 with Poly/ML version
v5.7-283-g04d3c95 .
I haven't tried any other OSs. I presume this is happening
where my main program calls
PolyML.SaveState.loadState.
I've attached a tarball of a cut-down set of source files that
exhibits the problem
together with a shell script that simulates what the ProofPower
make file does.
Regards,
Rob.
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
