David, > On 13 Nov 2017, at 20:47, David Matthews <[email protected]> > 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 <[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
