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

[polyml] SVN vs. Poly/ML 5.4

2010-07-26 Thread Makarius
On Mon, 26 Jul 2010, David Matthews wrote: This is probably as good an opportunity as any to summarise the current state of the SVN version. I'd be interested in feedback if anyone wants to try this out. We have the Poly/ML SVN version running in parallel with our regular Isabelle Tests

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 you

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] insufficient memory exception in polyml

2010-07-26 Thread Makarius
On Mon, 26 Jul 2010, 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? Maybe you should also try to rebuild the official 5.3.0 version from source.