Re: [polyml] Update to code-generator and run-time system interface

I've now pushed the first phase of garbage collection of the code area to git master. This marks unreachable code segments and fills them with HLT instructions so that any attempt to execute a segment that is supposedly garbage will produce an illegal instruction fault. I've dealt with

Re: [polyml] Update to code-generator and run-time system interface

> On 20 Oct 2016, at 18:01, David Matthews > wrote: > > On 20/10/2016 12:14, Rob Arthan wrote: >> During interactive development of a proof script it is usual to try >> things out repeatedly with frequent evaluations of minor variants of >> an attempted proof

Re: [polyml] Update to code-generator and run-time system interface

On 20/10/2016 12:14, Rob Arthan wrote: During interactive development of a proof script it is usual to try things out repeatedly with frequent evaluations of minor variants of an attempted proof step until you find one that works. It is ls also perfectly possible for a user to develop a

Re: [polyml] Update to code-generator and run-time system interface

> On 17 Oct 2016, at 20:38, Makarius wrote: > > On 20/09/16 14:15, David Matthews wrote: >> ... >> Currently, there is a leak because each top-level expression is compiled >> down to machine code even though the code is only executed once. My >> plan is to avoid that by

Re: [polyml] Update to code-generator and run-time system interface

Phil, Thanks for your comments. References from the heap to the start of a code cell are not too much of a problem. The difficulty is that some code cannot be garbage collected because it may still be running. Consider: fun f () = (OS.Process.sleep(Time.fromSeconds 60); print "Done\n");

Re: [polyml] Update to code-generator and run-time system interface

On 18/10/2016 13:43, Makarius wrote: On 17/10/16 23:58, David Matthews wrote: Although the lack of garbage collection of code would mean that repeatedly defining the same function would be a memory leak I would be surprised if it was a serious problem. Is it likely that one would repeatedly

Re: [polyml] Update to code-generator and run-time system interface

On 17/10/16 23:58, David Matthews wrote: > > Although the lack of garbage collection of code would mean that > repeatedly defining the same function would be a memory leak I would be > surprised if it was a serious problem. Is it likely that one would > repeatedly redefine the same function

Re: [polyml] Update to code-generator and run-time system interface

On 20/09/16 14:15, David Matthews wrote: > On 19/09/2016 21:15, Makarius wrote: >>> The handling of return addresses from functions has been simplified. A >>> consequence of this is that when pieces of code are compiled they are >>> stored in a separate area of memory rather than in the general

Re: [polyml] Update to code-generator and run-time system interface

On 22/09/16 16:50, David Matthews wrote: > On 19/09/2016 21:15, Makarius wrote: >> I am presently testing Poly/ML 38879127481c and Isabelle 9aed2da07200 >> and ran into a compiler problem in src/Pure/unify.ML: >> >> Exception- Fail "Exception- InternalError: chooseReg raised while >> compiling"

Re: [polyml] Update to code-generator and run-time system interface

Rob, I've had a look at this and it does appear to be more complicated than I thought. The pretty type is embedded fairly deeply in the compiler. The difference between PolyML.prettyPrint and PolyML.addPrettyPrinter is that PolyML.addPrettyPrinter is an infinitely overloaded function, like

Re: [polyml] Update to code-generator and run-time system interface

Makarius, On 19/09/2016 21:15, Makarius wrote: I am presently testing Poly/ML 38879127481c and Isabelle 9aed2da07200 and ran into a compiler problem in src/Pure/unify.ML: Exception- Fail "Exception- InternalError: chooseReg raised while compiling" raised I've pushed a fix and it no longer

Re: [polyml] Update to code-generator and run-time system interface

David, > On 20 Sep 2016, at 19:00, David Matthews > wrote: > > Rob, > The complication is that the pretty print datatype is essentially shared > between the compiler and the compiled code. If the compiler has been > compiled with a different length of int

Re: [polyml] Update to code-generator and run-time system interface

Rob and Makarius, First, thanks Rob for providing the patch. I've pushed the fix. I think the reason it works is that it was printing a full 32 or 64-bit value when the value was negative but the scan that was reading it back in again was expecting only a single byte. What is actually

Re: [polyml] Update to code-generator and run-time system interface

Makarius, > On 20 Sep 2016, at 16:42, Makarius wrote: > > On 20/09/16 16:50, Rob Arthan wrote: >> >> I think this patch fixes it: >> >> diff --git a/libpolyml/pexport.cpp b/libpolyml/pexport.cpp >> index b03b1da..a9ebd2e 100644 >> --- a/libpolyml/pexport.cpp >> +++

