Poly/ML

polyml@lists.polyml.org

2 participants
698 discussions

Release of version 0.4 of the ULTRA type error slicer for SML
by vincent.rahli＠gmail.com 14 Nov '09

14 Nov '09

We are happy to announce the release of the version 0.4 of our type error slicing software for the SML programming language. Major improvements over the previous release: * Overloaded operators can now be specified. * Special comments can now inform the type error slicer about identifiers in the top-level environment with their types/signatures. (This allows handling things like "use" and "CM.autoload" and working around the fact that we do not yet support "open".) * We provide a larger basis including more of the standard SML basis and some SML/NJ-specific declarations. * We fixed many cases where the Emacs interface failed silently. Other less important changes/improvements are: * We improved the error slices for record clashes. * We improved the pretty printing of error slices. * We improved the highlighting of white spaces. * We improved our error slice minimisation algorithm. * We improved the communication between our type error slicer and its Emacs interface. * We provide new error messages on status clashes (for example between an exception constructor and a datatype constructor). * Our test case database is much bigger, so there are fewer problems in general. * And we solved many bugs. Even more changes are documented in the ChangeLog file. The aim of our type error slicer is to provide useful type error reports for pieces of code written in SML: * It identifies all of the program points that contribute to a type error, including the spot with the actual programming error that caused the type error. * It highlights these program points in the original, unchanged source code. * It avoids showing internal details of the operation of the type inference machinery. A new compiled package of our type error slicer can be found at this URL: http://www2.macs.hw.ac.uk/~rahli/cgi-bin/slicer/downloads.html Known limitations: * We have not yet built the software for other operating systems than Linux. * The only currently supported user interface is via GNU Emacs (or our web demo). * Some features of the SML language are not parsed (the user will be notified if this is the case), and some type errors are not yet discovered (the user will need to rely on their usual type checker in these cases). Notable spots where the implementation is incomplete are functors (you can work around this by including signatures on functor applications), equality types, and fixity declarations. * We don't yet handle overloaded constants (for example 1 is always of type int). * The details of the SML basis library are incomplete (fortunately the user can add any additional details they are using). * The software does not currently scale well to very large programs (we are still improving this). It is currently suitable for small programs and use in teaching. * We have some known issues with context dependencies on long identifiers which yields wrong error reports. Best wishes, Vincent Rahli and Joe Wells

1 0

Re: profiling details
by schropp＠in.tum.de 12 Nov '09

12 Nov '09

> If profiling is turned on it is turned on for all threads. > Ok, I was suspecting something like that. Are there plans for profiling concurrent programs or even interactions of threads? > Profiling 2 records the number of words allocated in each function. It > works by pretending that the heap segment is full for each allocation so > forcing a call into the RTS. This adds a considerable overhead but does > produce accurate figures rather than samples. It measures the > allocation made and takes no account of whether or when the data > structures are garbage collected. Thanks for making that clear. > > Profiling 1 samples the program counter to find out where the code is > spending most of its time. It only really works properly in Linux. Mac > OS X does not have thread-specific CPU timers. In Linux a timer is set > for each thread which causes it to be interrupted every millisecond of > CPU time. One millisecond seems like a reasonable figure but you could > try changing it. You would have to modify > Processes::StartProfilingTimer in the RTS. Ok, maybe I'll try this. What happens if the thread is inside the RTS (but not engaged in GC, which is counted) when the timer goes off? Are those samples just ignored or do they count as UNKNOWN?

2 1

profiling details
by schropp＠in.tum.de 11 Nov '09

11 Nov '09

Hi, im an Isabelle Developer, wondering about the details of profiling 1&2: * what happens if another thread is executing while profiling is active for a selected thread (lets say by calling profile 1 f x in Isabelle)? In the resulting profile it looks to me like profiling doesnt know about threads and just accumulates all timings while active. Is this the same situation for profiling 1 and 2? * is it possible or even wise to reduce the distance of profiling 1"ticks" to achieve more accurate timings? * if a call gets "credit" for an allocation in a profiling 2 log, was the allocation done while profling 2 was active, or did it become garbage while profling 2 was active? Regards, Andy

2 1

Latest SVN version
by rda＠lemma-one.com 10 Nov '09

10 Nov '09

David, Rob Arthan wrote: > 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 for X >>>> windows and therefore not finding it. >>> I think any change here needs to wait for updates to autoconf. I'd >>> prefer not to put any special tests in myself. >> That's fine by me - I don't need the X bindings at the moment and I am sure > it >> would be easy to work around the problem if I did. > > Assuming that you have the Motif libraries installed as well as the > other X libraries you ought to be able to compile it in by giving the > appropriate paths: > ./configure --with-x --x-includes=/usr/X11R6/include \ > --x-libraries=/usr/X11R6/lib > > Don't forget configure no longer compiles in X-Windows by default. You > have to give the --with-x option explicitly. > 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" [ Motif.XmNlabelString "Hello World!" ]; I typically get the following error: Xlib: unexpected async reply (sequence 0x6c)! On one occasion it worked. but when I carry on and do: val _ = Motif.XtManageChild btn; val _ = Motif.XtRealizeWidget shell; nothing happens. The example program in the documentation has similar problems. I should say again that this is not a problem for me as I don't need to use the X or Motif interfaces at the moment. Regards, Rob.

2 1

Version 5.3 Release
by David.Matthews＠prolingua.co.uk 09 Nov '09

