Version 1.1.0
=============
svn.uri=:"http//common-lisp.net/project/armedbear/svn/trunk/abcl/"
(22 November 2012)
Features
--------
* A functioning (A)MOP implementation through the hard work of Rudi
Schlatte (@rudi)
* The implementation can be used across many more Quicklisp systems
through a process of extensive testing. Thanks @xach!
Nota bene: all of the following systems need patches to work as
of the 2012-10-13 Quicklisp. All patches have been accepted in
at least an initial form by the upstream maintainers.
** CLOSER-MOP
Quite possible with local patches
** CFFI
Needs patches to 2012-10-13 Quicklisp. [!!?]
*** Dynamic interfaces idempotent across process -- no more reloading
** HUNCHENTOOT
*** some bugs with underlying streams to be fixed in abcl-1.2-dev
** CXML
Basic XML parsing works. XPath still borked. [???]
* Java 5 bytecode Compiler
The internal Lisp-to-Java bytecode compiler has been hardened by
regression testing across Quicklisp libraries.
** Extensive interpreter/compiler bug fixes due to access to cl-test-suite [???] @antov
** large objects (?!?)
* The facility to construct runtime classes via JNEW-RUNTIME-CLASS (@astalla)
Pretty close to full coverage of primtives for creating synthethic
java classes at runtime. Easy to extend with your needs; sensible
defaults.
** Fields
*** getter/setters
** Annotations
* ASDF
** Stock ASDF-2.26 with conditional patches for the URL-PATHAME and
JAR-PATHNAME implementation extensions to ANSI.
* ABCL-CONTRIB
** ABCL-ASDF
Network installation of binary artifacts named by Maven POM uris.
*** checks at runtime if a given class is present in the
accessible classloaders
*** If the check for the presence of a class fails, find a
maven-3.0.4 binary locally, execute its Aether connector
to retrieve its transitive dependencies from the network.
** JSS
Java Syntax Sucks. q.v [lsw2]
Extensive bugfixing wrt. method resolution [#229]
** JFLI
A "captured from the wild" version of what @rich.hickey did before Clojure.
Changes
-------
* [#249] PATHNAME merge semantics DWIMs on an inferred type
Extends ANSI PATHNAME in a non-conforming manner, which was probably
already the case.
* [r13695] Reimplementation of global symbol macros to avoid using
the symbol's value slot.
* [r13696] DEFMACRO now supports documentation strings as per the
ANSI specification.
* [r13700] ABCL loads under the Weblogic 10.3 application server.
* [r13768] [#193] Allow zero-length symbols
* [r13785] JNEW-RUNTIME-CLASS gets fields and annotations
* [r13790] JNEW-RUNTIME-CLASS getters/setters for fields
* [r13796] [r13797] N3 DOAP description for ABCL
* [r13803] Build target 'abcl-contrib.jar' packages ABCL-CONTRIB
Fixes
-----
* ANSI [#241]
** &AUX parameters fixes RESTAS
* [#221] Stack exhaustsion on funcall in non-existing package
* [#113] DEFSTRUCT concurrency
* [#216][#211] Compiler
** stack inconsistency
* [#187] Better SORT and STABLE-SORT via Jorge Tavares [???]
injecting -Wall -Wno-error does not cause the test to produce the wrong
answer. (If it does, the wrong information is installed in /usr/include,
and ultimately provokes PR 47342.)
Same as -r1.8 of python27's patch-al.
injecting -Wall -Wno-error does not cause the test to produce the wrong
answer. (If it does, the wrong information is installed in /usr/include,
and ultimately provokes PR 47342.)
Highlights
This update release contains the following enhancements:
Additional Certified System Configurations
Security Feature Enhancements
Olson Data 2012i
JDK 7u10 contains Olson time zone data version 2012i. For more information, refer to Timezone Data Versions in the JRE Software.
Security Baselines
The security baselines for the Java Runtime Environment (JRE) at the time of the release of JDK 7u10 are specified in the following table:
JRE Family Version JRE Security Baseline
(Full Version String)
7 1.7.0_09
6 1.6.0_37
5.0 1.5.0_38
1.4.2 1.4.2_40
For more information about security baselines, see Deploying Java Applets With Family JRE Versions in Java Plug-in for Internet Explorer.
Additional Certified System Configurations
For JDK 7u10 release, the following additional system configurations have been certified:
Mac OS X 10.8
Windows 8
For more information, refer to Oracle Certified System Configurations page.
Security Feature Enhancements
The JDK 7u10 release includes the following enhancements:
The ability to disable any Java application from running in the browser. This mode can be set in the Java Control Panel or (on Microsoft Windows platform only) using a command-line install argument.
The ability to select the desired level of security for unsigned applets, Java Web Start applications, and embedded JavaFX applications that run in a browser. Four levels of security are supported. This feature can be set in the Java Control Panel or (on Microsoft Windows platform only) using a command-line install argument.
New dialogs to warn you when the JRE is insecure (either expired or below the security baseline) and needs to be updated.
For more information, see Setting the Level of Security for the Java Client and Java Control Panel.
Bug Fixes
Notable Bug Fixes in JDK 7u10
The following are some of the notable bug fixes included in JDK 7u10.
Area: java command
Description: Wildcard expansion for single entry classpath does not work on Windows platforms.
The Java command and Setting the classpath documents describe how the wildcard character (*) can be used in a classpath element to expand into a list of the .jar files in the associated directory, separated by the classpath separator (;).
This wildcard expansion does not work in a Windows command shell for a single element classpath due to the Microsoft bug described in Wildcard Handling is Broken.
See 7146424.
For a list of other bug fixes included in this release, see JDK 7u10 Bug Fixes page.
Highlights
This update release contains the following enhancements:
Additional Certified System Configurations
Security Feature Enhancements
Olson Data 2012i
JDK 7u10 contains Olson time zone data version 2012i. For more information, refer to Timezone Data Versions in the JRE Software.
Security Baselines
The security baselines for the Java Runtime Environment (JRE) at the time of the release of JDK 7u10 are specified in the following table:
JRE Family Version JRE Security Baseline
(Full Version String)
7 1.7.0_09
6 1.6.0_37
5.0 1.5.0_38
1.4.2 1.4.2_40
For more information about security baselines, see Deploying Java Applets With Family JRE Versions in Java Plug-in for Internet Explorer.
Additional Certified System Configurations
For JDK 7u10 release, the following additional system configurations have been certified:
Mac OS X 10.8
Windows 8
For more information, refer to Oracle Certified System Configurations page.
Security Feature Enhancements
The JDK 7u10 release includes the following enhancements:
The ability to disable any Java application from running in the browser. This mode can be set in the Java Control Panel or (on Microsoft Windows platform only) using a command-line install argument.
The ability to select the desired level of security for unsigned applets, Java Web Start applications, and embedded JavaFX applications that run in a browser. Four levels of security are supported. This feature can be set in the Java Control Panel or (on Microsoft Windows platform only) using a command-line install argument.
New dialogs to warn you when the JRE is insecure (either expired or below the security baseline) and needs to be updated.
For more information, see Setting the Level of Security for the Java Client and Java Control Panel.
Bug Fixes
Notable Bug Fixes in JDK 7u10
The following are some of the notable bug fixes included in JDK 7u10.
Area: java command
Description: Wildcard expansion for single entry classpath does not work on Windows platforms.
The Java command and Setting the classpath documents describe how the wildcard character (*) can be used in a classpath element to expand into a list of the .jar files in the associated directory, separated by the classpath separator (;).
This wildcard expansion does not work in a Windows command shell for a single element classpath due to the Microsoft bug described in Wildcard Handling is Broken.
See 7146424.
For a list of other bug fixes included in this release, see JDK 7u10 Bug Fixes page.
Set LICENSE while here.
Change in GNU Prolog version 1.4.2:
* fix a bug in the x86/NetBSD port
* fix a bug in the compiler for byte-code with op/3 directive
* fix a bug in the debugger
* modify decompose_file_name/4 (fix problems under windows)
* add built-in is_absolute_file_name/1 and is_relative_file_name/1
* modify the compiler include/1 directive handling
(if the file to include is not found, seach in directories of parent includers)
* modify atom table management (its size can be defined via env. var MAX_ATOM)
* fix a bug with soft-call inside a meta-call
* implement term_hash/2 and term_hash/4. Bacward incompatibility:
new_atom/3 and and atom_hash/2 no longer exists.
* fix some little bugs with 64 bits (e.g. stream id)
* modify the FD solver to handle very long computations
* fix a bug in the compiler (unification with fresh vars in the body)
* fix a bug with *-> containing ! in the test part (! was not local to the test)
* fix a bug to configure with sigaction on old linux kernels
* fix some problems/bugs on 64 bits machine
Change in GNU Prolog version 1.4.1:
* improve signal handling
* add an option --wam-comment to gplc and pl2wam
* fix multifile directive (works now with an empty predicate as required by ISO)
* fix absolute_file_name to expand ~ using HOMEDRIVE and HOMEPATH under windows
if HOME is not defined
* improve listing/0-1 output
* add soft cut control construct and its associated operator *->
* improve the top-level results in case of cyclic terms
* fix arithmetic evaluable functor ^/2 to work with floats
* increase maximum number of variables in a term
* add write_term option variable_names
* add built-in predicates between/3 and succ/2
* fix bug in the DCG expander
* fix bug in member/2
* recognize escape sequence \s (space) and \e (escape) if strict_iso is off
* add error detection in length/2 if given length is negative
* add built-in predicates maplist/2-5
* fix a regression bug in the FD solver about sparse domains
* increase size of FD internal stacks and fix memory leak
* port to x86_64/Darwin (Mac OS X) - many thanks to:
Ozaki Kiichi <gclient.gaap@gmail.com>
* fix a bug in x86_64 with --disable-regs
* fix a bug when consulting a file under Win XP/Vista 32 bits
* fix a bug when consulting a file using '$VAR'(N) or '$VARNAME'(A)
* fix a bug in new_atom/1-2 which returned duplicates
* fix a bug in write/1 when an empty atom is passed
* improve portray_clause (numbervars and space before final dot)
Change in GNU Prolog version 1.4.0:
* GNU Prolog is now licensed under a dual license LGPL or GPL
* port to x86_64/MinGW - many thanks to:
Jasper Taylor <jasper@simulistics.com> (see src/WINDOWS64)
* port to x86_64/MSVC (see src/WINDOWS64)
* add a configure option to control Windows HtmlHelp
--disable-htmlhelp or --enable-htmlhelp[=static/dynamic]
* improve a lot (and fix some bugs in) the Windows GUI Console
* change location of gprologvars.bat under Windows (in install directory)
* increase default stack sizes (32Mb for heap, 16Mb for others)
* change the default setting for flag strict_iso: it is on now
* add control constructs to the predicate table
* modify predicate_property/2 (built_in_fd ==> built_in, add control_construct)
only accepts a Head (a callable) (no longer a predicate indicator)
* fix a bug in the compiler (bad unification with singleton variable)
* fix a bug with strict_iso flag (was not passed to consult)
* add shebang support using #!/usr/bin/gprolog --consult-file
* modify the mangling scheme for future module support (see hexgplc)
* fix write_term default options (now numbervars(false) and namevars(false))
* fix read/1: tab and newlines are not accepted inside single/back/double quoted tokens
* add additional errors to compare/3 and keysort/2
* accept space under the top-level (same as ;)
* modify portray_clause/1-2 to add a newline at the end of the output
* add acyclic_term/1 (compatibility only since GNU Prolog does not handle cyclic terms)
* fix write/1 to treat '$VARNAME'(Atom) as a var name only if Atom is a valid var name
* rename evaluable functor atan/2 as atan2/2 and >< as xor
* add evaluable functor div/2
* detect op/3 error cases for | [] {}
* replace type_error(variable, X) by uninstantiation_error(X) (e.g. open/3-4)
* add built-in term_variables/2-3 and subsumes_term/2
* add some type tests on chars and codes (in number_chars/2, number_codes/2,..)
* fix some little bugs in the parser
* add meta_predicate property to predicate_property/2
* fix a memory leak in atom_concat/3 (in case of failure)
* add infix operator '|' (and allow it to be unquoted in read/write)
* improve top-level variables display adding () when needed
* support the ISO multifile/1 directive
* add built-ins false/0 and forall/2
* detect an instantiation_error in phrase/2-3
* allow rounding functions to accept an integer if strict_iso is off
* group all examples under a new directory 'examples'
* fix a bug in read_from_codes/2 and number_codes/2
* improve speed of built-in predicates on list (append, member, reverse,...).
* improve CTRL+C handling under the top-level
* add is_list/1 (same as list/1)
* add Prolog flags: dialect, home, host_os, host_vendor, host_cpu,
host, arch, version, version_data, unix, argv
* add preprocessor directives if/1 else/0 elif/1 endif/0
* fix a bug on large ints in the byte-code for 64-bits machine
* fix a bug with call/2-N
* change listing/0-1 printing stream: now it is current_output
* add a new stream alias: user_error associated to stderr
* add evaluable functors: (a)sinh/1, (a)cosh/1, (a)tanh/1
* add evaluable functors: epsilon/0, lsb/1, msb/1, popcount/1
* fix compilation problem under Mac OS X Snow Leopard (force 32-bits mode)
* add evaluable functors: log/2, gcd/2, tan/1, atan2/2, pi/0, e/0
* add built-in ground/1
* rename built-in sort0 as msort
* add new error detection for keysort
* accept (but ignore) directive encoding/1
* add xor/2 (bitwise XOR) ^/2 becomes integer exponentiation
* improve randomize/0 (more different values on consecutive calls)
* relax the lexer to also accept 0'' (ISO requires 0''' or 0'\') is strict_iso is off
* fix a bug with top-level options --entry-goal and --query-goal
This is the Linux port of the Sun Java(tm) Runtime Environment (J2SE 7.0).
* builtin.mk is not tested. BUILTIN_FIND_FILES.JAVAVM7 should be fixed
* Not for NetBSD 5
remove unnecessary conditional that broke build on NetBSD-6.99.15/amd64.
While here, replace another interpreter and skip one more file since
it gets replaced much later.
Bump PKGREVISION.
Changes since last release
==========================
Some highlights of this release are:
* Lots of bugs fixed.
* The MOP has been fixed to work with the upcoming release of
Closer-MOP
* ECL now produces a much more readable C code, with indentation and
more explicit declarations of variables.
Known issues
============
* Cygwin's library is still broken: fork/exec fails to reload the
cygwin library, or ECL's compiled libraries in a completely random
fashion. For this reason we recommend using ext:system instead of
ext:run-program in that platform.
* In Windows ECL comes with bytecodes compiler by default, because C
compilers are normally not avaiable. Unfortunately several
libraries out there are not prepared for this. If you plan to use
quicklisp and have a C compiler accessible to ECL, you may use
(ext:install-c-compiler) to switch back to the Lisp-to-C compiler.
changes in sbcl-1.1.2 relative to sbcl-1.1.1:
* notice: System requirements for SBCL on Microsoft Windows: Windows NT 5.1
or newer (Windows XP, Server 2003) is required. Support for Windows 2000
(NT 5.0) is no longer being maintained.
* notice: Starting with this version, SBCL on Windows no longer supports
building with disabled thread support.
* enhancement: frlocks have been added to SB-CONCURRENCY contrib module.
* enhancement: New feature sb-dynamic-core allows the runtime to be
rebuilt or relocated without requiring changes to the core file on
all linkage table platforms. Required on Windows. (Thanks to Anton
Kovalenko.)
* enhancement: Console I/O streams use UCS-2. (Thanks to Anton Kovalenko.)
* enhancement: I/O on Windows unnamed pipes is interruptible
asynchronously using interrupt-thread, timers when running on Windows NT
version 6.1 or newer (Windows 7, Server 2008 R2). (Thanks to Anton
Kovalenko.)
* enhancement: Support for the experimental safepoint-based stop-the-world
protocol on the PowerPC platform.
* bug fix: Non-blocking reads from the Windows console were not necessarily
non-blocking. Thanks to Anton Kovalenko. (lp#308923)
* bug fix: stability of threads on Windows has been improved upon through
an updated stop-the-world protocol (thanks to Anton Kovalenko).
GCC 4.7.2 is the first bug-fix release containing important fixes
for regressions and serious bugs in GCC 4.7.1 with over 70 bugs
fixed since the previous release.
A notable change in GCC 4.7.2 compared to 4.7.1 are ABI bug fixes
related to some C++11 templates (std::list and std::pair). As a result,
code using those templates in C++11 mode is again ABI compatible with
code in C++03/C++98 mode or C++11 mode of GCC 4.6 and earlier, but might
be ABI incompatible with code compiled by GCC 4.7.1 or 4.7.0 in C++11
mode. See http://gcc.gnu.org/gcc-4.7/changes.html for more details.
This is the list of problem reports (PRs) from GCC's bug tracking system
that are known to be fixed in this release. This list might not be complete
(that is, it is possible that some PRs that have been fixed are not listed
here).
http://gcc.gnu.org/bugzilla/buglist.cgi?bug_status=RESOLVED&resolution=FIXED&target_milestone=4.7.2
1) Don't pass both gcc 4.4 and gcc 4.7 paths to the driver. Detect
if gcc47 is available and use those paths, otherwise fall back to
gcc44.
2) Add support for exception handling
3) Add rdynamic support
4) Add gnu-hash style support
5) Fix (!!) crtstuff (This was obsolete, include PIE support)
6) Remove rpath-link
7) Remove unneeded duplicate libgcc handling
8) Make libgcc handling match gcc specs (different for gcc 4.4 and 4.7)
9) Update dragonfly driver test
Changelog:
Java(TM) SE Development Kit 6, Update 37 (JDK 6u37)
The full version string for this update release is 1.6.0_37-b06 (where "b" means "build") and the version number is 6u37.
Olson Data 2012c
JDK 6u37 contains Olson time zone data version 2012c. For more information, refer to Timezone Data Versions in the JRE Software.
Security Baselines
The security baselines for the Java Runtime Environment (JRE) at the time of the release of JDK 6u37 are specified in the following table:
JRE Family Version JRE Security Baseline(Full Version String)
6 1.6.0_37
5.0 1.5.0_38
1.4.2 1.4.2_40
For more information about security baselines, see Deploying Java Applets With Family JRE Versions in Java Plug-in for Internet Explorer.
Blacklist Entries
This update release includes the following new entries to the Blacklist:
Cisco AnyConnect Secure Mobility Client
Note: For more information, see Blacklist Jar Feature documentation.
Bug Fixes
This release contains fixes for security vulnerabilities. For more information, see Oracle Java SE Critical Patch Update Advisory.
The following table lists some of the notable bug fixes included in this release:
Bug ID Category Sub_Category Description
7183263 java_deployment security Regression: crossdomain.xml with dtd does not work
7195301 java classese_security XML Signature DOM implementation should not use instanceof to determine type of Node
* --enable-aqua build for Mac OS X is now a Cocoa implementation.
* Support has been added for Cygwin network pathnames.
* Updated to Unicode 6.2 support. Fixes for several crashes and bugs.
Local changes:
o Remove patch now included upstream
o Adapt PLIST to installed files
Upstream changes:
- Core
+ Prevent interpreter from dying twice
+ Complete rewrite of the IO system, including new unified IO PMC
semantics.
+ The Integer and Float PMCs now have a get_pointer vtable which is
needed when using NCI to bind to Fortran libraries such as LAPACK
- Deprecations
+ Moved dynpmc/os to pmc os. loadlib 'os' is not needed anymore.
- Platforms
+ Fixed for the FileHandle open method the append mode on Windows.
+ Fix compilation on Windows without working mt.exe
+ Detect GNU/Hurd as linux proper.
+ Fixed broken int3 trap on Solaris with gcc.
+ Updated the vms port on a YAPC::EU hackathon with vaxman and mvorl.
- Tests
+ Improve testability with valgrind or thread-sanitizer
Clang was hardwired to search for crt* stuff and libstdc++ at
/usr/lib/gcc41. This worked for most people even when DragonFly
moved to gcc 4.4 as the primary base compiler since gcc 4.1 was
usually also on the system.
With the release of DragonFly 3.2, gcc 4.7 replaced gcc 4.1 and
clang stopped compiling due to not being able to find libraries and
crt* objects. The new patches make clang driver first look for
gcc 4.7 and failing to find that: gcc 4.4.
The other patches were "de-fuzzed".
Revision bump was necessary because clang did build, it just didn't
work.
Patches submitted upstream:
http://llvm.org/bugs/show_bug.cgi?id=14417
Changelog:
2012-11-21
# Changes and additions
* On Windows, process now returns real process ids as in UNIX, not Windows process handles.
* The cgi.lsp module now handles multiform data in POST requests.
* Two new make files for compiling RedHat Fedora and CentOS distributions. The configure utility called by make will handle these two subflavors of RedHat Linux automatically.
# Bug fixes
* Memory overrun of invalid UTF8 strings now causes an error message "invalid UTF8 string".
* The function ref did sometimes not handle correctly multiple, nested matching expressions.
* The float function did sometimes not work correctly when used on list members.
* OpenBSD did not load .init.lsp.
# Compatibility with previous versions
* This version is compatible with previous versions in the 10.4 series of newLISP.
tcl_platform(machine), instead of using $MACHINE there.
This is in preparation for reverting the recent change
to the net/tcl-scotty PLIST.
Bump PKGREVISION.
architectures. Honour data and address space limits on all BSDs. Explicitly
limit the heap size during bootstrap to 256MB. This fixes e.g. my bulk
build, which is run with an AS limit of 2GB. Since hw.usermem would
tell the bootstrap JVM that > 3GB are available, initialisation would
fail. Bump revision.
changes in sbcl-1.1.1 relative to sbcl-1.1.0:
* enhancement: WITH-COMPILATION-UNIT no longer grabs the world-lock.
(COMPILE and COMPILE-FILE still do.)
* optimization: the SPARC backend now supports the precise generational
(GENCGC) garbage collection. Enabled by default on Solaris/SPARC and
Linux/SPARC. Thanks to Raymond Toy (via CMUCL).
* enhancement: add experimental support for the SB-THREAD feature and the
timer facility on Windows. Thanks to Dmitry Kalyanov and Anton Kovalenko.
Threads are enabled by default, and this version of SBCL is considered
to be the last and final release to officially support building with
threads disabled.
* optimization: The compiler no longer rotates loops in some cases where
this transformation actually lead to worse code being generated.
* bug fix: SB-CLTL2:MACROEXPAND-ALL correctly handles shadowing of
symbol-macros by lexical bindings.
* bug fix: stack allocation was prevented by high DEBUG declaration in
several cases.
* bug fix: SB-EXT:GC-LOGFILE signaled an error when no logfile was set.
(thanks to SANO Masatoshi)
* bug fix: PARSE-NATIVE-NAMESTRING performed non-native parsing when
:JUNK-ALLOWED was true.
* bug fix: type derivation inferred overly conservative types for
unions of array types. (lp#1050768)
richards@cs.princeton.edu). Updated package to use PLIST_VARS and CONF_FILES.
Updated coq to version 8.4. Changes include:
Logic
- Standard eta-conversion now supported (dependent product only).
- Guard condition improvement: subterm property is propagated through beta-redex
blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x";
this allows for instance to use "rewrite ... in ..." without breaking
the guard condition.
Vernacular commands
- The "Reset" command is now supported again in files given to coqc or Load.
- "Show Script" now indents again the displayed scripts. It can also work
correctly across Load'ed files if the option "Unset Atomic Load" is used.
- "Open Scope" can now be given the delimiter (e.g. Z) instead of the full
scope name (e.g. Z_scope).
- Commands "Back" and "BackTo" are now handling the proof states. They may
perform some extra steps of backtrack to avoid states where the proof
state is unavailable (typically a closed proof).
- The commands "Suspend" and "Resume" have been removed.
- A basic Show Script has been reintroduced (no indentation).
- New command "Set Parsing Explicit" for deactivating parsing (and printing)
of implicit arguments (useful for teaching).
- New command "Grab Existential Variables" to transform the unresolved evars
at the end of a proof into goals.
- It is now mandatory to have a space (or tabulation or newline or end-of-file)
after a "." ending a sentence.
- In SearchAbout, the [ ] delimiters are now optional.
- New command "Add/Remove Search Blacklist <substring> ...":
a Search or SearchAbout or similar query will never mention lemmas
whose qualified names contain any of the declared substrings.
The default blacklisted substrings are "_admitted" "_subproof" "Private_".
- When the output file of "Print Universes" ends in ".dot" or ".gv",
the universe graph is printed in the DOT language, and can be
processed by Graphviz tools.
- New command "Print Sorted Universes".
- The undocumented and obsolete option "Set/Unset Boxed Definitions" has
been removed, as well as syntaxes like "Boxed Fixpoint foo".
- A new option "Set Default Timeout n / Unset Default Timeout".
- Qed now uses information from the reduction tactics used in proof script
to avoid conversion at Qed time to go into a very long computation.
- New command "Show Goal ident" to display the statement of a goal, even
a closed one (available from Proof General).
- Command "Proof" accept a new modifier "using" to force generalization
over a given list of section variables at section ending.
- New command "Arguments" generalizing "Implicit Arguments" and
"Arguments Scope" and that also allows to rename the parameters of a
definition and to tune the behavior of the tactic "simpl".
Specification language and Notations
- Most compatibility notations of the standard library are now tagged as
(compat xyz), where xyz is a former Coq version, for instance "8.3".
These notations behave as (only parsing) notations, except that they may
triggers warnings (or errors) when used while Coq is not in a corresponding
-compat mode.
- To activate these compatibility warnings, use "Set Verbose Compat Notations"
or the command-line flag -verbose-compat-notations.
- For a strict mode without these compatibility notations, use
"Unset Compat Notations" or the command-line flag -no-compat-notations.
- Maximal implicit arguments can now be set locally by { }. The registration
traverses fixpoints and lambdas. Because there is conversion in types,
maximal implicit arguments are not taken into account in partial
applications (use eta expanded form with explicit { } instead).
- Added support for recursive notations with binders (allows for instance
to write "exists x y z, P").
- Structure/Record printing can be disable by "Unset Printing Records".
In addition, it can be controlled on type by type basis using
"Add Printing Record" or "Add Printing Constructor".
- Pattern-matching compilation algorithm: in "match x, y with ... end",
possible dependencies of x (or of the indices of its type) in the type
of y are now taken into account.
Tactics
- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
or "induction" to make it generate equations in the spirit of "case_eq".
The former syntax "_eqn" is discontinued.
- The name of the hypothesis introduced by tactic "remember" can be
set via the new syntax "remember t as x eqn:H" (wish #2489).
- Still no general "info" tactical, but new specific tactics info_auto,
info_eauto, info_trivial which provides information on the proofs found
by auto/eauto/trivial. Display of these details could also be activated by
"Set Info Auto"/"Set Info Eauto"/"Set Info Trivial".
- Details on everything tried by auto/eauto/trivial during a proof search
could be obtained by "debug auto", "debug eauto", "debug trivial" or by a
global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial".
- New command "r string" in Ltac debugger that interprets "idtac
string" in Ltac code as a breakpoint and jumps to its next use.
- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
harvey, zenon, gwhy) have been removed, since Why2 has not been
maintained for the last few years. The Why3 plugin should be a suitable
replacement in most cases.
- New proof engine.
- Scripts can now be structured thanks to bullets - * + and to subgoal
delimitation via { }. Note: for use with Proof General, a cvs version of
Proof General no older than mid-July 2011 is currently required.
- Support for tactical "info" is suspended.
- Support for command "Show Script" is suspended.
- New tactics constr_eq, is_evar and has_evar for use in Ltac.
- Removed the two-argument variant of "decide equality".
- New experimental tactical "timeout <n> <tac>". Since <n> is a time
in second for the moment, this feature should rather be avoided
in scripts meant to be machine-independent.
- Fix in "destruct": removal of unexpected local definitions in context might
result in some rare incompatibilities (solvable by adapting name hypotheses).
- Introduction pattern "_" made more robust.
- Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C.
- Unification in "apply" supports unification of patterns of the form
?f x y = g(x,y) (compatibility ensured by using
"Unset Tactic Pattern Unification"). It also supports (full) betaiota.
- Tactic autorewrite does no longer instantiate pre-existing
existential variables (theoretical source of possible incompatibilities).
- Tactic "dependent rewrite" now supports equality in "sig".
- Tactic omega now understands Zpred (wish #1912) and can prove any goal
from a context containing an arithmetical contradiction (wish #2236).
- Using "auto with nocore" disables the use of the "core" database (wish #2188).
This pseudo-database "nocore" can also be used with trivial and eauto.
- Tactics "set", "destruct" and "induction" accepts incomplete terms and
use the goal to complete the pattern assuming it is non ambiguous.
- When used on arguments with a dependent type, tactics such as
"destruct", "induction", "case", "elim", etc. now try to abstract
automatically the dependencies over the arguments of the types
(based on initial ideas from Chung-Kil Hur, extension to nested
dependencies suggested by Dan Grayson)
- Tactic "injection" now failing on an equality showing no constructors while
it was formerly generalizing again the goal over the given equality.
- In Ltac, the "context [...]" syntax has now a variant "appcontext [...]"
allowing to match partial applications in larger applications.
- When applying destruct or inversion on a fixpoint hiding an inductive
type, recursive calls to the fixpoint now remain folded by default (rare
source of incompatibility generally solvable by adding a call to simpl).
- In an ltac pattern containing a "match", a final "| _ => _" branch could be
used now instead of enumerating all remaining constructors. Moreover, the
pattern "match _ with _ => _ end" now allows to match any "match". A "in"
annotation can also be added to restrict to a precise inductive type.
- The behavior of "simpl" can be tuned using the "Arguments" vernacular.
In particular constants can be marked so that they are always/never unfolded
by "simpl", or unfolded only when a set of arguments evaluates to a
constructor. Last one can mark a constant so that it is unfolded only if the
simplified term does not expose a match in head position.
Libraries
- Reals: changed definition of PI, no more axiom about sin(PI/2).
- SetoidPermutation: a notion of permutation for lists modulo a setoid equality.
- BigN: fixed the ocaml code doing the parsing/printing of big numbers.
- MSetRBT: a new implementation of MSets via Red-Black trees (initial
contribution by Andrew Appel).
- MSetAVL: for maximal sharing with the new MSetRBT, the argument order
of Node has changed (this should be transparent to regular MSets users).
- Extension of the abstract part of Numbers, which now provide axiomatizations
and results about many more integer functions, such as pow, gcd, lcm, sqrt,
log2 and bitwise functions. These functions are implemented for nat, N, BigN,
Z, BigZ. See in particular file NPeano for new functions about nat.
- The definition of types positive, N, Z is now in file BinNums.v
- Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains
an internal module Z implementing the Numbers interface for integers.
This module Z regroups:
* all functions over type Z : Z.add, Z.mul, ...
* the minimal proofs of specifications for these functions : Z.add_0_l, ...
* an instantation of all derived properties proved generically in Numbers :
Z.add_comm, Z.add_assoc, ...
A large part of ZArith is now simply compatibility notations, for instance
Zplus_comm is an alias for Z.add_comm. The direct use of module Z is now
recommended instead of relying on these compatibility notations.
- Similar major reorganization of NArith, via a module N in NArith/BinNat.v
- Concerning the positive datatype, BinPos.v is now in a specific directory
PArith, and contains an internal submodule Pos. We regroup there functions
such as Pos.add Pos.mul etc as well as many results about them. These results
are here proved directly (no Number interface for strictly positive numbers).
- Note that in spite of the compatibility layers, all these reorganizations
may induce some marginal incompatibilies in scripts. In particular:
* the "?=" notation for positive now refers to a binary function Pos.compare,
instead of the infamous ternary Pcompare (now Pos.compare_cont).
* some hypothesis names generated by the system may changed (typically for
a "destruct Z_le_gt_dec") since naming is done after the short name of
the head predicate (here now "le" in module Z instead of "Zle", etc).
* the internals of Z.add has changed, now relying of Z.pos_sub.
- Also note these new notations:
* "<?" "<=?" "=?" for boolean tests such as Z.ltb Z.leb Z.eqb.
* "÷" for the alternative integer division Z.quot implementing the Truncate
convention (former ZOdiv), while the notation for the Coq usual division
Z.div implementing the Flooring convention remains "/". Their corresponding
modulo functions are Z.rem (no notations) for Z.quot and Z.modulo (infix
"mod" notation) for Z.div.
- Lemmas about conversions between these datatypes are also organized
in modules, see for instance modules Z2Nat, N2Z, etc.
- When creating BigN, the macro-generated part NMake_gen is much smaller.
The generic part NMake has been reworked and improved. Some changes
may introduce incompatibilities. In particular, the order of the arguments
for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now
comes first. By default, the power function now takes two BigN.
- Creation of Vector, an independent library for lists indexed by their length.
Vectors' names overwrite lists' one so you should not "Import" the library.
All old names changed: function names follow the ocaml ones and, for example,
Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing
Vector.VectorNotations.
- Removal of TheoryList. Requiring List instead should work most of the time.
- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
eq_rect_r (available by importing module EqNotations).
- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument).
Module System
- The names of modules (and module types) are now in a fully separated
namespace from ordinary definitions: "Definition E:=0. Module E. End E."
is now accepted.
- During subtyping checks, an opaque constant in a module type could now
be implemented by anything of the right type, even if bodies differ.
Said otherwise, with respect to subtyping, an opaque constant behaves
just as a parameter. Coqchk was already implementing this, but not coqtop.
- The inlining done during application of functors can now be controlled
more precisely, by the annotations (no inline) or (inline at level XX).
With the latter annotation, only functor parameters whose levels
are lower or equal than XX will be inlined.
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
- Print Assumptions should now handle correctly opaque modules (#2168).
- Print Module (Type) now tries to print more details, such as types and
bodies of the module elements. Note that Print Module Type could be
used on a module to display only its interface. The option
"Set Short Module Printing" could be used to switch back to the earlier
behavior were only field names were displayed.
CoqIDE
- Coqide now supports the "Restart" command, and "Undo" (with a warning).
Better support for "Abort".
- Coqide now runs coqtop as separated process, making it more robust:
coqtop subprocess can be interrupted, or even killed and relaunched
(cf button "Restart Coq", ex-"Go to Start"). For allowing such
interrupts, the Windows version of coqide now requires Windows >= XP
SP1.
- The communication between CoqIDE and Coqtop is now done via a dialect of XML.
- The backtrack engine of CoqIDE has been reworked, it now uses the
"Backtrack" command similarly to Proof General.
- The Coqide parsing of sentences has be reworked and now supports
tactic delimitation via { }.
- Coqide now accepts the Abort command (wish #2357).
- Coqide can read coq_makefile files as "project file" and use it to
set automatically options to send to coqtop.
- Preference files have moved to $XDG_CONFIG_HOME/coq and accelerators
are not stored as a list anymore.
Internal infrastructure
- Opaque proofs are now loaded lazily by default. This allows to be almost as
fast as -dont-load-proofs, while being safer (no creation of axioms) and
avoiding feature restrictions (Print and Print Assumptions work ok).
- Revised hash-consing code allowing more sharing of memory
- Experimental support added for camlp4 (the one provided alongside ocaml),
simply pass option -usecamlp4 to ./configure. By default camlp5 is used.
- Revised build system: no more stages in Makefile thanks to some recursive
aspect of recent gnu make, use of vo.itarget files containing .v to compile
for both make and ocamlbuild, etc.
- Support of cross-compilation via mingw from unix toward Windows,
contact P. Letouzey for more informations.
- New Makefile rules mli-doc to make html of mli in dev/doc/html and
full-stdlib to get a (huge) pdf reflecting the whole standard library.
Extraction
- By default, opaque terms are now truly considered opaque by extraction:
instead of accessing their body, they are now considered as axioms.
The previous behaviour can be reactivated via the option
"Set Extraction AccessOpaque".
- The pretty-printer for Haskell now produces layout-independant code
- A new command "Separate Extraction cst1 cst2 ..." that mixes a
minimal extracted environment a la "Recursive Extraction" and the
production of several files (one per coq source) a la "Extraction Library".
- New option "Set/Unset Extraction KeepSingleton" for preventing the
extraction to optimize singleton container types.
- The extraction now identifies and properly rejects a particular case of
universe polymorphism it cannot handle yet (the pair (I,I) being Prop).
- Support of anonymous fields in record (#2555).
Tools
- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq,
$XDG_DATA_DIRS/coq, and user-contribs before the standard library.
- Coq rc file has moved to $XDG_CONFIG_HOME/coq.
- Major changes to coq_makefile:
* mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work;
* mlihtml generates doc of mli, install-doc install the html doc in DOCDIR
with the same policy as vo in COQLIB;
* More variables are given by coqtop -config, others are defined only if the
users doesn't have defined them elsewhere. Consequently, generated makefile
should work directly on any architecture;
* Packagers can take advantage of $(DSTROOT) introduction. Installation can
be made in $XDG_DATA_HOME/coq;
* -arg option allows to send option as argument to coqc.
Changes in Squeak 4.3.
There aren't any applications bundled with this release.
Instead of working on applications to bundle with the image,
core developers have been inspired by the Cog virtual machine
to look deeply into the image for things they wanted to change.
As a result, the image is becoming smaller, tidier, and nimbler.
There are five Welcome Workspaces in Squeak 4.3.
The second is called Future Directions:
- This image is ~15M. If you execute - Smalltalk unloadAllKnownPackages -
it will become ~10M
- A SqueakCore image is available at http://ftp.squeak.org/4.3
- A reasonable target is the creation of a smaller image,
which may be a task before the community
- A place to explore where to make reductions is likely the
removal/replacement of GUIs
- Once we have a smaller core image, we can employ Andreas Raab's memo [1]
on how to load code back into the image. This will be based on tests
delineating the separate responsibilities of core and application developers
[1] http://lists.squeakfoundation.org/pipermail/squeak-dev/2010-May/150658.html
Changes in Squeak 4.2
* Preparation for adoption of Cog VM
* Significant class-library and IDE improvements, with many speed improvements
* High-precision Clock (microsecond precision)
* Cleaned-up code base, with better support for unloading optional packages and fonts.
* The last of the underscore assignments have been replaced with ANSI assignments.
* Refactoring and unification of Smalltalk and SmalltalkImage globals.
* API for stdio access (requires recent VM)
* Improved command-line interface
* Better Documentation (see Help > Help Browser)
* SUnit now supports timeouts
* More UI work including a tweaked look and feel, and support for translucent fonts
* Support for classic MVC has been restored to Squeak for better support of slower devices
* System Reporter (found under Help > About this system) - a tool
to simplify and standardise the reporting of your image's
set-up.
Changes in Squeak 4.1
This version combines the licence change occurring in the 4.0 release
with the development work that has been going on while the re-licensing
process took place.
Much of the work in this release has been focused on fundamental
improvements. Major achievements are the integration of Cog's
closure implementation, the improved UI look and feel,
the new anti-aliased fonts, the core library improvements,
and the modularity advances.
One key focus for this release was to address the issues that
have been known to frustrate developers using Squeak for the
first time. A much improved set of UI widgets, the new menu bar
including the fast search control, integrated help, improved
test coverage, more class and method comments, and integrated
syntax highlighting all make the system more accessible. The new
full closures, the new traits implementation, multiple
improvements to the collections and streams classes, the new
NumberParser hierarchy all help make development easier and
produce cleaner, faster code. Deploying your completed
applications will be made easier by the work done on making many
modules unloadable, and by support for other cleanup activities.
libXext/buildlink3.mk, now that it is included there.
Leave the places where its API version is set or variables from it
are used directly (about 3 packages).
2.10.9
Fix a libgdiplus issue that had forced linking against Apple's X11 stack for text rendering.
Fix issue where a native crash causes MonoDevelop to hang and neither Force Quit nor kill -9 would terminate it (Xamarin #2548).
Fix sgen failing with Assertion at sgen-gc.c:2506, condition `mono_sgen_need_bridge_processing ()' not met.
2.10.8
Changes
Updated the Task Parallel Library to include the latest fixes from our main development branch.
SQLiteConnection can now set the threading mode (Xamarin #652)
Improved the debugger protocol to speed up debugging and value lookup
Added basic support for MSBuild 4.0 (Leszek Ciesielski, Paul Selormey)
NuGet now runs on Mono
Phalanger 3.0 now runs with Mono
Adds support for some Azure libraries
Added support for bundling profilers in a static binary
The profiler can now log its data to any file descriptor (for over-the-net profile logging)
SGen now has native support for object systems that implement ToggleRefs
Mobile Profile now contains System.IO.MemoryMappedFiles
Added PerformanceCounters for JIT statistics
Add support for Android CPU count.
HashSet<T> can now be serialized (Neale Ferguson)
Bug Fixes
The --profile loader will now work on MacOS X without setting any environment variables
Fixes slow start on threads (Xamarin #1036)
Fixed the SGen interaction between weak references and ephemerons
Fixes --profile=log on x64 systems (Xamarin #971)
Fixes crash on some debugging configurations (Xamarin #1093)
Fixes timezone race condition (Xamarin #1055)
Fixes SendAsync reporting the wrong number of bytes sent (Xamarin #531)
Plug a managed leak in the ASP.NET stack (HttpResponse)
Fix an infinite loop in Path.GetTempFileName
Fixes Soap12 message serialisation incorrect for ReplyTo header value (Xamarin #1244)
Linked away exception on AsyncWaitHandle.WaitOne() on device (Xamarin #1144)
Fixed MonoDoc to avoid loading the same documentation more than once (fixes MonoDoc browser)
Fixes regression in System.Diagnostics.Process.PrivateMemorySize64 (Xamarin #1459)
ASP.NET fix for WebResource.axd and hashes containing /
ServiceModel now allows https endpoints (Xamarin #1203)
ServiceModel now allow requests with no headers (Xamarin #1205 and #1207 by Mario Kosmiskaso)
Fix for WebOperationContext.IncomingResponse (Xamarin #1209 by Mario Kosmiskaso)
Fix for propagating operation context (Xamarin #1210 by Mario Kosmiskaso)
Fix WebConnectionStream to return the correct length for input streams
Fix serialization reader (Xamarin #1462)
Various fixes to System.IO.Packaging
mono-service now passes the command line arguments to the services
Alternate path separator on Unix improves compatibility with Windows software
Fixes xsi:nil handling (Xamarin #1198)
Fixes hang caused by gdb attaching to the wrong process when Mono hard-crashes
Fixes the handling of XmlSchemaFrom importing, which is exposed by WebSphere WSDL tools
Fixes crash on inlined code that contained some patterns of exception throwing (Xamarin #1835)
Fixes monotonic clock on OSX and iOS (Xamarin #1366)
Fixes leak in Process class if WaitForExit was not called (Xamarin #1682)
Fixes typo in ASP.NET's SQLServer SessionState
Fixes marshaling of IPv6 addresses in Win32
Fixes race in ServiceModel.Logger
Fixes string truncation in Tds protocol (Xamarin #1916, Neale Ferguson)
Fixes System.Data DataView sorting
Fixes Debug information for dynamic methods (Novell #731579)
On Android, stdout/stderr become the logcat
Fixes ConditionalWeakTable behavior with SGen (Xamarin #1175)
Fixes SIGSEGV during GC when write barrier is set to cardtable (Xamarin #1917)
Added JSonSerializer support for nullables (Xamarin #163)
Fixes deadlock on SDB (Xamarin #2190)
Fixes heuristics for inserting breakpoints (Xamarin #407)
Fixes Array.Containsfor null items via ICollection<T> (Xamarin #2260)
Fixes scanning of complex values in SGen (Xamarin #228)
Fixes assignability of arrays with generic interfaces (Xamarin #2304)
Fixes FullAOT support for iterating Linq.OrderedEnumerable (Xamarin #2155)
Fix a libgdiplus issue that had forced linking against Apple's X11 stack for text rendering on MacOS.
Fix issue on Mac where a native crash causes MonoDevelop to hang and neither Force Quit nor kill -9 would terminate it (Xamarin #2548).
Mobile Profile Fixes
Xamarin 233: support commit/rollback/update events in iOS/Sqlite
Xamarin 154: Support Dispose on BinaryReader on the Mobile Profile
SGen bridge processing is now a two-step process (used for Mono/Android)
Xamarin 1999: all threads are now wrapped in NSAutoreleasePools.
The rm class doesn't always work for me because miniperl regenerates
some Makefiles and then overwrites the substed file. I haven't tracked
the exact reason that triggers this down yet.
