Re: [polyml] Unable to allocate immutable area

2008-11-18 Thread David Matthews
Tom Ridge wrote: I am using polyml to run hol. From within emacs, I normally use C-c C-r to send a region to the hol process. This involves emacs writing out to a tmp file, and the hol process attempting to use the file back in. After a lot of proof, I get the following error: Unable to

Re: [polyml] loadState and threads

2008-11-19 Thread David Matthews
Phil, The idea of loadState is to be able to load information saved in a previous session and it doesn't always work as expected when you reload the state into the session that saved it. That isn't something I imagined someone wanting to do. loadState restores the values of references in

Re: [polyml] printing out references

2008-11-28 Thread David Matthews
Michael Norrish wrote: How can I prettyprint a reference value so that I get some idea from looking at the output whether two such values are the same or not? I would suggest using PolyML.showSize. This displays the actual contents of an arbitrary data structure in hex and includes the

Re: [polyml] loadState and threads

2008-11-28 Thread David Matthews
Phil, Philip Clayton wrote: My understanding of loading a state is that new objects are created whether or not the same object is already loaded. That seems the right thing to do, as you say. When loading a child state however, I would expect only objects in the child state to be created

Re: [polyml] loadState and threads

2008-12-03 Thread David Matthews
Rob, The current saveState/loadState saves and restores the whole state. It works at the level of the memory and has no knowledge of what the values represent. When you load test2.polydb this simply restores all global references to the values they had when you saved the state. In

[polyml] Re: Segmentation fault when saving state

2009-01-29 Thread David Matthews
Phil, I've now looked into this and hopefully fixed it in CVS. saveState gets a new segment of memory from the system each time it is called and copies everything that is reachable from the root into that. As well being written out the segment needs to be retained as a whole since if a

[polyml] Updates in CVS

2009-01-29 Thread David Matthews
There have been a couple of updates to the Poly/ML CVS repository recently apart from those already mentioned on the list. They are both in the C++ run-time system. The mechanism for waiting for external events has been improved which mainly affects Windows pipes and processes. In

Re: [polyml] ML compiler

2009-02-06 Thread David Matthews
Lucas Dixon wrote: Some answers to my own questions... saves only 1MB, despite the fact that I have many deeply nested functors in my code. Changing the max inline depth also seems to have pretty much no change on the size of generated code so now I still wonder how I got 20MB of compiled

Re: [polyml] Move to Subversion

2009-03-23 Thread David Matthews
Basile STARYNKEVITCH wrote: David Matthews wrote: CVS is getting rather old now and most projects seem to have moved on. I've now moved Poly/ML's CVS repository to subversion and taken the opportunity to enable Trac on the SourceForge site. To download the development version you need svn co

Re: [polyml] Compilation error on AIX

2009-03-23 Thread David Matthews
nitralime wrote: I am trying to compile PolyML 5.2.1 on AIX 5L. After executing configure script ./configure --prefix=/usr/local/polyml and gmake I got the following error message: g++ -DHAVE_CONFIG_H

Re: [polyml] Compilation error on AIX

2009-03-24 Thread David Matthews
nitralime wrote: On Mon, Mar 23, 2009 at 6:55 PM, David Matthews I don't know how time consuming the implementation of XCOFF support would be. Excuse me my naive question: Is there any plan to implement it? None at the moment. It shouldn't be a great deal of work especially

[polyml] Syntax of fun bindings and constructor application

2009-07-03 Thread David Matthews
I've just been updating the type checking error messages for fun declarations and as part of the process I've been looking at the parsing. The syntax of a fun binding is similar to a pattern in many ways and the overlap between them is such that the easiest way to parse them is to treat them

Re: [polyml] Performance problems with saving and loading state

2009-07-27 Thread David Matthews
Rob Arthan wrote: On 26 Jul 2009, at 19:37, David Matthews wrote: Rob Arthan wrote: We have performance problems with ProofPower when compiled with Poly/ML using the latest sources as compared with version 5.2.1. The main problem is with loading a large state. In some of QinetiQ's tests

Re: [polyml] Performance problems with saving and loading state

2009-07-29 Thread David Matthews
Philip Clayton wrote: I have rebuilt ProofPower using this file and the times to start up are back to normal. I've set a build going to test the 150MB databases but won't know the outcome until tomorrow. This is looking good so far... Good. I've committed that change. It looks like it has

