Poly/ML

polyml@lists.polyml.org

1 participants
698 discussions

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

Syntax of fun bindings and constructor application
by David.Matthews＠prolingua.co.uk 03 Jul '09

03 Jul '09

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 just like patterns. The effect of this, though, is that Poly/ML has allowed forms that are not strictly allowed by ML97. This is mainly in the use of parentheses, accepting them in some cases where they are not allowed and not requiring them where they should be used, but also allowing type constraints in some places where they are not allowed. I've now fixed this so that these extensions are no longer allowed but this may mean that programs that previously compiled no longer will. Examples of incorrect syntax previously accepted are: fun (f x) y = x+y; infix ++; fun SOME x ++ SOME y = x = y; val (SOME) x = SOME 1; I'm mentioning this because this could affect long standing code. I found an example of the second case, where an infixed function was applied to a construction that wasn't parenthesised, in the C-interface code of Poly/ML. David.

1 0

New Scintilla plugin for Standard ML
by robertr＠rftp.com 03 Jul '09

03 Jul '09

I mentioned here recently that I was working on updating my Scintilla plugin for OCaml to also support Standard ML - and it is now "done"(*). Since this coincided fortuitously (and barely) with the release cycle for Scintilla/SciTE 1.79, the new version has been included in the just-released editing package. If you go to http://www.scintilla.org and look for binaries, you will be pointed to http://www.scintilla.org/SciTEDownload.html. Here you can get compiled versions of the full Scintilla package (supporting a lot of programming languages) as part of either Windows or GTK+/Linux builds of the SciTE editor. One thing which might be missed were one to jump right in and start editing SML with the SciTE editor + the aforementioned OCaml/SML plugin (called a "lexer" in Scintilla parlance): only ONE language at a time can be automagically associated with a given source file extension (file type). So, as things come out of the box, OCaml has .ml and .mli files, while SML has .sml files. This may be adjusted two ways: by selecting a specific language from the SciTE Language menu, a default binding may be overridden. Or, by adjusting configuration files, SML can "take over" .ml file support for itself. These issues are discussed in the caml.properties config file in the main SciTE directory - note that you probably don't want to count on .ml and .ML being distinguishable. Perhaps I am missing something, but it looks like Poly is all about an interactive read-eval-print loop sort of dev environment, as opposed to [also] supporting a non-interactive edit-compile-run model... this makes the efforts underway to have a richer interactive experience even more understandable. ;) As I have already built OCaml bindings for Scintilla, creating SML bindings should be doable... but would this really be usable, given that Scintilla is Windows or GTK+, while Poly seems to be more Windows or X (including Motif here) oriented. Hmmm. I bring this up, because I think Scintilla can be useful as the "editing and output window" part of an IDE. (*) - actually, while "done" as much as software projects ever are, some suggestions for updating the 3 [arbitrary] groups of keywords would be welcomed (again, see the caml.properties config file). ;) Robert

2 2

Strange syntax in PolyML Code
by dathayer＠microsoft.com 30 Jun '09

30 Jun '09

I am working with the Isabell/HOL system which is hosted by default on the PolyML system. I have found a strange syntax construct in some of the source code files consisting of @{ ...some verbage ... } , examples below. I have searched the ML library pages and the PolyML docs looking for this syntactical construct and have been unable to find it. Does anyone know what this signifies? let metaSubst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)" by (unfold propDef)} [@{thm propDef}] Thanks David Thayer

3 3

Building on Vista x64 with VS 2008
by robertr＠rftp.com 26 Jun '09

26 Jun '09

I have recently downloaded the PolyML 5.2.1 archive and built it on my 4GB Vista x64 SP2 box, feeding the supplied Visual Studio workspace to my VS 2008 SP1 dev environment. This went quite well, with only 2 build errors and one execution problem stopping the entire bootstrapping process! :) The 2 errors are just from using the newer dev environment: the _osver variable is no longer available. So, the 2 usages (line 1434 in basicio.cpp and line 168 in process_env.cpp) need to change. As a minimal change, I would suggest if (_osver & 0x8000) => if (GetVersion() & 0x80000000) as something that will still work in older and newer environments. The execution issue happens early in the "Custom Build Step" use of PolyImport.exe: during startup, the polymain(...) function obtains the size of installed physical memory, and then defaults to using half of it. IMHO, this logic could use a new look, given modern system memory levels (4GB and up is becoming common, especially in today's dev environments)... in any case, the first actual call to VirtualAlloc is for something like 1.5 GB, and is failed. Since I was willing to believe that finding that much contiguous virtual address space could be hard - or maybe it was just that the demand to commit all of it too was the actual cause - I just forcibly cut the memory usage back to 256M and the rest of the build proceeded flawlessly, creating a functioning PolyML system. I built all 4 of the pre-defined targets - the only one that appeared seriously slow was the "IntDebug". ;) So, possibly adding some logic to (in the absence of command-line or other override) "cap" the default memory usage at 256 MB or 512 MB might be in order? Robert

3 10

Trac and CVS on SourceForge
by David.Matthews＠prolingua.co.uk 24 Jun '09

24 Jun '09

Having tried out Trac on SourceForge I've now disabled it. The problem is that SourceForge does not provide access to the configuration file necessary to add notification email addresses so it wouldn't be possible to know that a bug had been posted without checking the site. The SourceForge bug Tracker is still available and that does provide email notification. At the same time I've removed CVS since we're now using SVN. Regards, David.

1 0

PolyML Users
by ldixon＠inf.ed.ac.uk 03 Jun '09

03 Jun '09

Hello, I'm trying to find out what projects use, or can be built on PolyML, in order to write a grant application to improve PolyML and provide a continuous level of support for it. In particular, the grant would aim to provide better editing support (we have started working on this already), improvements to the module system (based on existing work by Andreas Rossberg and others), improvements to garbage collection for multi-threading programs, and perhaps improved compatibility with OCaml and Haskell (maybe based on the HLVM project). If you feel you would benefit from this, please do let me know. The more users of PolyML, the stronger our case. :) Many thanks, lucas

1 0

← Newer
1
...
49
50
51
52
53
54
55
...
70
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