Poly/ML

polyml@lists.polyml.org

2 participants
698 discussions

ULTRA type error slicer for SML: version 0.6 and TECHNICAL REPORT
by vincent.rahli＠gmail.com 19 Aug '10

19 Aug '10

We are happy to announce the release of two things: * Technical report HW-MACS-TR-0079 "A constraint system for a SML type error slicer" which explains how our type error slicing software works. * The new version 0.6 of our type error slicing software for the SML programming language. The abstract of the technical report is: Existing compilers for many languages have confusing type error messages. Type error slicing (TES) helps the programmer by isolating the part of a program contributing to a type error, but unfortunately TES was initially done for a tiny toy language. Extending TES to a full programming language is extremely challenging, and for SML we needed a number of innovations and generalisations. Some issues would be faced for any language, and some are SML-specific but representative of the complexity of language-specific issues likely to be faced for other languages. We solve both kinds of issues and present a simple, general constraint system for providing type error slices for ill-typed programs. Our constraint system elegantly and efficiently handles features like the intricate "open" SML feature. We show how the simple clarity of type error slices can demystify language features known to confuse users. We also provide in an appendix a case study on how to use TES to help modifying user data types, and extend the core language presented in the main body of this report to handle more of the implementation of our system. These extensions allow handling local declarations, type declarations and some uses of signatures. Regarding the software, major improvements over the previous release include: * The slicer is 10 to 100 times faster in many cases, and can reasonably be used on programs containing 10 thousand lines of code. * We support some uses of functors (that is, we report some type errors involving functors). * We report more kinds of errors and the error messages have been improved. * We provide a source archive (that is, a .tar.gz file which you unpack and run ?./configure; make; make install? in the unpacked directory). Other less important improvement is: * The slicer now quickly sends non-minimal error slices to the user interface and then sends a minimal replacement error slice after doing more time-consuming work. * We partially support fixity declarations in that we parse and type check programs using them correctly. Highlighting of infix declarations and identifiers in error slices is not yet correct. 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 source archive and new Ubuntu (Debian based) and Fedora (Red-Hat based) packages of our type error slicer can be found at this URL: http://www.macs.hw.ac.uk/ultra/compositional-analysis/type-error-slicing/ The technical report can be found at this URL: http://www.macs.hw.ac.uk:8080/techreps/view_record.jsp?id=0079 Known limitations: * We have not yet built the software for other operating systems than Linux. * The currently supported user interfaces are via a terminal window, GNU Emacs (or our web demo). We are currently developing a Vim interface. * 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 equality types and sharing constraints. * The details of the SML basis library are incomplete (fortunately the user can add any additional details they are using). Best wishes, Vincent Rahli and Joe Wells

1 0

Poly/ML 5.4
by David.Matthews＠prolingua.co.uk 14 Aug '10

14 Aug '10

There was an error in the default handler that is supposed to kill a thread that raises an uncaught exception. Now fixed. David Ramana Kumar wrote: > This code segfaults in 5.4 but runs fine in 5.3: > > open Thread Unix > val tail = ref (execute("/usr/bin/env",["sleep","0"])) > fun stopTail () = (kill(!tail,Posix.Signal.term); reap (!tail); ()) > fun restartTail () = (stopTail() handle OS.SysErr _ => ()) > val () = Thread.interrupt (Thread.fork(restartTail,[])) > > On Fri, Aug 13, 2010 at 1:36 AM, David Matthews > <David.Matthews(a)prolingua.co.uk> 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 is the time to check that your software will run >> in the current version and let me know if there are problems. Don't forget >> to run >> make compiler >> twice to build the current version (SVN 1189). >> >> David >> >> _______________________________________________ >> polyml mailing list >> polyml(a)inf.ed.ac.uk >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >>

1 0

Workshop on ML 2010 - Call for Participation
by matthew.fluet＠gmail.com 10 Aug '10

10 Aug '10