[polyml] Deferred signature copying

2009-08-04 Thread David Matthews
Last week I committed into SVN the last major piece of some changes I've been making to the modules implementation. There are a lot of detailed changes but this last bit involves a change to way structures and functors are implemented. Previously, whenever a signature was used it was

Re: [polyml] Out of memory when saving state

2009-08-05 Thread David Matthews
Philip Clayton wrote: When using SaveState.saveChild to save the state, I am getting: Timing - parse:0.0, semantics:0.0, translate:0.0, generate:0.0, run:43.7 Exception SysErr: SysErr (Out of Memory, SOME ENOMEM) raised Even after shareCommonData and fullGC I notice that objSize

Re: [polyml] Poly/ML build fails on cygwin

2009-08-27 Thread David Matthews
Rob, All I can say is that it works for me with 5.2.1 downloaded from SourceForge and the most recent update of Cygwin. Make sure that you have an up-to-date version of Cygwin. Try running ./polyimport -H 10 polytemp.txt exportPoly.sml and see if you get any other error messages. Regards,

Re: [polyml] Poly/ML on Windows (MinGW/MSYS port)

2009-09-04 Thread David Matthews
Hi Gabriel, Gabriel Dos Reis wrote: I tried to build Poly/ML on Windows using the MSYS/MinGW toolchains, but was unsuccessful The build failed with: This is an out-of-source build, meaning that I keep the build directory separate from the vanilla Poly/ML source tree. I had a quick look

Re: [polyml] Poly/ML on Windows (MinGW/MSYS port)

2009-09-05 Thread David Matthews
Gabriel Dos Reis wrote: On Fri, Sep 4, 2009 at 3:49 AM, David Matthewsdavid.matth...@prolingua.co.uk wrote: Doing an out-of-source build won't currently work. You may be able to build the library but compiling the basis library into Poly/ML assumes that it is running within the directory that

Re: [polyml] Poly/ML on Windows (MinGW/MSYS port)

2009-09-06 Thread David Matthews
Gabriel Dos Reis wrote: I'm using the latest MinGW/MSYS releases, with full developer toolsets. On my machine (Windows XP, 32-bit), the header is located under /ming/mingw32/include. The in-source build indeed is now OK. Thanks! The out-of-source build still fails for libpolyml. Now, it is

Re: [polyml] Building Poly/ML on MacOS X 10.6

2009-09-07 Thread David Matthews
r...@lemma-one.com wrote: My first attempt to compile Poly/ML 5.2.1 on Snow Leopard (= MacOS X 10.6) resulted in an error due to a cast of a pointer to an int in libpolyml/x86_dep.cpp. There is a fix for this in the latest source, but the build then falls over as follows: Rob, I had an email

Re: [polyml] Building Poly/ML on MacOS X 10.6

2009-09-07 Thread David Matthews
Rob, r...@lemma-one.com wrote: If I do: ./configure --build=x86_64-darwin then make works, but make cvs then fails like this: make all-recursive Making all in libpolyml make[2]: Nothing to be done for `all'. Making all in libpolymain make[2]: Nothing to be done for `all'. make[2]: Nothing

Re: [polyml] Building Poly/ML on MacOS X 10.6

2009-09-07 Thread David Matthews
Just a further update on this: the problem seems to be the config.guess script which reports that this is a 32-bit processor rather than a 64-bit one. I've updated to the latest version from the master version at git.savannah.gnu.org but I'm not sure that this fixes it. I came across a

Re: [polyml] Re: [Building Poly/ML on MacOS X 10.6]

2009-09-09 Thread David Matthews
Rob, Can I take it that the current SVN builds on Mac OS 10.6 without any extra options, although your Makefiles will have to add the -segprot option? I may need to ask you test it again if the official config.guess is updated to include support for 10.6. Eventually I'd like to remove the

[polyml] Re: Suppressing pretty-printing

2009-09-16 Thread David Matthews
Rob Arthan pointed out that the new behaviour in 5.3 of printing abstract types isn't always desirable and that it might be useful to explain how to restore the old behaviour. I've added an entry to the FAQ http://www.polyml.org/FAQ.html#defaultpretty which includes instructions on how to

