Re: [polyml] Fwd: [isabelle] insufficient memory exception in polyml

2010-07-27 Thread David Matthews
Phil Clayton wrote: The Poly/ML download page ( http://www.polyml.org/download.html ) says: ./configure make make compiler make make install Should the third make command be 'make compiler' then? (I've always found just 'make' does nothing.) I've updated the web page for the current SVN. T

Re: [polyml] Fwd: [isabelle] insufficient memory exception in polyml

2010-07-26 Thread Phil Clayton
David Matthews wrote: One important point to make is that you should run "make compiler" TWICE i.e. make make compiler make compiler The reason for this is that the format of exception handlers has changed and if it is only run once there is danger that a raised exception could encounter code

Re: [polyml] Fwd: [isabelle] insufficient memory exception in polyml

2010-07-26 Thread Gerwin Klein
On 26/07/2010, at 6:14 PM, David Matthews wrote: >> It's a bit difficult to provide good data at the moment, because I'm >> travelling and have only a low-bandwidth connection to my machine in >> the office, but I can produce more when I'm back mid Aug. > > Let's look into this more carefully when

Re: [polyml] Fwd: [isabelle] insufficient memory exception in polyml

2010-07-26 Thread David Matthews
Gerwin Klein wrote: On 26/07/2010, at 1:35 PM, David Matthews wrote: Did you rebuild the compiler before you ran with that version (i.e. make compiler) or use the original compiler? I checked out the svn trunk version from scratch, and did run "make compiler". OK. This is probably as good

Re: [polyml] Fwd: [isabelle] insufficient memory exception in polyml

2010-07-26 Thread Gerwin Klein
On 26/07/2010, at 1:35 PM, David Matthews wrote: > Gerwin Klein wrote: >> Since the below I've run a few more experiments, and the theory does >> run fine with image built after less than 25min with the current svn >> trunk version of polyml on x86_64-darwin (5.4 Experimental). >> However, with t

Re: [polyml] Fwd: [isabelle] insufficient memory exception in polyml

2010-07-26 Thread David Matthews
Gerwin Klein wrote: Since the below I've run a few more experiments, and the theory does run fine with image built after less than 25min with the current svn trunk version of polyml on x86_64-darwin (5.4 Experimental). However, with the polyml-3.1-fixes version, it is still running after 45min w

[polyml] Fwd: [isabelle] insufficient memory exception in polyml

2010-07-24 Thread Gerwin Klein
This looks more like a polyml issue than an Isabelle issue, so I'm reposting here. Since the below I've run a few more experiments, and the theory does run fine with image built after less than 25min with the current svn trunk version of polyml on x86_64-darwin (5.4 Experimental). However, wit