Poly/ML

polyml@lists.polyml.org

704 discussions

Pretty-printer seems to loop
by rda＠lemma-one.com 31 Aug '09

31 Aug '09

David, I have a problem building ProofPower with the latest Poly/ML. The build goes into a loop at a point where it opens a certain structure. This will be the first time Poly/ML has had to pretty-print a value of the type THM that represents theorems. This type has a circularity passing through a ref and a certain dictionary data type. I have attached a very cutdown version of the failing code. The cutdown version behaves slightly differently in that I see some never-ending output, while the ProofPower build just goes into a silent busy hang. The dictionary type OE_DICT that causes the problem is an amalgam of two simpler dictionary data types S_DICT (simple dictionaries using an association list) and E_DICT (efficient dictionaries using a hash key and a binary tree). Somewhat oddly the problem doesn't happen if I replace OE_DICT with either S_DICT or E_DICT even though the representation type for OE_DICT is just S_DICT * E_DICT. If it is just that the latest source in SVN is just not in a stable state, let me know and I will give up until further notice. I also noted in passing that types declared as abstypes are now equality types. Was this a conscious attempt to implement one of the Successor ML proposals? Regards, Rob.

2 1

Detecting unreferenced identifiers
by David.Matthews＠prolingua.co.uk 31 Aug '09

31 Aug '09

I fixed a bug recently [831] where I'd reorganised some code and the wrong identifier was being picked up. It would have been immediately apparent if the compiler had detected that an identifier was unreferenced so I've now added that check. In the current SVN version identifier checking is off by default but can be turned on with PolyML.Compiler.reportUnreferencedIds := true; The compiler will then report identifiers that are unreferenced as a warning. Currently, this applies only to value identifiers, excluding value constructors. An identifier is referenced if it used anywhere, which includes a recursive use, exported as a top-level value or used in the result of a structure or functor. When used in a structure or functor an identifier must be mentioned in the signature to be considered as referenced. Reference information isn't currently available through the IDE protocol but that can be added. Enabling unreferenced identifier checking on the compiler itself showed up a minor bug so it's already proved useful. David

2 3

Re: PolyML application news
by ldixon＠inf.ed.ac.uk 27 Aug '09

27 Aug '09

Hello, Unfortunately, as some people suspected, the PolyML application was deemed to be out of scope and so it was not taken forward for funding. However, I did get positive feedback and we were recommended to resubmit the application to another funding stream. So I am now thinking about adapting the previous proposal, adding a bit more of a research angle. I had a few discussions already, e.g. adapting the idea of equality type to a more general notion of type classes (from Larry, I think). Do email me your ML-grumbles and thoughts: I'll be bouncing various ideas around at the ML-workshop in the forthcoming ICFP conference. The old (so far unfunded) application can be found here: http://dream.inf.ed.ac.uk/projects/polyml/appl.pdf best, lucas Lucas Dixon wrote: > Hi, > > Quickly following the second draft, I've done a good deal more polishing > up of the proposal, and this is probably close to the final version. > > Thanks very much for all the feedback! > > Many thanks, > lucas

1 0

Poly/ML build fails on cygwin
by rda＠lemma-one.com 27 Aug '09

27 Aug '09