Re: [polyml] Latest SVN version

2009-11-03 Thread David Matthews
Rob, Rob Arthan wrote: RC2 is working fine for ProofPower. I am testing on Snow Leopard using SVN rev 924 of the Poly/ML source. I tried both x86_64 and i386 architectures - to get the latter work you still seem to have to specify CXXFLAGS etc. I see that configure is still using xmkmf to test

[polyml] Version 5.3 Release

2009-11-09 Thread David Matthews
I've now released Poly/ML version 5.3 on the SourceForge site. As well as the usual source code I've also built a Windows installer script that will install a binary version on Windows. The release notes are at http://www.polyml.org/docs/ReleaseNotes.html which describe what's new in this

Re: [polyml] Latest SVN version

2009-11-10 Thread David Matthews
Rob, Rob Arthan wrote: David, Out of interest, I have tried this and it compiles OK. However I think that multi-threading is causing a problem with it. If I execute: val shell = Motif.XtAppInitialise HelloWorld HW [] []; val btn = Motif.XmCreatePushButton shell hello-btn [

Re: [polyml] Motif Poly/ML configuration Issues(Errors)

2009-11-28 Thread David Matthews
I don't want to discourage you but you've asked some rather basic questions along with some more advanced ones. You might benefit from looking at a book on the language. I'll try to give a quick answer to your questions. Question 1: get error when run open XWindows

Re: [polyml] Pretty-printing in version 5.3

2009-12-14 Thread David Matthews
Rob, I think the problem is actually with the wrapper function that is used to emulate install_pp in terms of addPrettyPrinter. When I wrote a version of your pretty printer directly in the new form (included below) it worked as expected. I've now written a quick document describing the new

Re: [polyml] Inspecting structures

2010-01-27 Thread David Matthews
Currently there isn't any straightforward ways of doing any of these. They are all things that would be nice to have and we may get round to doing as part of the general improvements in user-interface. Some of the hooks are there to do these kinds of things but they're not very apparent.

Re: [polyml] eval (or use-ing from a string)

2010-02-10 Thread David Matthews
I don't think it was a deliberate omission. It's easy to write in terms of PolyML.compiler so maybe it was just that there wasn't much demand for it. If you want to send me your code I'll have a look at it and see if it should be included. Regards, David Ramana Kumar wrote: Are there any

Re: [polyml] run-time cost of single-constructor datatypes

2010-03-04 Thread David Matthews
Brian Huffman wrote: Hello all, In Haskell, when I declare the following type: data Foo = MkFoo (Int, Bool) the constructor MkFoo has a run-time cost: A pointer must be dereferenced whenever I pattern-match on MkFoo, and memory is allocated when I apply the MkFoo constructor. On the other

Re: [polyml] segmentation fault during build

2010-03-08 Thread David Matthews
Ramana Kumar wrote: I decided to update Poly/ML svn today and ran into this problem. Not a big deal since my old version still works, but maybe there's a bug to be found. ... Use: basis/PrettyPrinter.sml Use: basis/FinalPolyML.sml Use: basis/TopLevelPolyML.sml /bin/sh: line 1: 16849

Re: [polyml] run-time cost of single-constructor datatypes

2010-03-08 Thread David Matthews
Brian Huffman wrote: For reasons related to pretty-printing (which, to be honest, I don't completely understand), other developers have determined that opaque ascription should be avoided in the Isabelle sources. So most uses of opaque ascription have now been replaced with abstype, like this:

Re: [polyml] segmentation fault during build

2010-03-10 Thread David Matthews
I've fixed a bug in the X86/64 version (SVN 1082) and it now builds successfully. David Makarius wrote: On Mon, 8 Mar 2010, David Matthews wrote: Ramana Kumar wrote: I decided to update Poly/ML svn today and ran into this problem. Not a big deal since my old version still works, but maybe

[polyml] Profiling on Mac OS X

2010-04-04 Thread David Matthews
There's a problem using PolyML.profiling 1 on Mac OS X and think this has been discussed before. Time profiling works by setting a timer and then examining the program counter when the timer goes off to determine which function is being executed. Linux supports per-thread timers and when a

Re: [polyml] Documentation of Poly/ML opcode

2010-05-01 Thread David Matthews
Hi, The opcodes in int_opcodes.h apply only to the interpreted version of Poly/ML and the interpreter is only used on platforms where there is no native code-generator. There's not much, if any, documentation for the internals of the compiler or run-time system. Probably the most useful

Re: [polyml] 5.3 variability in Posix.Process.exec

2010-05-11 Thread David Matthews
Michael Norrish wrote: It turns out that on Mac OS X execv returns ENOTSUP if the process is multi-threaded. You need to use Posix.Process.fork first to start a new process: case Posix.Process.fork() of SOME _ = OS.Process.exit OS.Process.success | NONE = Posix.Process.exec(/bin/ls, [ls]);

Re: [polyml] 5.3 variability in Posix.Process.exec

2010-05-12 Thread David Matthews
Michael Norrish wrote: Well, it seems as if the problem for exec is just on MacOS, and I'm happy to fork there, even if it's annoying to have to do so. Cygwin is not really relevant, but I suppose that, out of idle curiosity, it would nice to know if Posix.Process.exec worked there. My

Re: [polyml] 5.3 variability in Posix.Process.exec

2010-05-13 Thread David Matthews
Makarius wrote: On Wed, 12 May 2010, Michael Norrish wrote: Cygwin is not really relevant, but I suppose that, out of idle curiosity, it would nice to know if Posix.Process.exec worked there. I have checked the (long) mail exchange with David from 2 years ago, when we sorted out many issues

Re: [polyml] Poly/ML exit codes

2010-05-13 Thread David Matthews
Michael Norrish wrote: On 13/05/10 11:01, Michael Norrish wrote: The presence of Killed makes me think that the script is being killed by an external signal, perhaps a SIGSEGV caused by hitting a limit on stack-size. But is this plausible? Would Poly/ML catch that signal and then exit with

Re: [polyml] Poly/ML interpreter's opcodes

2010-05-19 Thread David Matthews
Yue, Yue Li wrote: Right now I'm studying the Poly/ML's interpreter, trying to understand the semantics of opcodes implemented in interpret.cpp. However, I have difficulty on understanding some of the opcodes: 1. INSTR_non_local, in its implementation Here what does this instruction do, and

Re: [polyml] Poly/ML build fails on Fedora 12

2010-05-27 Thread David Matthews
Rob, This seems to be something to do with selinux. Apparently the linker defaults to requiring an executable stack unless all the files that make up the module contain a special directive to say they don't require it. Output from g++ does contain the marker but the hand-coded assembly code

Re: [polyml] configure script problem on OS X

2010-06-06 Thread David Matthews
Philip Weaver wrote: Hello. I have noticed that the configure script fails if the CXX environment variable is set on OS X. The error message is (when CXX=/usr/bin/c++): checking for /usr/bin/c++... no configure: error: No C++ compiler found. Unable to build Poly/ML. This happens when CXX

Re: [polyml] Pretty printing singleton tuples

2010-06-14 Thread David Matthews
Thanks for pointing that out. I've fixed it in SVN and added a regression test. Note that picking up the fix requires rebuilding the compiler. Just a general warning to everyone that the format of exception handlers on X86 has changed and that in order to rebuild the compiler in SVN it's

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-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.

[polyml] Poly/ML 5.4

2010-08-12 Thread David Matthews
I'm planning to release Poly/ML 5.4 by the end of this month unless there are any show-stoppers. I've had a couple of bug reports from Phil Clayton and fixed those. I've also fixed a few minor bugs so that it will build on the PowerPC and Sparc. Now is the time to check that your software

Re: [polyml] Poly/ML 5.4

2010-08-14 Thread David Matthews
2010, at 16:36, David Matthews wrote: I'm planning to release Poly/ML 5.4 by the end of this month unless there are any show-stoppers. I've had a couple of bug reports from Phil Clayton and fixed those. I've also fixed a few minor bugs so that it will build on the PowerPC and Sparc. Now

Re: [polyml] Poly/ML 5.4

2010-08-19 Thread David Matthews
Matthew, Thanks for reporting that. I've installed a fix; well more of a work-around really and your example now compiles. I managed to reduce it a few lines which are now in the regression test suite. Regards, David Matthew Fluet wrote: David, Poly/ML 5.4 (SVN r1192) gives an

Re: [polyml] Poly/ML 5.4

2010-08-19 Thread David Matthews
Matthew, That looks suspiciously like the execute bit problem. Did you include -segprot POLY rwx rwx to the linker? See the last line of (the updated) http://www.polyml.org/FAQ.html#standalone David Matthew Fluet wrote: David, With that change, I was able to successfully compile MLton with

Re: [polyml] Poly/ML 5.4

2010-08-20 Thread David Matthews
Rob Arthan wrote: Matthew, That looks suspiciously like the execute bit problem. Did you include -segprot POLY rwx rwx to the linker? See the last line of (the updated) http://www.polyml.org/FAQ.html#standalone On that point, I recall having some problems caused by using cc rather than c++.

Re: [polyml] Poly/ML 5.4

2010-08-22 Thread David Matthews
Rob Arthan wrote: Thanks for the clarification. In fact, I didn't explain myself very well. What I meant was that as I have had problems of the sort linking Poly/ML programs because I used cc rather than c++, I thought it might be better to use c++ in the documentation throughout. I think it

Re: [polyml] Interfaces for printing IR and generated code

2010-08-22 Thread David Matthews
Yue Li wrote: I was trying to understand and document the semantics of the opcode set used by Poly/ML's interpreter, and I'm wondering whether inside Poly/ML's compiler, there are such debugging functions which could print out the IR tree as well as the generated op code for an input ML program?

Re: [polyml] Poly/ML 5.4

2010-08-23 Thread David Matthews
Thanks for reporting that. I've committed a fix and included your example as a regression test. David Makarius wrote: Here is another thing that looks like a regression from Poly/ML 5.3.0. datatype ('a, 'b) foo = Foo of 'a * 'b; val _ = PolyML.addPrettyPrinter (fn depth = fn (pretty1,

[polyml] Source code overview

2010-08-25 Thread David Matthews
Following a suggestion from Lucas I've gone through the Poly/ML source code and produced an overview that describes where each file fits into the overall structure. It still needs work both on the text and on the layout but at least it's a start. It's in the documentation directory in SVN as

Re: [polyml] PolyML memory parameters

2010-08-31 Thread David Matthews
Lucas, It looks as though these are a long way out of date. The Using Poly/ML document really needs to be completely updated. The current settings can be found from poly --help which shows: Compiler arguments: -v Print the version of Poly/ML and exit --help Print this

Re: [polyml] function for input from stdin

2010-09-01 Thread David Matthews
Johan, There's nothing wrong with the function or Poly/ML or SML/NJ's implementation. I think the difficulty you are having has to do with differences in way Poly/ML and SML/NJ handle their read-eval-print loops and the interaction between this and TextIO. From your previous message to me

Re: [polyml] Interfaces for printing IR and generated code

2010-09-02 Thread David Matthews
Dear Yue, You've obviously made quite a lot of progress. Yue Li wrote: 1. In the printed IR of a program, seems the print out has two sections, for example: 2 * 3; BLOCK(DECL #1{0 uses} = GLOBAL (FUN run_call2(1), LAMBDAINLINE( run_call2(1) CL=false CR=0 LEV=0 LOCALS=0

[polyml] Poly/ML 5.4 Released

2010-09-03 Thread David Matthews
I've uploaded version 5.4 to SourceForge and updated the web site. Thanks to everyone for your bug reports and comments. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Interfaces for printing IR and generated code

2010-09-03 Thread David Matthews
Yue Li wrote: Are signatures preserved only until type checking phase before the code generation phase? Any declaration will involve a name, a description of some sort and some code. The description might be the type of a value or in the case of a structure or signature a data-structure

Re: [polyml] Pretty-printing of infix constructors

2010-09-06 Thread David Matthews
Rob Arthan wrote: I have a small issue with the Poly/ML pretty-printer. If you run: datatype FOO = D of (int * int); infix D; 1 D 2; Poly/ML prints: val it = D (1, 2) : FOO Poly/ML will parse D(1, 2) but only because of a non-standard extension that lets you omit the keyword op that the

Re: [polyml] Names in initial top-level environment

2010-09-07 Thread David Matthews
Well spotted. I've cleaned them up and added a regression test for it. That's the most likely to be accidentally added. David Phil Clayton wrote: I've just noticed that the Poly/ML top-level initially has the names it unused bound to (). However unlikely, this could be accidentally

[polyml] Re: Questions on the code trees of functors

2010-09-14 Thread David Matthews
Yue Li wrote: functor myfctor(s: A) : B = struct type element = s.element end From above, I understand that functor is compiled to a lambda expression. But I don't quite see what the body of the lambda expression does. functor myfctor(s: A) : B = struct type element = s.element

Re: [polyml] St9bad_alloc with Memory Limits near 2^n GB

2010-09-16 Thread David Matthews
I haven't been able to reproduce this but I don't have a machine with that much memory. I suspect that what is happening is that poly is trying to allocate as much memory as possible for its own heap and not leaving anything spare for the C++ heap. This is something I'm planning to address

Re: [polyml] Low-level C FFI: call_sym or call_sym_and_convert?

2010-09-21 Thread David Matthews
On 19/09/2010 16:09, Phil Clayton wrote: I'm about to start generating code that makes calls to C via the low-level FFI. I was planning to use a form where parameters that provide return values are temporary vols created by alloc, as shown in the example SML code below (as suggested in the C

Re: [polyml] Polyml and binutils Gold (link failure)

2010-10-11 Thread David Matthews
On 10/10/2010 18:49, Basile Starynkevitch wrote: I just noticed (on Debian/Testing/AMD64) that with both polyml-5.4 latest SVN trunk (i.e. rev 1215) it is not possible to use binutils gold linker. error: polyexport.o: unsupported REL reloc section /usr/bin/ld: internal error in

Re: [polyml] St9bad_alloc with Memory Limits near 2^n GB

2010-10-25 Thread David Matthews
On 16/09/2010 12:52, Tjark Weber wrote: I'll be happy to test a fix/the next release on my machine when you have one. I've now had a chance to look at this and I've installed some experimental changes to SVN. I've added some handlers to the C++ new allocator so that it shouldn't crash if

Re: [polyml] Socket.accept on MacOS causes 100% processor usage

2011-01-12 Thread David Matthews
Hi Lucas, I've committed a fix to SVN head. The problem was that Mac OS X requires the time-out argument to the select system call to be properly formatted as micro-seconds and seconds whereas Linux seems to be more tolerant of the usec field being larger than a million. I seem to remember

Re: [polyml] exit code 89 with r1259

2011-01-17 Thread David Matthews
I'm actively working on the garbage collector so some commits may be buggy. It's probably better to avoid SVN just at the moment although the current commit (1264) should be better on X86/64 than 1259. More news when I have something more stable. David On 14/01/2011 09:25, Ramana Kumar

Re: [polyml] CInterface problem on SPARC/Solaris

2011-01-26 Thread David Matthews
Poly/ML 4.2.0 is very old now and I really wouldn't be surprised if something like this was broken. Try with version 5.4 and see if that works. I did remove support for older SparcStations at one point so it may be that you will have to use 5.3 or 5.2. You can find them all on the

[polyml] Re: On understanding Poly/ML function definition IR

2011-02-09 Thread David Matthews
On 08/02/2011 00:31, Yue Li wrote: I'm trying to get better understanding about the code tree of Poly/ML function definition. I would appreciate if I can gain some insights from you. For instance, given the following definition: fun f a b = a + b; The first point to appreciate is that this

Re: [polyml] Building MS Windows applications

2011-02-17 Thread David Matthews
I think I actually built that using Msys/Mingw. If you install them you can build from source exactly as you would on Unix or cygwin. There are other possibilities. There are project files for Visual C++ 6 which should work under newer versions of Visual C++. I think it's now possible to

Re: [polyml] InternalError: jump too large raised while compiling

2011-02-19 Thread David Matthews
On 18/02/2011 08:54, Andreas Lochbihler wrote: Dear all, I use Isabelle to generate ML code from my formalisation in Isabelle. When I try to load the output ML file in Poly/ML 5.4, I get the following exception: Exception- InternalError: jump too large raised while compiling Exception- Fail

Re: [polyml] Problem with Poly/ML on Cygwin on Vista

2011-02-19 Thread David Matthews
Is this related to Data Execution Prevention or perhaps some anti-virus checker? saveChild could well be copying some executable code and then returning into the copied version. The data segments are all created with execute permission but it's possible that something doesn't like this.

Re: [polyml] InternalError: jump too large raised while compiling

2011-02-21 Thread David Matthews
Thanks. That enabled me to see what was going wrong. I've committed a fix to SVN and the file compiles, at least as far as complaining about some missing declarations, on X86-32 and X86-64. You will need to run make compiler if you want to use the SVN version. Regards, David On 21/02/2011

[polyml] Re: Poly/ML codetree generation

2011-03-01 Thread David Matthews
On 28/02/2011 17:07, Yue Li wrote: On 02/28/2011 07:55 AM, David Matthews wrote: I've added a CodeTree sub-structure to the PolyML structure which makes the codetree available to ML programs. This just passes through the internal construction functions. To build a codetree you just call

Re: [polyml] Infinite loop when forcing GC after creating a weak pointer

2011-03-03 Thread David Matthews
Actually it was a deadlock but still it was a bug. Thanks for reporting it. I've fixed it in SVN head and I'll probably port the fix to the fixes branch. David On 03/03/2011 01:08, Ivan Tomac wrote: Entering this from the REPL appears to make Poly/ML go into an infinite loop: $ rlwrap

[polyml] Re: creating heterogeneous array in the Poly/ML codetree

2011-03-12 Thread David Matthews
This sounds like an ML tuple but tuples are always immutable i.e. the fields cannot be updated. In ML array is used for an updatable data-structure. Is that what you mean? By known size do you mean a size specified at compile-time? Are the index values always compile-time constants or can

Re: [polyml] Fwd: creating heterogeneous array in the Poly/ML codetree

2011-03-15 Thread David Matthews
On 15/03/2011 05:46, Lucas Dixon wrote: I'm not sure if this is what you meant, but the type of exceptions is heterogeneous in the sense that all exceptions, no matter what data they hold, have the same type. The query was really about the lower levels where the data structures are untyped

Re: [polyml] Memory leak? Poly/ML SVN 1307

2011-06-07 Thread David Matthews
Aleks, I have been doing quite a bit of work on the memory management. In most cases it should be a lot better but there's scope for some tuning. I'm planning to come back to that in due course. If you want a stable platform you should really stick with the last release rather than SVN.

Re: [polyml] Semantics of Threading Intrrupt Flags and proper interpretation in .Net simulation

2011-06-07 Thread David Matthews
Hi David, On 06/06/2011 23:48, Dave Thayer wrote: My questions are 1. What is the semantics of these flags as related to the behavior of threads and the Interrupt signal? Have you looked at http://www.polyml.org/docs/Threads.html ? There's an explanation there. If it's not clear

[polyml] IEEE reals

2011-06-16 Thread David Matthews
I've fixed a bug that Grant Passmore reported where the IEEEReal.setRoundingMode settings weren't working on X86. I've written a small regression test for this particular case but it would be nice to test Poly/ML's real numbers more completely. I'm not that familiar with real number

Re: [polyml] Repeated ascriptions

2011-06-28 Thread David Matthews
It's a while since I looked at this but I'm fairly sure that if you provide a signature that Poly/ML will recheck the structure against the signature. It may be possible to avoid this in specific situations but there are a lot of cases where things get complicated. For example, the signature

Re: [polyml] measuring/profiling memory consumption

2011-07-07 Thread David Matthews
I'm not sure I can suggest very much. The most likely cause is a change in Isabelle but it could be something to do with Poly/ML. PolyML.objSize PolyML.rootFunction will tell you the size of the data that is reachable from the root. It won't include any data that is only reachable from the

[polyml] Bug fixes and 5.4.1

2011-07-14 Thread David Matthews
There have been a few bugs fixed since the release of 5.4. I've now back-ported the fixes to the 5.4-fixes branch and updated the pre-built compilers for all the architectures. The two issues that seem to have caused particular problems are the divide instruction bug that caused an assertion

Re: [polyml] Order of evaluation of arguments to a function

2011-08-18 Thread David Matthews
On 18/08/2011 17:02, Alex Merry wrote: On 18/08/11 16:08, Ramana Kumar wrote: what about evaluating f? So the order of evaluation of (f x y) is f x (f x) y ((f x) y) This seems like a natural evaluation order for an eager functional language. I have always understood that the Definition of

Re: [polyml] Dud exception traces

2011-09-25 Thread David Matthews
PolyML.exception_trace only shows the functions that have separate pieces of code. Small functions are inlined by the compiler and won't show up. You can override this by setting PolyML.Compiler.maxInlineSize to something small e.g. zero. Alternatively, you can use the debugger to find the

Re: [polyml] Dud exception traces

2011-09-26 Thread David Matthews
of parameters? Either way, I managed to get ahold of the exact exception (with params) like this: exception foo; val exp = (use bug.ML; foo) handle e = e; PolyML.Debug.breakEx exp; use bug.ML; Very cool. On 25 September 2011 17:29, David Matthews david.matth...@prolingua.co.uk wrote

Re: [polyml] Fortify detects buffer overflow

2011-11-14 Thread David Matthews
I've attempted to reproduce this without success. I'm running Ubuntu 11.10 and had to install the hardening packages manually do there may be some difference. I can't tell much from the backtrace because the function names within the poly library aren't being shown. Could you try rebuilding

Re: [polyml] Null pointer and comparing CInterface.vol values

2011-11-15 Thread David Matthews
Phil, I think it could be possible to provide CInterface.null as a persistent vol pointing to a value containing (void*)0. I know that seems a contradiction but it should be possible. I'm just not sure it's necessary. Why do you need to have null and isNull? Have you considered instead

Re: [polyml] Resource consumption of the SVN version vs. 5.4.1

2011-11-16 Thread David Matthews
Andreas, How much real memory do you have on this machine? I would not expect that the size of the live data or the CPU time will have changed much, indeed I would have expected the CPU time to have reduced. There has, though, been a major change in the garbage-collector and in the way that

Re: [polyml] Null pointer and comparing CInterface.vol values

2011-11-16 Thread David Matthews
On 16/11/2011 15:17, Phil Clayton wrote: On 16/11/11 11:17, David Matthews wrote: On 16/11/2011 04:15, Ian Zimmerman wrote: Phil David, My situation is slightly unusual so perhaps it's Phil useful/interesting to explain some background. I'm working on Phil support for GLib/GTK in SML which

Re: [polyml] Null pointer and comparing CInterface.vol values

2011-11-16 Thread David Matthews
On 16/11/2011 17:15, Makarius wrote: On Wed, 16 Nov 2011, Rob Arthan wrote: On 16 Nov 2011, at 15:17, Phil Clayton wrote: I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that

Re: [polyml] Printing arbitrary objects

2011-11-16 Thread David Matthews
What do you mean by the structure? Just typing the value at the top-level will print a value which may be an arbitrary data structure. There's no standard way in ML to include general print function within a piece of code. There is the non-standard PolyML.print function to pretty-print a

Re: [polyml] Null pointer and comparing CInterface.vol values

2011-11-16 Thread David Matthews
On 16/11/2011 18:07, Phil Clayton wrote: The calling conventions for x86_64 appear to pass via registers not only the initial floating point arguments but also the initial int/pointer arguments: http://en.wikipedia.org/wiki/X86_calling_conventions So I suspect all arguments, not just floating

Re: [polyml] CInterface.setFinal pointer mismatch

2011-11-18 Thread David Matthews
Phil, Thanks for providing a compact example. I ran the test and found out what was happening. Essentially, if two pointers contained the same value but the finaliser was associated with the later entry in the vol table it was possible that the internal memory used to hold the pointer value

Re: [polyml] Null pointer and comparing CInterface.vol values

2011-11-18 Thread David Matthews
On 18/11/2011 13:49, Phil Clayton wrote: On 17/11/11 19:40, David Matthews wrote: Well, having decided that the existing code is horrible I bit the bullet and investigated libffi more closely. It turns out that it does everything we need including callbacks. I've now modified the foreign

Re: [polyml] Null pointer and comparing CInterface.vol values

2011-11-21 Thread David Matthews
On 18/11/2011 13:49, Phil Clayton wrote: With Fedora, there is a minor configuration issue: like many packages, libffi headers are not installed on a standard path, so relies on pkg-config to supply cflags/libs arguments. I was able to build by simply adding symbolic links in /usr/include. After

  1   2   3   4   5   >