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.
David
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 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.
since Isabelle/8905114fd23b, I'm seeing intermittent problems in the session "Iptables_Semantics_Examples_Big":
04:54:57.051 Run out of store - interrupting threads 04:54:57.051 Failed to recover - exiting
Here are the relevant log entries:
https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/581/consoleFul...
https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/583/consoleFul...
https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/584/consoleFul...
https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/585/consoleFul...
Is this a problem that can be solved by increasing the heap space? I didn't touch that setting and some build (#582) went through without problems.
The relevant environment settings are:
ML_PLATFORM="x86_64-linux" ML_OPTIONS="-H 4000 --maxheap 10G"
Cheers Lars
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 3000 --maxheap 30000 for that recently and it performs quite well (after months of not working at all).
The subsequent chart confirms the use of substantial heap space: http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/Iptabl...
Here are the overall results:
timing: 1:47:37 elapsed time, 8:17:10 cpu time, factor 4.62 ML timing: 1:47:33 elapsed time, 10:16:19 cpu time, factor 5.73 maximum heap: 29997 M average heap: 25795 M Isabelle version: e6a695d6a6b2 AFP version: fee069c9805b
Makarius
I've been using --minheap 3000 --maxheap 30000 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 30000 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.
The months refer to the intermediate state of the Poly/ML repository between stable 5.6 and the coming stable 5.7.1.
I am very glad that we are back to a version that works, even better than before. See the timing charts here: http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/index....
Makarius
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 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.
[0]: https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/586/consoleFull [1]: https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/586/artifact/heaps/polyml-5.7.1_x86_64-linux/log/Iptables_Semantics_Examples_Big/*view*/
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_Examples_Big mainly consists of generated code snippets. David has changed the arrangements for that significantly in Poly/ML 5.7.1: it is no longer on the regular heap.
Makarius
David,
On 8 Nov 2017, at 14:10, David Matthews <David.Matthews at prolingua.co.uk> 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.
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 <David.Matthews at prolingua.co.uk> 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.
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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 <rda at lemma-one.com> 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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
<fordavidm20171113.tgz>
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 start of the next segment and should have been adjusted. Zero-sized cells can arise from Array.fromList [].
David
On 13/11/2017 16:48, James Clarke wrote:
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 <rda at lemma-one.com> 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.
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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
David,
On 13 Nov 2017, at 20:47, David Matthews <David.Matthews at prolingua.co.uk> 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 that assertion fault but something similar.
The whole ProofPower build now goes through, so I'm fairly sure you've broken the back of this problem. I need to run some more tests on different OSs and with different Poly/ML compile time options. I'll get back to you about the outcome on Wednesday.
Regards,
Rob.
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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 <rda at lemma-one.com> wrote:
David,
On 13 Nov 2017, at 20:47, David Matthews <David.Matthews at prolingua.co.uk>
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 that assertion fault but something similar.
The whole ProofPower build now goes through, so I'm fairly sure you've broken the back of this problem. I need to run some more tests on different OSs and with different Poly/ML compile time options. I'll get back to you about the outcome on Wednesday.
Regards,
Rob.
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 <David.Matthews at prolingua.co.
uk> 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 <
David.Matthews at prolingua.co.uk> 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 <
David.Matthews at prolingua.co.uk> 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 > polyml at inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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... clang
******************************************************** * WARNING: Don't know the best CFLAGS for this system * * Use ./configure CFLAGS=... to specify your own flags * * (otherwise, a default of CFLAGS=-O3 will be used) * ********************************************************
2) The configure script doesn't complain about unrecognised options beginning with --enable. E.g,
configure --enable-garbage
just carries on. This fooled me when I managed to misspell --enable-intinf-as-int. If this is forced upon you by autoconfig, then so be it.
Many thanks for your rapid turnround with the earlier problems. Your great work on Poly/ML is very much appreciated.
Regards,
Rob.
Rob,
On 15/11/2017 17:10, Rob Arthan wrote:
- 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
- WARNING: Don't know the best CFLAGS for this system *
- Use ./configure CFLAGS=... to specify your own flags *
- (otherwise, a default of CFLAGS=-O3 will be used) *
I have seen this myself when building, remotely, on Mac OS X. I don't know if this is something that should be fixed or not.
- The configure script doesn't complain about unrecognised options beginning
with --enable. E.g,
configure --enable-garbage
just carries on. This fooled me when I managed to misspell --enable-intinf-as-int. If this is forced upon you by autoconfig, then so be it.
I did a search and came up with this: https://www.gnu.org/software/autoconf/manual/autoconf-2.68/html_node/Option-... . Poly/ML's autoconf script uses AC_CONFIG_SUBDIRS to build libffi so that will disable all option checking. There doesn't seem to be any way to override this and turn it on within the script but --enable-option-checking does seem to work. However ./configure --enable-option-cheking doesn't produce any warning at all so it doesn't help if that is misspelled.
Regards, David
On 15/11/17 09:58, David Matthews wrote:
On 15/11/2017 17:10, Rob Arthan wrote:
- 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
- WARNING: Don't know the best CFLAGS for this system? *
- Use ./configure CFLAGS=... to specify your own flags *
- (otherwise, a default of CFLAGS=-O3 will be used)??? *
I have seen this myself when building, remotely, on Mac OS X.? I don't know if this is something that should be fixed or not.
I have not tried the pre-release 5.7.1, but this warning is also reproducible on Linux with previous versions as described in [0]. I noticed no ill effects resulting from this, but perhaps the final output is not as tuned as it could be.
[0]: http://lists.inf.ed.ac.uk/pipermail/polyml/2017-September/002057.html
David,
On 15 Nov 2017, at 17:58, David Matthews <David.Matthews at prolingua.co.uk> wrote: I did a search and came up with this: https://www.gnu.org/software/autoconf/manual/autoconf-2.68/html_node/Option-... . Poly/ML's autoconf script uses AC_CONFIG_SUBDIRS to build libffi so that will disable all option checking. There doesn't seem to be any way to override this and turn it on within the script but --enable-option-checking does seem to work. However ./configure --enable-option-cheking doesn't produce any warning at all so it doesn't help if that is misspelled.
Thank! It's not as silly as it sounds:
alias conf="./configure --enable-option-checking"
is the latest addition to my .bashrc file.
Regards,
Rob.
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 toolchain.
[0]: https://github.com/libffi/libffi/blob/master/m4/ax_cc_maxopt.m4#L73-L155 [1]: http://git.savannah.gnu.org/gitweb/?p=autoconf-archive.git;a=blob_plain;f=m4...
On 16/11/17 13:42, Rob Arthan wrote:
David,
On 15 Nov 2017, at 17:58, David Matthews <David.Matthews at prolingua.co.uk> wrote: I did a search and came up with this: https://www.gnu.org/software/autoconf/manual/autoconf-2.68/html_node/Option-... . Poly/ML's autoconf script uses AC_CONFIG_SUBDIRS to build libffi so that will disable all option checking. There doesn't seem to be any way to override this and turn it on within the script but --enable-option-checking does seem to work. However ./configure --enable-option-cheking doesn't produce any warning at all so it doesn't help if that is misspelled.
Thank! It's not as silly as it sounds:
alias conf="./configure --enable-option-checking"is the latest addition to my .bashrc file.
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 >> <David.Matthews at prolingua.co.uk> 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 <David.Matthews at prolingua.co.uk> 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 > <David.Matthews at prolingua.co.uk> 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 >>> <David.Matthews at prolingua.co.uk> 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 > polyml at inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 <David.Matthews at prolingua.co.uk> 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 >> <David.Matthews at prolingua.co.uk> 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 >>>> <David.Matthews at prolingua.co.uk> 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 >> polyml at inf.ed.ac.uk >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > > > > > > > _______________________________________________ > polyml mailing list > polyml at inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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.1-inf/bin/poly Poly/ML 5.7.1 Release (Git version v5.7-290-g44b7b88e) 0.40 real 0.00 user 0.00 sys
Over repeated experiments, I see occasional upwards blips in the real time for 5.7, but 5.7.1 sticks doggedly to about 0.4 seconds.
Regards,
Rob.
On 25 Nov 2017, at 13:08, David Matthews <David.Matthews at prolingua.co.uk> wrote:
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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 <David.Matthews at prolingua.co.uk> 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 >>> polyml at inf.ed.ac.uk >>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> >> >> >> >> >> >> >> _______________________________________________ >> polyml mailing list >> polyml at inf.ed.ac.uk >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> > _______________________________________________ > polyml mailing list > polyml at inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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/2017 16:44, Rob Arthan wrote:
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.1-inf/bin/poly Poly/ML 5.7.1 Release (Git version v5.7-290-g44b7b88e) 0.40 real 0.00 user 0.00 sys
Over repeated experiments, I see occasional upwards blips in the real time for 5.7, but 5.7.1 sticks doggedly to about 0.4 seconds.
Regards,
Rob.
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 release 5.7.1.
This change a24f39a95ca9 causes a new problem when building modules/IntInfAsInt:
... echo "use "./ROOT.sml";" | ../../poly -q -error-exit Error 1
Before emitting that error, it appears to "hang" for several seconds.
The build procedure is that of Isabelle, e.g.:
$ isabelle build_polyml -m32 -s sha1 polyml-git --with-gmp $ isabelle build_polyml -m64 -s sha1 polyml-git --with-gmp
I've also seen the error with manual invocation of:
./configure --enable-intinf-as-int && make clean && make compiler
This effect is somewhat non-deterministic, but it appears quite reliably on my reference machines for x86-linux and x86_64-linux (Ubuntu 12.04 LTS).
In most other system configurations it appears to work.
Makarius
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 (44b7b88) as 5.7.1 and investigate the problem later. Are you certain the problem you've identified doesn't happen in that version?
David
On 25/11/2017 21: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'll give it a couple of days and then release 5.7.1.
This change a24f39a95ca9 causes a new problem when building modules/IntInfAsInt:
... echo "use "./ROOT.sml";" | ../../poly -q -error-exit Error 1
Before emitting that error, it appears to "hang" for several seconds.
The build procedure is that of Isabelle, e.g.:
$ isabelle build_polyml -m32 -s sha1 polyml-git --with-gmp $ isabelle build_polyml -m64 -s sha1 polyml-git --with-gmp
I've also seen the error with manual invocation of:
./configure --enable-intinf-as-int && make clean && make compiler
This effect is somewhat non-deterministic, but it appears quite reliably on my reference machines for x86-linux and x86_64-linux (Ubuntu 12.04 LTS).
In most other system configurations it appears to work.
Makarius _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 LTS test systems.
Makarius
David,
On 26 Nov 2017, at 09:14, David Matthews <David.Matthews at prolingua.co.uk> 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 view of this I'm inclined to release the version without this change (44b7b88) as 5.7.1 and investigate the problem later.
i?ve no objection to that as far as ProofPower is concerned, because the situation in the ProofPower build process where there a lots of little runs of Poly/ML is completely untypical of normal use of ProofPower. In normal use, a typical session is either an interactive session lasting hours or even days or a batch replay of a proof script that will take 10 seconds or more.
Regards,
Rob.
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'll give it a couple of days and then release 5.7.1.
This change a24f39a95ca9 causes a new problem when building modules/IntInfAsInt:
... echo "use "./ROOT.sml";" | ../../poly -q -error-exit Error 1
Before emitting that error, it appears to "hang" for several seconds.
The build procedure is that of Isabelle, e.g.:
$ isabelle build_polyml -m32 -s sha1 polyml-git --with-gmp $ isabelle build_polyml -m64 -s sha1 polyml-git --with-gmp
I've also seen the error with manual invocation of:
./configure --enable-intinf-as-int && make clean && make compiler
This effect is somewhat non-deterministic, but it appears quite reliably on my reference machines for x86-linux and x86_64-linux (Ubuntu 12.04 LTS).
In most other system configurations it appears to work.
I have tested this once again with Ubuntu 12.04 or 14.04 systems with x86 or x86_64. The problem can happen in all combinations, but more frequently on 12.04 than 14.04 and on x86 than x86_64.
Makarius
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 to be to get rid of the crow-bar thread completely.
However, I am releasing 44b7b88 as 5.7.1. The other changes can go into master and fixes-5.7.1.
David
On 26/11/2017 10:49, Makarius wrote:
On 25/11/17 22:45, Makarius wrote:
This change a24f39a95ca9 causes a new problem when building modules/IntInfAsInt:
... echo "use "./ROOT.sml";" | ../../poly -q -error-exit Error 1
Before emitting that error, it appears to "hang" for several seconds.
The build procedure is that of Isabelle, e.g.:
$ isabelle build_polyml -m32 -s sha1 polyml-git --with-gmp $ isabelle build_polyml -m64 -s sha1 polyml-git --with-gmp
I've also seen the error with manual invocation of:
./configure --enable-intinf-as-int && make clean && make compiler
This effect is somewhat non-deterministic, but it appears quite reliably on my reference machines for x86-linux and x86_64-linux (Ubuntu 12.04 LTS).
In most other system configurations it appears to work.
I have tested this once again with Ubuntu 12.04 or 14.04 systems with x86 or x86_64. The problem can happen in all combinations, but more frequently on 12.04 than 14.04 and on x86 than x86_64.
Makarius
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 delayed on exit. In the simplest Hello World GTK application, if it is open for more than about 3 s before being closed, it will take at least 43 s to close. (I assume that is terminated due to the crow-bar thread.) Oddly, another Hello World GTK demo (based on GApplication) doesn't exhibit this behaviour.
I agree that it is a bit late in the release cycle to address this and don't see the half second delay on exit being particularly problematic generally.
Regards, Phil
On 25/11/17 17:44, David Matthews wrote:
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/2017 16:44, Rob Arthan wrote:
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.1-inf/bin/poly Poly/ML 5.7.1 Release (Git version v5.7-290-g44b7b88e) ???????? 0.40 real???????? 0.00 user???????? 0.00 sys
Over repeated experiments, I see occasional upwards blips in the real time for 5.7, but 5.7.1 sticks doggedly to about 0.4 seconds.
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 race condition between the main thread and the crow-bar thread. Removing that delay meant that sometimes the crow-bar thread was missing the notification to shut down.
Regards, David
On 26/11/2017 22:07, Phil Clayton wrote:
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 delayed on exit.? In the simplest Hello World GTK application, if it is open for more than about 3 s before being closed, it will take at least 43 s to close.? (I assume that is terminated due to the crow-bar thread.) Oddly, another Hello World GTK demo (based on GApplication) doesn't exhibit this behaviour.
I agree that it is a bit late in the release cycle to address this and don't see the half second delay on exit being particularly problematic generally.
Regards, Phil
Hi David,
I just noticed the problem below [not critical for me].
When compiling a particular application on Ubuntu 14.04, 64 bit, with the latest PolyML revision (Git version v5.7.1-7-g01482bf), I get the exception :
??? ... ??? Exception- InternalError: asGenReg raised while compiling ??? Exception- Fail "Exception- InternalError: asGenReg raised while compiling" raised
Exactly the same exception is raised, at the same place, when compiling that application on Macosx (Sierra).
--
After some digging, it appears that the latest revision that compiles successfully the application was that one:
??? commit aa3b02654b38ad3faadc60c5960702cba6be87df ??? Author: David Matthews <dm at prolingua.co.uk> ??? Date:?? Fri Sep 22 19:13:26 2017 +0100
The next (commit dbffbc3778c12209f5fa0ac5a715105609eefc69) fails to compile earlier than the latest, with error: Fail "Exception- InternalError: AllocStore: in set raised while compiling"
The next one (commit fdefe56be03fe4fb4fe540c88ec1372e0cd4dab8) fails exactly as the latest revision does.
The application is fairly large and involves many files, so I did not try yet to isolate the part in sml source that fails to compile.? But I suppose there are some means that I don't know to print more precise information while compiling ...
Best, ? Bernard.
Hi Bernard, This is an assertion fault inside the code-generator. Probably the easiest way to deal with this would be for me to try compiling the code under the debugger. I can get it to trap when the exception is raised and see what is happening. It doesn't matter if the code is quite large so long as it is possible to compile it just by "using" a file. Could you either email it to me directly or put it somewhere I can pick it up?
Regards, David
On 29/11/2017 17:39, Bernard Berthomieu wrote:
Hi David,
I just noticed the problem below [not critical for me].
When compiling a particular application on Ubuntu 14.04, 64 bit, with the latest PolyML revision (Git version v5.7.1-7-g01482bf), I get the exception :
??? ... ??? Exception- InternalError: asGenReg raised while compiling ??? Exception- Fail "Exception- InternalError: asGenReg raised while compiling" raised
Exactly the same exception is raised, at the same place, when compiling that application on Macosx (Sierra).
--
After some digging, it appears that the latest revision that compiles successfully the application was that one:
??? commit aa3b02654b38ad3faadc60c5960702cba6be87df ??? Author: David Matthews <dm at prolingua.co.uk> ??? Date:?? Fri Sep 22 19:13:26 2017 +0100
The next (commit dbffbc3778c12209f5fa0ac5a715105609eefc69) fails to compile earlier than the latest, with error: Fail "Exception- InternalError: AllocStore: in set raised while compiling"
The next one (commit fdefe56be03fe4fb4fe540c88ec1372e0cd4dab8) fails exactly as the latest revision does.
The application is fairly large and involves many files, so I did not try yet to isolate the part in sml source that fails to compile.? But I suppose there are some means that I don't know to print more precise information while compiling ...
Best, ? Bernard.
-
bernard＠laas.fr -
David.Matthews＠prolingua.co.uk -
jrtc27＠jrtc27.com -
lars＠hupel.info -
makarius＠sketis.net -
matthew.fernandez＠gmail.com -
phil.clayton＠veonix.com -
Ramana.Kumar＠cl.cam.ac.uk -
rda＠lemma-one.com