The 2010 ACM SIGPLAN Workshop on ML http://www.cs.rit.edu/~mtf/ml2010 Baltimore, Maryland, United States Sunday, September 26, 2010 co-located with ICFP 2010 Call for Participation ML is a family of programming languages that includes dialects known as Standard ML, Objective Caml, and F#. The development of these languages has inspired a large amount of computer science research, both practical and theoretical. This workshop aims to provide a forum to encourage discussion and research on ML and related technology (higher-order, typed, or strict languages). The format of the 2010 Workshop on ML will be different than that of recent years, returning to a more informal model: a workshop with presentations selected from submitted abstracts but without published proceedings. We hope that this format will encourage the presentation of more exciting (if unpolished) research and deliver a more lively workshop atmosphere. Invited Speaker ~~~~~~~~~~~~~~~ Luke Hoban (Microsoft) -- Bringing F# to Visual Studio 2010 Program ~~~~~~~ 9:00 Invited Talk Visual F#: Bringing F# to Visual Studio 2010 Luke Hoban (Microsoft Research) 10:00 Break 10:30 Probabilistic programming using first-class stores and first-class continuations Oleg Kiselyov (FNMOC); Chung-chieh Shan (Rutgers University) 10:55 Effective progamming in ML Daan Leijen (Microsoft Research); Ross Tate (University of California, San Diego) 11:20 Discussion 11:30 First-class modules and composable signatures in Objective Caml 3.12 Alain Frisch (LexiFi); Jacques Garrigue (Nagoya University Graduate School of Mathematics) 11:55 First-class modules: hidden power and tantalizing promises Jeremy Yallop (Applicative Ltd); Oleg Kiselyov (FNMOC) 12:20 Discussion 12:30 Lunch break 14:00 Deriving a Typed Implementation for Coroutines in ML Konrad Anton (Universitat Freiburg); Peter Thiemann (Universitat Freiburg) 14:25 The Design Rationale for Multi-MLton Suresh Jagannathan (Purdue University); Armand Navabi (Purdue University); KC Sivaramakrishnan (Purdue University); Lukasz Ziarek (Purdue University) 14:50 Discussion 15:00 Mirage: high-performance ML kernels in the cloud Anil Madhavapeddy (University of Cambridge); Thomas Gazagnaire (INRIA Sophia Antipolis) 15:25 Hosting a Standard ML compiler in a Web Browser: Status Report Martin Elsman 15:50 Discussion 16:00 Break 16:30 A simple and effective method for assigning blame for type errors David MacQueen (University of Chicago) 16:55 The MetaOCaml files: Status report and research proposal Oleg Kiselyov (FNMOC); Chung-chieh Shan (Rutgers University) 17:20 Discussion 17:30 Closing Registration and Local Arrangements ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * https://regmaster3.com/2010conf/ICFP10/register.php * http://www.icfpconference.org/icfp2010/local.html Program Chair ~~~~~~~~~~~~~ Matthew Fluet Rochester Institute of Technology Program Committee ~~~~~~~~~~~~~~~~~ Kathleen Fisher AT&T Labs Research Adam Granicz IntelliFactory Daan Leijen Microsoft Research Johan Nordlander Lulea University of Technology Sungwoo Park Pohang University of Science and Technology Daniel Spoonhower Google

1 0

Fwd: [isabelle] insufficient memory exception in polyml
by kleing＠cse.unsw.edu.au 27 Jul '10

27 Jul '10