09 Nov '09

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 release. Thanks to Lucas and Makarius for their contributions and for organising support for me through the University of Edinburgh and TUM. Also thanks to everyone for comments and bug reports. Regards, David

1 0

Latest SVN version
by rda＠lemma-one.com 03 Nov '09

03 Nov '09

David, 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 for X windows and therefore not finding it. However while hamlet compiles and runs OK with poly compiled for the 32 bit architecture, it compiles but fails with a bus error with the 64 bit architecture. I believe I configured the Makefile correctly - I adjusted the settings for POLY_LIBDIR and added the appropriate -arch option to the step where it links the executable. I've appended the output from the dynamic linker and gdb: I am afraid I don't have a cutdown version of the problem, because there isn't really anything to cut down: it appears to be failing before calling the hamlet main function. Regards, Rob. rda]- DYLD_PRINT_LIBRARIES= hamlet dyld: loaded: /Users/rda/bld/hamlet-1.3.1/./hamlet dyld: loaded: /usr/local/poly/x86_64/lib/libpolyml.1.dylib dyld: loaded: /usr/lib/libstdc++.6.dylib dyld: loaded: /usr/lib/libSystem.B.dylib dyld: loaded: /usr/lib/system/libmathCommon.A.dylib Bus error rda]- gdb hamlet GNU gdb 6.3.50-20050815 (Apple version gdb-1344) (Fri Jul 3 01:19:56 UTC 2009) Copyright 2004 Free Software Foundation, Inc. GDB is free software, covered by the GNU General Public License, and you are welcome to change it and/or distribute copies of it under certain conditions. Type "show copying" to see the conditions. There is absolutely no warranty for GDB. Type "show warranty" for details. This GDB was configured as "x86_64-apple-darwin"...Reading symbols for shared libraries .... done (gdb) run Starting program: /Users/rda/bld/hamlet-1.3.1/hamlet Reading symbols for shared libraries +++. done Program received signal EXC_BAD_ACCESS, Could not access memory. Reason: KERN_PROTECTION_FAILURE at address: 0x00000001000060f0 [Switching to process 18897] 0x00000001000060f0 in PolyML.runFunction(1)(1) () (gdb) where #0 0x00000001000060f0 in PolyML.runFunction(1)(1) () #1 0x000000018298a968 in ?? () Previous frame inner to this frame (gdb could not unwind past this frame) (gdb)

2 3

Version 5.3 Release Candidate 2
by David.Matthews＠prolingua.co.uk 27 Oct '09

27 Oct '09

Thank you to everyone who reported bugs (or successes) in RC1. There have been quite a few fixes as a result and now everything that I'm aware of has been fixed. I have upped the version string to RC2 so this is the last chance to check that everything is working before the release. I've made new versions of the pre-built compilers in the imports directory and moved the version 5.3-specific basis library files into their normal locations. This means that it's sufficient to run ./configure make and it isn't necessary to run the "make compiler" step. If I don't hear anything in the next week or so I'll release 5.3. Regards, David

1 0

eqtype analysis bug in r902
by Michael.Norrish＠nicta.com.au 22 Oct '09

22 Oct '09

The attached causes the following error message, after doing a poly < simple.sml Poly/ML 5.3 Release candidate 1 > # # # ... # # Error-Type error in function application. Function: = : ''a * ''a -> bool Argument: (v, w) : ''a * hol_type Reason: Can't unify ''a to hol_type (Requires equality type) Found near exists_tyvar (fn v => v = w) ty Error-Type error in function application. Function: exists_tyvar : (hol_type -> bool) -> hol_type -> bool Argument: (fn v => v = w) : ''a -> bool Reason: Can't unify hol_type to ''a (Requires equality type) Found near exists_tyvar (fn v => v = w) ty Static Errors Poly 5.2 compiles the same code fine. r902 also compiles it fine if the (redundant, in this stripped down example) KTypes signature is removed, and the KTypes structure loses its signature ascription. mlton and Moscow ML also compile the code without complaint. Michael

2 1

Sparc support
by David.Matthews＠prolingua.co.uk 12 Oct '09

12 Oct '09

There's been a problem with the multiprocessor code in Poly/ML on the Sparc and I've traced this to some hand-coded assembly code. The problem is that v9 processors appear to require memory barrier instructions in the atomic increment and decrement instructions but these instructions aren't implemented on earlier processors. That really means that there have to be different versions of the code for v9 and for earlier processors. There are various options for dealing with this requiring more or less effort but I'd first like to have some idea of how much Sparc machines are currently used. If they are used are these v9 processors or are people still using v8/v7 processors? David

1 0

exception SysErr
by phil.clayton＠lineone.net 12 Oct '09

12 Oct '09

David, The basis library documentation for exception SysErr states: ...but if a SysErr exception has the form SysErr (s, SOME e), then we have errorMsg e = s. http://www.standardml.org/Basis/os.html However, it appears that Poly/ML is not always preserving that property because errorMsg e and s are sometimes different strings, for example: val () = ignore (TextIO.openIn "a non-existent file name") handle e as IO.Io {cause, ...} => ( case cause of OS.SysErr (s, SOME e) => ( print "\n"; app print ["s = \"", s, "\"\n"]; app print ["errorMsg e = \"", OS.errorMsg e, "\"\n"] ) | _ => () ); If the Standard is to be followed and one of the messages must be chosen, the string returned by errorMsg e seems to be the useful one as s can be deduced from the structure of the program, at least in this example. Regards, Phil

2 1

← Newer
1
...
46
47
48
49
50
51
52
...
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