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