This looks more like a polyml issue than an Isabelle issue, so I'm reposting here. Since the below I've run a few more experiments, and the theory does run fine with image built after less than 25min with the current svn trunk version of polyml on x86_64-darwin (5.4 Experimental). However, with the polyml-3.1-fixes version, it is still running after 45min with memory usage approaching 7.5GB and still raising. I'm not quite sure how to proceed. I don't think I'll want to run our production proofs on an experimental polyml version. How experimental/far away from release is the current trunk? Cheers, Gerwin Begin forwarded message: > From: Gerwin Klein <gerwin.klein(a)nicta.com.au> > Date: 23 July 2010 4:06:19 PM GMT+02:00 > To: Isabelle Users ML <cl-isabelle-users(a)lists.cam.ac.uk> > Subject: [isabelle] insufficient memory exception in polyml > > I am currently updating a very large theory from Isabelle2009-1 to Isabelle2009-2. So far this update was less painful than previous one, but I seem to be stuck now: > > I am getting various versions of insufficient memory exceptions from polyml-5.3 after the theory has been fully processed at the point (I presume) where polyml is writing the image to disk, possibly while it is doing garbage collection. > > A sample output of the log file is (the log file is btw gzipped and the error code is success, but the image is never written): > > lemma ... [last lemma of thy] > val it = () : unit > val it = () : unit > ML> Exception- Fail "Insufficient memory" raised > ML> > > The platform is polyml-5.3.0_x86-linux > with > ISABELLE_USEDIR_OPTIONS="-M 1 -p 0 -q 0 -v true" > and unchanged standard ML settings. > > The machine has 8G of RAM and otherwise works fine for other big developments. > > On polyml-5.3.0_x86-darwin, I am getting the same with the same settings. With -M 2, I am getting a C level exception in polyml at the same point with the message to set a breakpoint in a malloc function on stdour/err (but the same exception in the log). > > On polyml-5.3.0_x86_64-darwin, I am getting with -M 1 the same log, and this message on std out: > > Building CKERNEL ... > poly(5949,0xa0a3e500) malloc: *** mmap(size=134217728) failed (error code=12) > *** error: can't allocate region > *** set a breakpoint in malloc_error_break to debug > Finished CKERNEL (0:32:51 elapsed time, 0:32:47 cpu time, factor 0.99) > > (possibly the same as the 32bit version, but I've lost the previous output. Can reproduce if needed) > > With -M 3 and -M 2, on 64bit Darwin, I am instead getting exceptions about not being able to start another thread (at the same point). Again, the machine has 8GB of RAM and is otherwise rock solid. > > The same image builds easily under 32bit and 64bit polyml 5.3.0 (same version) on machines with less than 4GB of memory in Isabelle2009-1. > > Any ideas? > > I've tried playing around with -H and --mutable/--immutable settings, without success, but I don't have a good guideline what to try. > > Cheers, > Gerwin > > >

4 8

PASCO 2010: Programming Challenge
by Daniel.Cordeiro＠imag.fr 13 Jul '10

13 Jul '10

Matrix product over multi-precision integer and gcd computation http://pasco2010.imag.fr/contest.html 21st-23rd July 2010 PASCO 2010 Programming Challenge http://pasco2010.imag.fr/ Call for Participation ---------------------- Since the 80s and during the 90s a lot of parallel algorithms was proposed for computer algebra. Thus, 30 years after few computer algebra system are able to exploit modern parallel architectures multi-core, cluster and GPUs. The International Workshop on Parallel and Symbolic Computation (PASCO) is a series of workshops dedicated to the promotion and advancement of parallel algorithms and software in all areas of symbolic mathematical computation. The pervasive ubiquity of parallel architectures and memory hierarchy has led to the emergence of a new quest for parallel mathematical algorithms and software capable of exploiting the various levels of parallelism: from hardware acceleration technologies (multi-core and multi-processor system on chip, GPGPU, FPGA) to cluster and global computing platforms. To push up the limits of symbolic and algebraic computations, beyond the optimization of the application itself, the effective use of a large number of resources -- memory and general or specialized computing units -- is expected to enhance the performance multi-criteria objectives: time, energy consumption, resource usage, reliability. This year the PASCO 2010 workshop organize two programming challenges on ones of the most fundamental algorithms arising in computer algebra and providing rich opportunities for high performance computing. The two problems are matrix multiplication and gcd computations. Instances of the problems are given on the web site. The competition will take place live during the PASCO 2010 workshop. The results of the competition will be presented as part of the PASCO 2010 program. All participating teams will run their program on a selected set of the problems. The rule of the game is available on the PASCO 2010 workshop site [http://pasco2010.imag.fr/contest.html]. We strongly encourage all developers of parallel program or developers of parallel computer algebra system tools to participate in the competition. Teams are invited to send a declaration of participation as soon as possible by sending a mail to the PASCO 2010 conference organizers at pasco2010(a)imag.fr with the following information: * The name of the team and the contact information (name, email address, institution or company) of each team member willing to participate to the PASCO 2010 programming contest; * The name of the contact person (interlocutor and team representative). Accounts will be created on machine to allow teams to prepare their competition. Important dates --------------- Team declaration of participation: 19 July 2010 Preparation of the team: From 18 June until 20 July (remotely) Final preparation day: Wednesday 21 July 2010 at the Conference location Face to face challenge: Thursday 22 July 2010 Publication of the results during the Conference banquet.

1 0

Workshop on ML 2010 - Extended Submission Deadline
by matthew.fluet＠gmail.com 25 Jun '10

25 Jun '10

In response to requests, the submission deadline has been extended by one week until 2 July 2010. The 2010 ACM SIGPLAN Workshop on ML http://www.cs.rit.edu/~mtf/ml2010 Baltimore, Maryland, United States Sunday, September 26, 2010 co-located with ICFP 2010 Call for Content (Extended Deadline) ML is a family of programming languages that includes dialects known as Standard ML, Objective Caml, and F#. The development of these languages has inspired a large amount of computer science research, both practical and theoretical. This workshop aims to provide a forum to encourage discussion and research on ML and related technology (higher-order, typed, or strict languages). The format of the 2010 Workshop on ML will be different than that of recent years, returning to a more informal model: a workshop with presentations selected from submitted abstracts but without published proceedings. We hope that this format will encourage the presentation of more exciting (if unpolished) research and deliver a more lively workshop atmosphere. Invited Speaker ~~~~~~~~~~~~~~~ Luke Hoban (Microsoft) -- Bringing F# to Visual Studio 2010 Important Dates ~~~~~~~~~~~~~~~ Submission: 2 July, 2010 (extended) Notification: 9 August, 2010 Format ~~~~~~ The workshop will consist of presentations by the participants, selected from submitted abstracts. Participants are invited to submit working drafts, source code, and/or extended abstracts for distribution on the workshop homepage and to the attendees, but as the workshop will have no formal proceedings, any contributions may be submitted for publication to other venues. (See the SIGPLAN republication policy for more details.) Scope ~~~~~ We primarily seek research presentations on topics related to ML, including (but not limited to): * applications: case studies, experience reports, pearls, etc. * extensions: higher forms of polymorphism, generic programming, objects, concurrency, distribution and mobility, semi-structured data handling, etc. * type systems: inference, effects, overloading, modules, contracts, specifications and assertions, dynamic typing, error reporting, etc. * implementation: compilers, interpreters, type checkers, partial evaluators, runtime systems, garbage collectors, etc. * environments: libraries, tools, editors, debuggers, cross-language interoperability, functional data structures, etc. * semantics: operational, denotational, program equivalence, parametricity, mechanization, etc. Research presentations should describe new ideas, experimental results, significant advances in ML-related projects, or informed positions regarding proposals for next-generation ML-style languages. We especially encourage presentations that describe work in progress, that outline a future research agenda, or that encourage lively discussion. In addition to research presentations, we seek both Status Reports and Demos that emphasize the practical application of ML research and technology. Status Reports: Status reports are intended as a way of informing others in the ML community about the status of ML-related research or implementation projects, as well as communicating insights gained from such projects. Status reports need not present original research, but should deliver new information. In the abstract submission, describe the project and the specific technical content to be presented. Demos: Live demonstrations or tutorials are intended to show new developments, interesting prototypes, or work in progress, in the form of tools, libraries, or application software built on or related to ML technology. In the abstract submission (which need only be about half a page), describe the demo and its technical content, and be sure to include the demo's title, authors, collaborators, references, and acknowledgments. A demonstration should take 10-15 minutes. The exact time per demo will be decided based on the number of accepted submissions. (Please note that you will need to provide all the hardware and software required for your demo; the workshop organizers are only able provide a projector.) Submission Guidelines and Instructions ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Email submissions to mtf AT cs.rit.edu. Submissions should be at most two pages, in PDF format, and printable on US Letter or A4 sized paper. Persons for whom this poses a hardship should contact the program chair. Submissions longer than a half a page should include a paragraph synopsis suitable for inclusion in the workshop program. Program Chair ~~~~~~~~~~~~~ Matthew Fluet Rochester Institute of Technology Program Committee ~~~~~~~~~~~~~~~~~ Kathleen Fisher AT&T Labs Research Adam Granicz IntelliFactory Daan Leijen Microsoft Research Johan Nordlander Lulea University of Technology Sungwoo Park Pohang University of Science and Technology Daniel Spoonhower Google

1 0

Pretty printing singleton tuples
by phil.clayton＠lineone.net 14 Jun '10

14 Jun '10

I've just noticed that singleton tuples don't seem to be pretty printed as valid SML: Poly/ML 5.4 Experimental > {1 = true}; val it = (true): {1: bool} Presumably this should say: val it = {1 = true}: {1: bool} Phil

2 1

SML systems disagreeing on Date.localOffset
by Michael.Norrish＠nicta.com.au 10 Jun '10

10 Jun '10

My machine is Linux michaeln-desktop 2.6.31-22-generic #60-Ubuntu SMP Thu May 27 00:22:23 UTC 2010 i686 GNU/Linux Consider: print (Time.toString (Date.localOffset()) ^ "\n") poly (5.3) gives: ~36000.000 (-10 hours) Moscow ML (2.01) gives: 50400.000 (+14 hours) mlton (20070826) gives: 50400.000 sml/nj (v110.69) gives ~36000.000 Local time (Australian east coast in cold, cold winter) is 10 hours ahead of UTC. The Basis says: The offset from UTC for the local time zone. (Moscow ML's behaviour is consistent with its own documentation, but it doesn't pretend to implement Basis 2002.) It seems to me that the answer should actually be +10 hours, because that is what you add to UTC to get *from* UTC to my local time. Note that the Basis documentation for interpreting the offset field in the record passed to the Date.date function is a whole other story. (I don't know who/what to write to for SML/NJ.) Michael.

2 1

Date.fromTimeLocal off by a day
by Michael.Norrish＠nicta.com.au 09 Jun '10

09 Jun '10

On Linux: Linux michaeln-desktop 2.6.31-22-generic #60-Ubuntu SMP Thu May 27 00:22:23 UTC 2010 i686 GNU/Linux -- michaeln(~) date -R Wed, 09 Jun 2010 09:39:11 +1000 michaeln(~) poly Poly/ML 5.3 Release > Date.toString (Date.fromTimeLocal (Time.now())); val it = "Tue Jun 08 09:39:38 2010" : string > Date.toString (Date.fromTimeUniv (Time.now())); val it = "Tue Jun 08 23:41:21 2010" : string -- Michael

2 1

PASCO 2010: Call for Participation
by Daniel.Cordeiro＠imag.fr 07 Jun '10

07 Jun '10

------------------------------------------------------------------------ CALL FOR PARTICIPATION PASCO 2010 International Workshop on Parallel Symbolic Computation 2010 Grenoble University, INRIA and CNRS Grenoble, France, July 21-23, 2010 http://pasco2010.imag.fr/ ------------------------------------------------------------------------ The "2010 International Workshop on Parallel and Symbolic Computation" (PASCO) is the 4th meeting in a series of workshops dedicated to the promotion and advancement of parallel algorithms and software in all areas of symbolic mathematical computation. Following previous editions, PASCO 2010 will have presentations of accepted research papers and extended abstracts, invited talks, tutorial courses. Moreover, a programming contest will take place during the conference. * PASCO 2010 on-line registration is now available at http://pasco2010.imag.fr/ Early Registration (by June 30th) ACM/SIGSAM Members 190 EUR Non-ACM/SIGSAM Members 210 EUR Students 60 EUR Late and On-Site Registration ACM/SIGSAM Members 230 EUR Non-ACM/SIGSAM Members 250 EUR Students 90 EUR * Invited Lectures Christian Bertin (ST) & Claude-Pierre Jeannerod, (INRIA), France. Techniques and tools for implementing IEEE 754 floating-point arithmetic on VLIW integer processors. Erich L. Kaltofen , North Carolina State University, USA. 15 years after DSC and WLSS2: what parallel computations I do today. Stephen T. Lewin-Berlin, Quanta Research Cambridge, USA. Exploiting Multicore Systems with Cilk * Tutorials Jeremy Johnson , Drexel University, USA. Automatic Performance Tuning. Daniel Kunkle , Northeastern University, USA. Roomy: A System for Space Limited Computations. * Organization General co-Chairs: Marc Moreno-Maza, University of Western Ontario, Canada and Jean-Louis Roch, Grenoble University, France. Local Arrangement Chairs: Jean-Guillaume Dumas, Grenoble University, France and Thierry Gautier, INRIA, France and Clement Pernet, Grenoble University, France. Administration Chair: Daniele Herzog, INRIA France. Publicity Chair: Daniel Cordeiro, Grenoble University, France. ------------------------------------------------------------------------

1 0

← Newer
1
...
42
43
44
45
46
47
48
...
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