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 <r...@lemma-one.com> wrote: > David, > > > On 13 Nov 2017, at 20:47, David Matthews <david.matth...@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.matth...@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.matth...@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.matth...@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@inf.ed.ac.uk > >>>>>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > >>>>> > >>>>> > >>>>> > >>>>> > >>>>> > >>>>> > >>>>> > >>>>> _______________________________________________ > >>>>> polyml mailing list > >>>>> polyml@inf.ed.ac.uk > >>>>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > >>>>> > >>>> _______________________________________________ > >>>> polyml mailing list > >>>> polyml@inf.ed.ac.uk > >>>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > >>> _______________________________________________ > >>> polyml mailing list > >>> polyml@inf.ed.ac.uk > >>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > >> _______________________________________________ > >> polyml mailing list > >> polyml@inf.ed.ac.uk > >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > _______________________________________________ > > polyml mailing list > > polyml@inf.ed.ac.uk > > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > _______________________________________________ > polyml mailing list > polyml@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >
_______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