I can't build version 5.2.1 of polyml on cygwin. THe make step fails like this: .... gcc -Wall -fno-strict-aliasing -O3 -o .libs/polyimport.exe polyimport.o libpolyml/.libs/libpolyml.dll.a -lgdi32 -lwsock32 -lpthread -ldl -lstdc++ -lgcc -L/usr/local/lib creating polyimport.exe cp imports/polymli386.txt polytemp.txt ./polyimport -H 10 polytemp.txt < exportPoly.sml > /dev/null make[2]: *** [polyexport.o] Error 53 make[2]: Leaving directory `/cygdrive/c/Documents and Settings/rob.arthan/My Documents/2-Misc/Downloads/polyml/polyml.5.2.1' make[1]: *** [all-recursive] Error 1 make[1]: Leaving directory `/cygdrive/c/Documents and Settings/rob.arthan/My Documents/2-Misc/Downloads/polyml/polyml.5.2.1' make: *** [all] Error 2 I can't crack my way through the various shell scripts, C programs and bits of ML that are involved here, so I can't tell where the error number 53 comes from. (If it is a Unix errno value, then it is the very weird "ENOANO: No anode"). Any suggestions gratefully received, Rob.

2 4

Out of memory when saving state
by pclayton＠taz.qinetiq.com 17 Aug '09

17 Aug '09

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 rootFunction returns Timing - parse:0.0, semantics:0.0, translate:0.0, generate:0.0, run:63.4 val it = 218901122 : int which is considerably larger than the 1382064 that is returned in a fresh poly session. It is my understanding that the upper limit on the size of a state is determined by the resources available on a machine. Before looking into a 64 bit OS with more addressable memory etc. I wondered if it is possible to tell from the above values whether I am just trying to save something infeasibly large? Thanks again, Phil The information contained in this E-Mail and any subsequent correspondence is private and is intended solely for the intended recipient(s). The information in this communication may be confidential and/or legally privileged. Nothing in this e-mail is intended to conclude a contract on behalf of QinetiQ or make QinetiQ subject to any other legally binding commitments, unless the e-mail contains an express statement to the contrary or incorporates a formal Purchase Order. For those other than the recipient any disclosure, copying, distribution, or any action taken or omitted to be taken in reliance on such information is prohibited and may be unlawful. Emails and other electronic communication with QinetiQ may be monitored and recorded for business purposes including security, audit and archival purposes. Any response to this email indicates consent to this. Telephone calls to QinetiQ may be monitored or recorded for quality control, security and other business purposes. QinetiQ Limited Registered in England & Wales: Company Number:3796233 Registered office: 85 Buckingham Gate, London SW1E 6PD, United Kingdom Trading address: Cody Technology Park, Cody Building, Ively Road, Farnborough, Hampshire, GU14 0LX, United Kingdom http://www.qinetiq.com/home/notices/legal.html

2 2

FFI and C++?
by robertr＠rftp.com 05 Aug '09

05 Aug '09

Hi, Is there an update in the works for the Poly FFI? I may not be looking in the correct place, but I am seeing what may be a needed feature: let's say I am happy with Poly managing the lifetimes of "volatile" C-data values, and handling the freeing of malloced memory. What about C++? One would need some way to [at least] arrange for a delete operation (so as to invoke any needed destructor(s))... and this is assuming we wrap C++ objects created with new[] inside a "simple" new-created object - otherwise we need to be able to issue a delete[]. This could still potentially be handled by a C-style interface, if we could optionally associate a C "finalize" function with a volatile - this function could be called by the Poly memory reclamation when the volatile is truly unreachable; upon its return, Poly can go ahead and complete the free operation. This issue comes up both in the general case of talking to extra-Poly code (where we may have some control of the interface presented), but also in the case of talking to an existing library that is C++ rather than C based... in this case, we really need to allow the foreign code base to perform its own lifetime-management related operations. Like I said, this functionality may be available already... but if isn't, what are others' thoughts on the subject? Is this facility needed? Robert

2 13

Re: Segmentation fault
by David.Matthews＠prolingua.co.uk 05 Aug '09

05 Aug '09

Phil, I'm copying this to the list since it may affect other people and in fact I think I may have discussed this with Makarius in the past. The issue was a unexplained segfault which turned out to be caused by the GC running out of stack space. Fundamentally, the problem is that the marking phase of the GC uses a recursive algorithm which can recurse as deep as the data structure being marked. It does a good job of avoiding recursion if there is only one pointer in an object but that doesn't always avoid the problem. The solution, I think, would be to use a bounded queue along with a second bitmap to record when objects need to be rescanned. This will probably have to wait until at least the next release and might be best tackled along with parallelising the garbage collector. As far as I know there's no way to know that the stack is about to run out and provide some more helpful error message. Regards, David Philip Clayton wrote: > Good news! "ulimit -s unlimited" solves this. By default it was set to > 10240 (I believe that is kB). That is useful to know about. > > In case you are wondering, this GC recursion was happening during the > lexing of a block of text that was several MB, I think approx 4-5 MB. I > would imagine that the particular reader/lexer (part of ProofPower/DAZ) > was just building up a very deep structure. > > Thanks, > Phil > > > David Matthews wrote: >> Phil, >> It looks to me as though there is some very deep data structure and >> that the GC is running out of stack space. It is also possible that >> there's a bug and the GC is in a recursive loop. >> >> What is your stack limit set to? Try "ulimit -s" under bash. Try >> removing the limit with "ulimit -s unlimited". >> >> I have a feeling that there was a change that meant that when marking >> a data structure the GC now involves some extra function calls and so >> may require more stack space than it did.

1 0

Deferred signature copying
by David.Matthews＠prolingua.co.uk 04 Aug '09

04 Aug '09

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 completely copied so that the types used in the values were distinct from those in any other use of the signature. I've now changed this so that the signatures are now carried around in their original forms and the type information is carried in a map that only gets applied as late as possible. The effect of this change is that the memory required for a named signature is allocated once and that using it, either to name a sub-structure in another signature, or as an explicit signature constraint for a structure or functor, incurs only a small additional overhead. Whether it makes any difference to your code will depend on the extent to which you reuse signatures. It does seem to make a difference to the size of the compiler although other changes have rather swamped it. An extreme example was Lucas' Quantomatic which reduced in size from 150Mbytes to 13Mbytes! David.

1 0

Performance problems with saving and loading state
by David.Matthews＠prolingua.co.uk 29 Jul '09

29 Jul '09

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 solved this problem without the difficulty of overestimating the size that I was trying to avoid. With the experimental IDE we build up very long chains of saved states, with the Poly/ML compiler which is a comparatively small project the chain is over 90 long, so overestimating the size can result in running out of memory. David

2 1

Performance problems with saving and loading state
by rda＠lemma-one.com 27 Jul '09

27 Jul '09

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, it now takes nearly 40 minutes to load a state (occupying about 150Mb on disc) that previously took about 20 seconds. Unfortunately, my attempts to create simple examples of this type problem do not exhibit much difference between 5.2.1 and the latest sources. I wondered if anyone else has had similar problems or has any suggestions about how to isolate the problem. I believe the problem is quite old. It apparently predates the move from CVS to SVN. Regards, Rob.

2 3

← Newer
1
...
49
50
51
52
53
54
55
...
71
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML