PolyML version 4.1.3 is now available. Below are a list of the major
changes and bug fixes since the 4.1.2 release taken from the release
notes. Version 4.1.3 has been available unofficially for a while but
the release on the web site is now complete and this incorporates a few
bug fixes which were only found during testing.
As usual I welcome comments and bug reports and I'll try to respond
fairly quickly but the response will depend on pressure of other work.
David
New features and Changes
Printing control switches
New switches have been added to the Poly/ML.Compiler structure to
control the printing of declarations. In both cases the default setting
is true. Setting PolyML.Compiler.printInAlphabeticalOrder causes
declarations to be printed in the order in which they were made rather
than in alphabetical order. Setting
PolyML.Compiler.printTypesWithStructureName to false causes types to be
printed without the structure from which they came.
Large database support
The support for large databases has been improved and it is now
possible to create a database which will occupy all of the virtual
memory reserved for it. The actual limits vary between operating
systems and platforms but are typically around 400Mbytes.
To aid this the -S option when running the disc garbage-collector (-d
option), introduced in 4.1.1, has been extended with -Smin and -Smax.
The options can be written using either -s or -S and with or without a
space. Setting a size is now "sticky" so if no -s/-S option is given
the previous limits are retained rather than being reset to the
default. The -Smax option sets the limits to the maximum space
available. This space now depends only on the size reserved for any
parent databases and not, as before, on the history of the database.
The -Smin option compacts the database into a size whose upper limit is
set to the size actually in use before compaction. To make best use of
it it is probably best to run it twice, once to compact the database
and again to set the upper limits to the now reduced size. It is useful
when a database has been created which will not be modified further but
where child databases may be created. Compacting a database to the
minimum size allows any child databases to occupy as much space as
possible.
The disc garbage collection has been changed so that it is now possible
to use all the address space. Previously it was always necessary to
reserve a certain portion of the space to allow the database to be
collected.
Bugs fixed
Mac OS X 10.2
Mac OS X 10.2 introduced a undocumented change to the kernel interface
when delivering signals. This meant that the original binaries will not
run on 10.2. This has now been fixed.
Crash on delivering console interrupt on PowerPC
There was a bug in the Poly/ML process (lightweight thread) code on the
PowerPC which caused a crash when a process terminated. This could
happen when a user-installed signal handler was called, for example the
console interrupt handler in Isabelle.
Crash in equality code
An error in the compilation of the equality function meant that certain
expressions involving equality could cause a crash. This has been fixed.