Re: [polyml] Update to code-generator and run-time system interface

> On 20 Sep 2016, at 16:42, Makarius wrote: > > On 20/09/16 16:50, Rob Arthan wrote: >> >> I think this patch fixes it: >> >> diff --git a/libpolyml/pexport.cpp b/libpolyml/pexport.cpp >> index b03b1da..a9ebd2e 100644 >> --- a/libpolyml/pexport.cpp >> +++

Re: [polyml] Update to code-generator and run-time system interface

David, After using the patch in my last post to enable me to build poly, ProofPower now builds and behaves as I would expect it to when compiled without —enable-intinf-as-int. When I compile with —enable-intinf-as-int I get a problem because the type of PolyML.PrettyBlock has a FixedInt in it

Re: [polyml] Update to code-generator and run-time system interface

On 20/09/16 16:50, Rob Arthan wrote: > > I think this patch fixes it: > > diff --git a/libpolyml/pexport.cpp b/libpolyml/pexport.cpp > index b03b1da..a9ebd2e 100644 > --- a/libpolyml/pexport.cpp > +++ b/libpolyml/pexport.cpp > @@ -158,7 +158,7 @@ void PExport::printObject(PolyObject *p) >

Re: [polyml] Update to code-generator and run-time system interface

David, Makarius, I think this patch fixes it: diff --git a/libpolyml/pexport.cpp b/libpolyml/pexport.cpp index b03b1da..a9ebd2e 100644 --- a/libpolyml/pexport.cpp +++ b/libpolyml/pexport.cpp @@ -158,7 +158,7 @@ void PExport::printObject(PolyObject *p) for (unsigned i = 0; i <

Re: [polyml] Update to code-generator and run-time system interface

On 20/09/16 14:16, David Matthews wrote: >> >> Instead of creating a new singleton string each time, it would refer to >> a vector of 256 pre-allocated values. > > That seems a very good idea. I've implemented it. I've tried to compile this version d7b9234f2793 using configure

Re: [polyml] Update to code-generator and run-time system interface

David, I have just pulled get rev d7b9234f2793aef14b984ad808bbdfc6e1c59403 and get the following when I do make compiler (after configure with no options other than —prefix=/usr/local/poly/dev): Making all in libpolymain make[3]: Nothing to be done for `all'. Making all in . ./polyimport

Re: [polyml] Update to code-generator and run-time system interface

On 19/09/2016 21:54, Makarius wrote: On 16/09/16 14:24, David Matthews wrote: The representation of strings has been simplified. Previously, single character strings were represented by the character itself as a tagged value. This was largely a relic of SML 90 which didn't have a separate

Re: [polyml] Update to code-generator and run-time system interface

On 19/09/2016 21:15, Makarius wrote: The handling of return addresses from functions has been simplified. A consequence of this is that when pieces of code are compiled they are stored in a separate area of memory rather than in the general heap and not garbage-collected. Does that mean that

Re: [polyml] Update to code-generator and run-time system interface

Rob, Thanks for that. It was using signed rather than unsigned comparisons. I've pushed a fix. Regards, David On 18/09/2016 22:35, Rob Arthan wrote: Many thanks for the quick turn round on these issues. I have got quite a bit further. The ProofPower build is now failing as a result of the

Re: [polyml] Update to code-generator and run-time system interface

David, Many thanks for the quick turn round on these issues. I have got quite a bit further. The ProofPower build is now failing as a result of the following issue: 5) In string comparisons, the leading character is being treated as negative if it has character code greater than 127: E.g., >

Re: [polyml] Update to code-generator and run-time system interface

Rob, Thanks for that and for cutting it down to something manageable. As a result I've been able to track down and fix the problem. Let me know as and when you find anything else. Regards, David On 17/09/2016 16:20, Rob Arthan wrote: David, On 17 Sep 2016, at 14:49, Rob Arthan

Re: [polyml] Update to code-generator and run-time system interface

David, > On 17 Sep 2016, at 14:49, Rob Arthan wrote: … > … I am getting a segfault somewhere in the > ProofPower parser generator. I will report again when I have > isolated that. To the list of three issues in my previous e-mail, I can now add: 4) In some circumstances a

Re: [polyml] Update to code-generator and run-time system interface

David, I have been having a go at building ProofPower with the latest updates. Here is some miscellaneous feedback: 1) Are these two errors in the configure output harmless? (This is on Mac OS X using Apple’s Xcode tools.) checking for __attribute__((visibility("hidden")))... no clang: error: