- Haskell - Haskell.org

ANNOUNCE: graphviz-2999.1.0.2
by Ivan Lazar Miljenovic 25 Jul '09

25 Jul '09

This is a bug release that fixes a bug spotted by Srihari Ramanathan where the Dot representation of Color values were double-quoted when they shouldn't have been. -- Ivan Lazar Miljenovic Ivan.Miljenovic(a)gmail.com IvanMiljenovic.wordpress.com

1 0

Call for Papers: VSTTE 2009
by Jean-Christophe Filliâtre 24 Jul '09

24 Jul '09

We apologise if you receive this message more than once. ********************************************************* * * * VSTTE 2009 * * * * Workshop on Verified Software * * Theory Tools and Experiments * * * * (affiliated with Formal Methods Week) * * * * November 2, 2009 * * Eindhoven, the Netherlands * * http://vstte09.lri.fr/ * * * * Deadline for submissions: Sep 4, 2009 * * * ********************************************************* FM 2009 is the sixteenth in a series of symposia of the Formal Methods Europe association, and the second one that is organized as a world congress. Ten years after FM'99, the 1st World Congress, the formal methods communities from all over the world will once again have an opportunity to meet. FM 2009 will be both an opportunity to celebrate, and an opportunity to join in when enthusiastic researchers and practitioners from a diversity of backgrounds and schools come together to discuss their ideas and experiences. The workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2009) will take place on November the 2nd. The focus of this workshop will be on tools, as previous VSTTE conferences in Zurich and Toronto emphasised theories and experiments. Consisting of contributed papers and invited talks, the workshop will focus on the tools behind the development of systematic methods for specifying, building, and verifying high-quality software. This includes topics like: * Program logic * Specification and verification techniques * Tool support for specification languages * Tool for various design methodologies * Tool integration and plug-ins * Automation in formal verification * Tool comparisons and benchmark repositories * Combination of tools and techniques (e.g. formal vs. semiformal, software specification vs. engineering techniques) * Customizing tools for particular applications Papers about tool architectures, and their achievements are most welcome. The contributed papers, which should report on previously unpublished work, can reflect current and preliminary work in areas of software verification. New technical results, overviews of new developments in software verification projects, short papers accompanying tool demonstrations, as well as position papers on how to further advance the goal of verified software are all welcome. SUBMISSION PROCEDURE ==================== Submitted papers should not have been submitted elsewhere for publication, should use the Springer-Verlag's package ftp://ftp.springer.de/pub/tex/latex/svjour/sttt/, and should not exceed 15 pages including appendices. Papers will be processed through the EasyChair conference management system. IMPORTANT DATES =============== Submission deadline September 4, 2009, 11:59pm Samoa time (UTC-11) Notification of acceptance October 2, 2009 Final version October 16, 2009 CONTACT ======= Leo Freitas, leo(a)cs.york.ac.uk Department of Computer Science University of York, YO10 5DD York, UK Tel: (+44) (0) 1904 434753 Jean-Christophe Filliatre, Jean-Christophe.Filliatre(a)lri.fr CNRS / INRIA Saclay - Ile-de-france - ProVal Parc Orsay Universite, batiment N 4, rue Jacques Monod 91893 Orsay Cedex FRANCE Tel: (+33) (0)1 74 85 42 27 FURTHER INFORMATION =================== Further information will be put on the workshop web-page http://vstte09.lri.fr/.

1 0

ANN: darcs 2.3.0
by Petr Rockai 24 Jul '09

24 Jul '09

Hello! I'd like to announce immediate availability of a new stable release of darcs, 2.3.0. There is a number of improvements and bugfixes over the previous stable release, 2.2. Moreover, work has been done to improve performance of "darcs whatsnew" for large repositories. As in the past, there are two source tarballs available. As of this release, the cabal-based build is preferred, and the autoconf build is deprecated. You can obtain the source tarballs at these addresses: * http://repos.mornfall.net/darcs/darcs-2.3.0.tar.gz * http://repos.mornfall.net/darcs/darcs-2.3.0_autoconf.tar.gz The build instructions are available in the enclosed README file in those tarballs. Moreover, if you have cabal-install available, you can install latest stable release of darcs by issuing the following commands (no tarballs needed): $ cabal update $ cabal install darcs This should give you a darcs binary in `~/.cabal/bin` -- you should probably add this to your PATH. More detailed instructions for installing on Windows are available near the end of this announcement. What's New ---------- This is a summary of important changes since the last stable release (2.2): * Lots and lots of documentation changes (Trent). * Haskeline improvements (Judah). * Cabal as default buildsystem (many contributors). * Fixes in darcs check/repair memory usage (Bertram, David). * Performance improvement in subtree record (Reinier). * New option: --summary --xml (Florian Gilcher). * New option: changes --max-count (Eric and Petr). * Fix changes --only-to-files for renames (Dmitry). * Performance fix in "darcs changes" (Benedikt). * Hardlinks on NTFS (Salvatore). * Coalesce more changes when creating rollbacks (David). * New unit test runner (Reinier). * Inclusion of darcs-shell in contrib (László, Trent). * Author name/address canonisation: .authorspellings (Simon). * Working directory index and substantial "darcs wh" optimisation (Petr). * New command: "darcs show index" (Petr). * Gzip CRC check and repair feature (Ganesh). A number of issues has been resolved since 2.2 as well. See http://bugs.darcs.net/issueN for details on bug number N. * 948 darcsman (Trent) * 1206 countable nouns (Trent) * 1285 cabal test v. cabal clean (Trent) * 1302 use resolved, not resolved-in-unstable (Trent) * 1235 obliterate --summary (Rob) * 1270 no MOTD for --xml-output (Lele) * 1311 cover more timezones (Dave) * 1292 re-encoding haskeline input (Judah) * 1313 clickable ToC and refs in PDF manual Trent) * 1310 create merged \darcsCommand{add} (Trent) * 1333 better "cannot push to current repository" warning (Petr) * 1347 (autoconf) check for unsafeMMapFile if mmap use enabled (Dave) * 1361 specify required includes for curl in cabal file (Reinier) * 1379 remove libwww support (Trent) * 1366 remove unreachable code for direct ncurses use (Trent) * 1271 do not install two copies of darcs.pdf (Trent) * 1358 encode non-ASCII characters in mail headers (Reinier) * 1393 swap "darcs mv" and "darcs move" (Trent) * 1405 improve discoverability of global author file (Trent) * 1402 don't "phone home" about bugs (Trent) * 1301 remove obsolete zsh completion scripts (Trent) * 1162 makeAbsolute is now a total function (Ben F) * 1269 setpref predist - exitcode ignored bug (Ben M) * 1415 --edit-long-comment, not --edit-description, in help (Trent) * 1413 remove duplicate documentation (Trent) * 1423 complain about empty add/remove (Trent) * 1437 Implement darcs changes --max-count (Eric) * 1430 lazy pattern matching in (-:-) from Changes command module (Dmitry) * 1434 refactor example test (Trent) * 1432 refer to %APPDATA%, not %USERPROFILE% (Trent) * 1186 give a chance to abort if user did not edit description file (Dmitry) * 1446 make amend-record -m foo replace only the patch name (Dmitry) * 1435 default to get --hashed from a darcs-1.0 source (Trent) * 1312 update and reduce build notes (Trent) * 1351 fix repository path handling on Windows (Salvatore) * 1173 support hard links on NTFS (Salvatore) * 1248 support compressed inventories for darcs-1 repos (Ganesh) * 1455 implement "darcs help environment" (Trent) The question of GHC 6.8 ----------------------- Using GHC 6.10.3 or newer is *strongly recommended*. You may compile darcs with GHC 6.8, but there are several caveats. If you are using 6.8.2 or older, please disable mmap support (pass -f-mmap to cabal install or runghc Setup configure). Note that the GHC 6.8.2 that ships with Debian Lenny is not affected and it should be safe to keep mmap enabled. It is also recommended to disable use of Hackage zlib when compiling with GHC 6.8.2 (including the Debian Lenny version): pass -f-zlib to cabal. When using zlib, we have seen occasional crashes with error messages like "openBinaryFile: file locked" -- this is a known GHC 6.8.2 bug (and is fixed in GHC 6.8.3). Last, if you are using a 64-bit system, darcs may hang when you exit a pager when compiled with GHC older than 6.10.3. Although this is harmless, it is quite inconvenient. Overall, the status of GHC 6.8 is "semi-supported": for many cases, things will work just fine, especially if you take a little extra caution with compilation flags. Installing on Windows --------------------- To install darcs on Windows systems from scratch, please download the Haskell Platform and MSYS: * http://hackage.haskell.org/platform/2009.2.0.1/HaskellPlatform-2009.2.0.1-s… * http://sourceforge.net/projects/mingw/files/MSYS+Base+System/MSYS-1.0.11-rc… After installing both, you should have an "MSYS" icon: run MSYS and in the terminal window type (the `$` character denotes the prompt, do not repeat it): $ cabal update $ cabal install darcs -f-curl This should download, compile and install all required dependencies and also darcs itself. The resulting darcs executable will be placed into the Haskell Platform executables folder, and should be accessible from the MSYS shell (just type "darcs --version" to check). Yours, Petr.

2 1

ANN: yices 0.0.0.1 - Haskell programming interface to Yices SMT solver
by Ahn, Ki Yung 24 Jul '09

24 Jul '09

http://hackage.haskell.org/package/yices Incomplete (no bitvectors) syntax, parser, and inter process communication to Yices from Haskell through pipe. Purpose for building and using this library was to generate test cases from constraints that SMT solvers can solve. I only used it for that particular purpose, so the code in general is not yet fully tested. Use at your own risk and error reports are welcomed. See http://yices.csl.sri.com/ for further information on Yices. Note: this package does not include Yices. You should get it from the Yices homepage and install it before using this library. @ If you already have a better API for Yices or other SMT solvers, and if you can open the source please upload it to hacakage. That would be great help for some people. -- Ahn, Ki Yung

1 0

ANNOUNCE: generator 0.5.1
by Yair Chuchem 23 Jul '09

23 Jul '09

A new "generator" package has been uploaded to Hackage. It implements an alternative list monad transformer, a list class, and related functions. The difference from mtl/transformers's ListT is that mtl is a monadic action that returns a list: newtype ListT m a = ListT { runListT :: m [a] } generator's is a monadic list: data ListItem l a = Nil | Cons { headL :: a, tailL :: l a } newtype ListT m a = ListT { runListT :: m (ListItem (ListT m) a) } A short example program which reads numbers from the user and interactively sums them up: import Control.Monad.ListT (ListT) import Data.List.Class (execute, joinM, repeat, scanl, takeWhile) import Prelude hiding (repeat, scanl, takeWhile) main = execute . joinM . fmap print . scanl (+) 0 . fmap (fst . head) . takeWhile (not . null) . fmap reads . joinM $ (repeat getLine :: ListT IO (IO String)) I also wrote an example/blog-post about using ListT to add an undo option to the classic game of "hamurabi": http://mashebali.blogspot.com/2009/07/charlemagne-disraeli-and-jefferson.ht… Another interesting observation is that "ListT [] a" is a tree of "a"s. The module Data.List.Tree includes functions to prune and search such trees (dfs, bfs, bestFirstSearchOn, etc). This can be useful for modularizing code that uses the list monad for combinatoric search by decoupling tree creation from processing and pruning.

5 7

ANNOUNCE: ALUT 2.2.0.0
by Sven Panne 23 Jul '09

23 Jul '09

A new version of the ALUT package has been uploaded to Hackage. It is functionally equivalent to the previous version, but the dependency on the OpenGL package has been removed. Instead, the highly portable StateVar package is used, decoupling things a bit more. Cheers, S.

1 0

ANNOUNCE: OpenAL 1.4.0.0
by Sven Panne 23 Jul '09

23 Jul '09

A new version of the OpenAL package has been uploaded to Hackage. It is functionally equivalent to the previous version, but the dependency on the OpenGL package has been removed. Instead, the highly portable StateVar, ObjectName and Tensor package are used, decoupling things a bit more. Cheers, S.

1 0

ANNOUNCE: Tensor 1.0.0.1
by Sven Panne 23 Jul '09

23 Jul '09

A new Tensor package has been uploaded to Hackage. It is yet another spin-off of the OpenGL package, containing a few tensor data types and their instances for some basic type classes. Currently the word "tensor" might be a bit too much, but it is planned to add matrices, too. Note that this package deliberately does *not* contain new type classes or some elaborate tensor operations. After some discussion it was clear that the design space is too large and there a various ways to add these features, with varying goals in the design, none "more correct" or canonical than the other. Cheers, S.

1 0

Call for Papers: PLPV 2010
by Jean-Christophe Filliâtre 22 Jul '09

22 Jul '09

Call For Papers Programming Languages meets Program Verification (PLPV) 2010 http://slang.soe.ucsc.edu/plpv10/ Tuesday, January 19, 2010 Madrid, Spain Affiliated with POPL 2010 Overview: The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic and/or structural properties of the programming language. One example is dependently typed programming languages, which leverage a language's type system to specify and check richer than usual specifications, possibly with programmer-provided proof terms. Another example is extended static checking systems like Spec#, which extends C# with pre- and postconditions along with a static verifier for these contracts. We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. To encourage cross-pollination between different communities, we seek a broad the scope for PLPV. In particular, submissions may have diverse foundations for verification (type-based, Hoare-logic-based, etc), target diverse kinds of programming languages (functional, imperative, object-oriented, etc), and apply to diverse kinds of program properties (data structure invariants, security properties, temporal protocols, etc). Submissions: Submissions should fall into one of the following three categories: 1. Regular research papers that describe new work on the above or related topics. Submissions in this category have an upper limit of 12 pages, but shorter submissions are also encouraged. 2. Work-in-progress reports should describe new work that is ongoing and may not be fully completed or evaluated. Submissions in this category should be at most 6 pages in total length. 3. Proposals for challenge problems which the author believes is are useful benchmarks or important domains for language-based program verification techniques. Submissions in this category should be at most 6 pages in total length. Submissions should be prepared with SIGPLAN two-column conference format. Submitted papers must adhere to the SIGPLAN republication policy. Concurrent submissions to other workshops, conferences, journals, or similar forums of publication are not allowed. Publication: Accepted papers will be published by the ACM and appear in the ACM digital library. Student Attendees: Students with accepted papers or posters are encouraged to apply for a SIGPLAN PAC grant that will help to cover travel expenses to PLPV. Details on the PAC program and the application can be found on the workshop web page. PAC also offers support for companion travel. Important Dates: * Electronic submission: October 8, 2009, 11:59pm Samoa time (UTC-11) * Notification: November 8, 2009 * Final version: November 17, 2009 * Workshop: January 19, 2010 Organizers: * Cormac Flanagan (University of California, Santa Cruz) * Jean-Christophe Filliâtre (CNRS) Program Committee: * Adam Chlipala (Harvard University) * Ranjit Jhala (University of California, San Diego) * Joseph Kiniry (University College Dublin) * Rustan Leino (Microsoft Research) * Xavier Leroy (INRIA Paris-Rocquencourt) * Conor McBride (University of Strathclyde) * Andrey Rybalchenko (Max Planck Institute for Software Systems) * Tim Sheard (Portland State University) * Stephanie Weirich (University of Pennsylvania)

1 0

ANNOUNCE: uacpid-0.0.4
by Dino Morelli 22 Jul '09

22 Jul '09

Announcing uacpid-0.0.4 uacpid is a daemon designed to be run in userspace that will monitor the local system's acpid socket for hardware events. These events can then be acted upon by handlers with access to the user's environment. An example of why you need this: Suppose you want to have a hardware event change the active X displays, like a laptop external monitor function button. Some tools to achieve this display change require the logged in user's DISPLAY and other settings that may be difficult or impossible to gain access to from acpid scripts. Another example is media control function buttons, like play/pause or next/previous track for a music player. uacpid is running as you and is getting the hardware events reported by the system's acpid. uacpid can then act on the events on your behalf, with your environment. Available from Hackage, Arch Linux's AUR, darcs, see the homepage: http://ui3.info/d/proj/uacpid.html -- Dino Morelli email: dino(a)ui3.info web: http://ui3.info/d/ irc: dino- pubkey: http://ui3.info/d/dino-4AA4F02D-pub.gpg

1 0