earlier, but there became no-ops due to my change to db4/bl3 and thus
didn't do harm. Now that part of that change was backed out they became
harmful again and thus need to go.
changes. The "dbm" module could fail to build correctly, erroring out with:
*** WARNING: renaming "dbm" since importing it failed: build/lib.linux-i686-2.4/dbm.so: undefined symbol: dbm_firstkey
In this case, the "dbm" module has accidentally linked with "databases/gdbm",
which happens to be installed, but was never buildlinked in. It may be
relevant that /usr/include/gdbm/ndbm.h is installed on this system.
Remove the "gdbm" test from the "dbm" module configuration, leaving the "ndbm"
support, and the fall-back "bdb" support (which will likely fall back to db4).
Bump PKGREVISION - the package would still install, but with missing
functionality.
changes. The "dbm" module could fail to build correctly, erroring out with:
*** WARNING: renaming "dbm" since importing it failed: build/lib.linux-i686-2.5/dbm.so: undefined symbol: dbm_firstkey
In this case, the "dbm" module has accidentally linked with "databases/gdbm",
which happens to be installed, but was never buildlinked in. It may be
relevant that /usr/include/gdbm/ndbm.h is installed on this system.
Remove the "gdbm" test from the "dbm" module configuration, leaving the "ndbm"
support, and the fall-back "bdb" support (which will likely fall back to db4).
Bump PKGREVISION - the package would still install, but with missing
functionality.
on Linux one can't build some extensions against an old Python (with
spurious -ldb4 linkage) anymore
also sync the bl3 files of the non-default versions with python25
for consistency
(Changes that can break existing programs are marked with a "*" )
Language features:
- Addition of lazy patterns: "lazy <pat>" matches suspensions whose values,
after forcing, match the pattern <pat>.
- Introduction of private abbreviation types "type t = private <type-expr>",
for abstracting the actual manifest type in type abbreviations.
- Subtyping is now allowed between a private abbreviation and its definition,
and between a polymorphic method and its monomorphic instance.
Compilers:
- The file name for a compilation unit should correspond to a valid
identifier (Otherwise dynamic linking and other things can fail, and
a warning is emitted.)
* Revised -output-obj: the output name must now be provided; its
extension must be one of .o/.obj, .so/.dll, or .c for the
bytecode compiler. The compilers can now produce a shared library
(with all the needed -ccopts/-ccobjs options) directly.
- -dtypes renamed to -annot, records (in .annot files) which function calls
are tail calls.
- All compiler error messages now include a file name and location, for
better interaction with Emacs' compilation mode.
- Optimized compilation of "lazy e" when the argument "e" is
already evaluated.
- Optimized compilation of equality tests with a variant constant constructor.
- The -dllib options recorded in libraries are no longer ignored when
-use_runtime or -use_prims is used (unless -no_auto_link is
explicitly used).
- Check that at most one of -pack, -a, -shared, -c, -output-obj is
given on the command line.
- Optimized compilation of private types as regular manifest types
(e.g. abbreviation to float, float array or record types with only
float fields).
Native-code compiler:
- New port: Mac OS X / Intel in 64-bit mode (configure with -cc "gcc -m64").
- A new option "-shared" to produce a plugin that can be dynamically
loaded with the native version of Dynlink.
- A new option "-nodynlink" to enable optimizations valid only for code
that is never dynlinked (no-op except for AMD64).
- More aggressive unboxing of floats and boxed integers.
- Can select which assembler and asm options to use at configuration time.
Run-time system:
- New implementation of the page table describing the heap (two-level
array in 32 bits, sparse hashtable in 64 bits), fixes issues with address
space randomization on 64-bit OS (PR#4448).
- New "generational" API for registering global memory roots with the GC,
enables faster scanning of global roots.
(The functions are caml_*_generational_global_root in <caml/memory.h>.)
- New function "caml_raise_with_args" to raise an exception with several
arguments from C.
- Changes in implementation of dynamic linking of C code:
under Win32, use Alain Frisch's flexdll implementation of the dlopen
API; under MacOSX, use dlopen API instead of MacOSX bundle API.
- Programs may now choose a first-fit allocation policy instead of
the default next-fit. First-fit reduces fragmentation but is
slightly slower in some cases.
Standard library:
- Parsing library: new function "set_trace" to programmatically turn
on or off the printing of a trace during parsing.
- Printexc library: new functions "print_backtrace" and "get_backtrace"
to obtain a stack backtrace of the most recently raised exception.
New function "record_backtrace" to turn the exception backtrace mechanism
on or off from within a program.
- Scanf library: fine-tuning of meta format implementation;
fscanf behaviour revisited: only one input buffer is allocated for any
given input channel;
the %n conversion does not count a lookahead character as read.
Other libraries:
- Dynlink: on some platforms, the Dynlink library is now available in
native code. The boolean Dynlink.is_native allows the program to
know whether it has been compiled in bytecode or in native code.
- Bigarrays: added "unsafe_get" and "unsafe_set"
(non-bound-checking versions of "get" and "set").
- Bigarrays: removed limitation "array dimension < 2^31".
- Labltk: added support for TK 8.5.
- Num: added conversions between big_int and int32, nativeint, int64.
More efficient implementation of Num.quo_num and Num.mod_num.
- Threads: improved efficiency of mutex and condition variable operations;
improved interaction with Unix.fork (PR#4577).
- Unix: added getsockopt_error returning type Unix.error.
Added support for TCP_NODELAY and IPV6_ONLY socket options.
- Win32 Unix: "select" now supports all kinds of file descriptors.
Improved emulation of "lockf" (PR#4609).
Tools:
- ocamldebug now supported under Windows (MSVC and Mingw ports),
but without the replay feature. (Contributed by Dmitry Bely
and Sylvain Le Gall at OCamlCore with support from Lexifi.)
- ocamldoc: new option -no-module-constraint-filter to include functions
hidden by signature constraint in documentation.
- ocamlmklib and ocamldep.opt now available under Windows ports.
- ocamlmklib no longer supports the -implib option.
- ocamlnat: an experimental native toplevel (not built by default).
Camlp4:
* programs linked with camlp4lib.cma now also need dynlink.cma.
the exported libraries
(according to the CVS log, this was only to work around spurious db4
dependencies which are hopefully fixed by my last change to db4/bl3)
Changes from V8.1 to V8.2
=========================
Language
- If a fixpoint is not written with an explicit { struct ... }, then
all arguments are tried successively (from left to right) until one is
found that satisfies the structural decreasing condition.
- New experimental typeclass system giving ad-hoc polymorphism and
overloading based on dependent records and implicit arguments.
- New syntax "let 'pat := b in c" for let-binding using irrefutable patterns.
- New syntax "forall {A}, T" for specifying maximally inserted implicit
arguments in terms.
- Sort of Record/Structure, Inductive and CoInductive defaults to Type
if omitted.
- Support for optional "where" notation clauses for record fields.
- (Co)Inductive types can be defined as records
(e.g. "CoInductive stream := { hd : nat; tl : stream }.")
- New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
statements.
- Support for sort-polymorphism on constants denoting inductive types.
- Several evolutions of the module system (handling of module aliases,
functorial module types, an Include feature, etc).
- Prop now a subtype of Set (predicative and impredicative forms).
- Recursive inductive types in Prop with a single constructor of which
all arguments are in Prop is now considered to be a singleton
type. It consequently supports all eliminations to Prop, Set and Type.
As a consequence, Acc_rect has now a more direct proof [possible source
of easily fixed incompatibility in case of manual definition of a recursor
in a recursive singleton inductive type].
- New syntax to do implicit generalization in binders and inside terms.
- New tentative syntax for introduction of record objects without mentioning
the constructor {| field := body; ... |}, turning missing fields into holes
(compatible with refine and Program).
Vernacular commands
- Added option Global to "Arguments Scope" for section surviving.
- Added option "Unset Elimination Schemes" to deactivate the automatic
generation of elimination schemes.
- Modification of the Scheme command so you can ask for the name to be
automatically computed (e.g. Scheme Induction for nat Sort Set).
- New command "Combined Scheme" to build combined mutual induction
principles from existing mutual induction principles.
- New command "Scheme Equality" to build a decidable (boolean) equality
for simple inductive datatypes and a decision property over this equality
(e.g. Scheme Equality for nat).
- Added option "Set Equality Scheme" to make automatic the declaration
of the boolean equality when possible.
- Source of universe inconsistencies now printed when option
"Set Printing Universes" is activated.
- New option "Set Printing Existential Instances" for making the display of
existential variable instances explicit.
- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the
"compute"/"cbv" reduction strategy, respectively meaning reduce only, or
everything but, the constants id1 ... idn. "lazy" alone or followed by
"[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply
all of beta-iota-zeta-delta, possibly restricting delta.
- New command "Strategy" to control the expansion of constants during
conversion tests. It generalizes commands Opaque and Transparent by
introducing a range of levels. Lower levels are assigned to constants
that should be expanded first.
- New options Global and Local to Opaque and Transparent.
- New command "Print Assumptions" to display all variables, parameters
or axioms a theorem or definition relies on.
- "Add Rec LoadPath" now provides references to libraries using partially
qualified names (this holds also for coqtop/coqc option -R).
- SearchAbout supports negated search criteria, reference to logical objects
by their notation, and more generally search of subterms.
- "Declare ML Module" now allows to import .cmxs files when Coq is
compiled in native code with a version of OCaml that supports native
Dynlink (>= 3.11).
- New command "Create HintDb name [discriminated]" to explicitely declare
a new hint database and optionaly turn on a discrimination net
implementation to index all the lemmas in the database.
- New commands "Hint Transparent" and "Hint Opaque" to set the unfolding
status of definitions used by auto. This information is taken into account
by the discrimination net and the unification algorithm.
- "Hint Extern" now takes an optional pattern and applies the given tactic
all the time if no pattern is given.
- Specific sort constraints on Record now taken into account.
- "Print LoadPath" supports a path argument to filter the display.
Libraries
- Several parts of the libraries are now in Type, in particular FSets,
SetoidList, ListSet, Sorting, Zmisc. This may induce a few
incompatibilities. In case of trouble while fixing existing development,
it may help to simply declare Set as an alias for Type (see file
SetIsType).
- New arithmetical library in theories/Numbers. It contains:
* an abstract modular development of natural and integer arithmetics
in Numbers/Natural/Abstract and Numbers/Integer/Abstract
* an implementation of efficient computational bounded and unbounded
integers that can be mapped to processor native arithmetics.
See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN
for unbounded natural numbers and Numbers/Integer/BigZ for unbounded
integers.
* some proofs that both older libraries Arith, ZArith and NArith and
newer BigN and BigZ implement the abstract modular development.
This allows in particular BigN and BigZ to already come with a
large database of basic lemmas and some generic tactics (ring),
This library has still an experimental status, as well as the
processor-acceleration mechanism, but both its abstract and its
concrete parts are already quite usable and could challenge the use
of nat, N and Z in actual developments. Moreover, an extension of
this framework to rational numbers is ongoing, and an efficient
Q structure is already provided (see Numbers/Rational/BigQ), but
this part is currently incomplete (no abstract layer and generic
lemmas).
- Many changes in FSets/FMaps. In practice, compatibility with earlier
version should be fairly good, but some adaptations may be required.
* Interfaces of unordered ("weak") and ordered sets have been factorized
thanks to new features of Coq modules (in particular Include), see
FSetInterface. Same for maps. Hints in these interfaces have been
reworked (they are now placed in a "set" database).
* To allow full subtyping between weak and ordered sets, a field
"eq_dec" has been added to OrderedType. The old version of OrderedType
is now called MiniOrderedType and functor MOT_to_OT allow to
convert to the new version. The interfaces and implementations
of sets now contain also such a "eq_dec" field.
* FSetDecide, contributed by Aaron Bohannon, contains a decision
procedure allowing to solve basic set-related goals (for instance,
is a point in a particular set ?). See FSetProperties for examples.
* Functors of properties have been improved, especially the ones about
maps, that now propose some induction principles. Some properties
of fold need less hypothesis.
* More uniformity in implementations of sets and maps: they all use
implicit arguments, and no longer export unnecessary scopes (see
bug #1347)
* Internal parts of the implementations based on AVL have evolved a
lot. The main files FSetAVL and FMapAVL are now much more
lightweight now. In particular, minor changes in some functions
has allowed to fully separate the proofs of operational
correctness from the proofs of well-balancing: well-balancing is
critical for efficiency, but not anymore for proving that these
trees implement our interfaces, hence we have moved these proofs
into appendix files FSetFullAVL and FMapFullAVL. Moreover, a few
functions like union and compare have been modified in order to be
structural yet efficient. The appendix files also contains
alternative versions of these few functions, much closer to the
initial Ocaml code and written via the Function framework.
- Library IntMap, subsumed by FSets/FMaps, has been removed from
Coq Standard Library and moved into a user contribution Cachan/IntMap
- Better computational behavior of some constants (eq_nat_dec and
le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
transparent, ...) (exceptional source of incompatibilities).
- Boolean operators moved from module Bool to module Datatypes (may need
to rename qualified references in script and force notations || and &&
to be at levels 50 and 40 respectively).
- The constructors xI and xO of type positive now have postfix notations
"~1" and "~0", allowing to write numbers in binary form easily, for instance
6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v).
- Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular
a better power function).
- Changes in ZArith: several additional lemmas (used in theories/Numbers),
especially in Zdiv, Znumtheory, Zpower. Moreover, many results in
Zdiv have been generalized: the divisor may simply be non-null
instead of strictly positive (see lemmas with name ending by
"_full"). An alternative file ZOdiv proposes a different behavior
(the one of Ocaml) when dividing by negative numbers.
- Changes in Arith: EqNat and Wf_nat now exported from Arith, some
constructions on nat that were outside Arith are now in (e.g. iter_nat).
- In SetoidList, eqlistA now expresses that two lists have similar elements
at the same position, while the predicate previously called eqlistA
is now equivlistA (this one only states that the lists contain the same
elements, nothing more).
- Changes in Reals:
* Most statement in "sigT" (including the
completeness axiom) are now in "sig" (in case of incompatibility,
use proj1_sig instead of projT1, sig instead of sigT, etc).
* More uniform naming scheme (identifiers in French moved to English,
consistent use of 0 -- zero -- instead of O -- letter O --, etc).
* Lemma on prod_f_SO is now on prod_f_R0.
* Useless hypothesis of ln_exists1 dropped.
* New Rlogic.v states a few logical properties about R axioms.
* RIneq.v extended and made cleaner.
- Slight restructuration of the Logic library regarding choice and classical
logic. Addition of files providing intuitionistic axiomatizations of
descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
- Definition of pred and minus made compatible with the structural
decreasing criterion for use in fixpoints.
- Files Relations/Rstar.v and Relations/Newman.v moved out to the user
contribution repository (contribution CoC_History). New lemmas about
transitive closure added and some bound variables renamed (exceptional
risk of incompatibilities).
Notations, coercions, implicit arguments and type inference
- More automation in the inference of the return clause of dependent
pattern-matching problems.
- Experimental allowance for omission of the clauses easily detectable as
impossible in pattern-matching problems.
- Improved inference of implicit arguments, now working inside record
declarations.
- New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
Defensive" for controlling inference and use of implicit arguments.
- New modifier in "Implicit Arguments" to force an implicit argument to
be maximally inserted.
- New options Global and Local to "Implicit Arguments" for section
surviving or non export outside module.
- Level "constr" moved from 9 to 8.
- Structure/Record now printed as Record (unless option Printing All is set).
- Support for parametric notations defining constants.
- Insertion of coercions below product types refrains to unfold
constants (possible source of incompatibility).
- New support for fix/cofix in notations.
Tactic Language
- Second-order pattern-matching now working in Ltac "match" clauses
(syntax for second-order unification variable is "@?X").
- Support for matching on let bindings in match context using syntax
"H := body" or "H := body : type".
- (?X ?Y) patterns now match any application instead of only unary
applications (possible source of incompatibility).
- Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer).
- The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]"
is extended so that at most one expr_i may have the form "expr .."
or just "..". Also, n can be different from the number of subgoals
generated by expr_0. In this case, the value of expr (or idtac in
case of just "..") is applied to the intermediate subgoals to make
the number of tactics equal to the number of subgoals.
- A name used as the name of the parameter of a lemma (like f in
"apply f_equal with (f:=t)") is now interpreted as a ltac variable
if such a variable exists (this is a possible source of
incompatibility and it can be fixed by renaming the variables of a
ltac function into names that do not clash with the lemmas
parameter names used in the tactic).
- New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
- "let rec ... in ... " now supported for expressions without explicit
parameters; interpretation is lazy to the contrary of "let ... in ...";
hence, the "rec" keyword can be used to turn the argument of a
"let ... in ..." into a lazy one.
- Patterns for hypotheses types in "match goal" are now interpreted in
type_scope.
- A bound variable whose name is not used elsewhere now serves as
metavariable in "match" and it gets instantiated by an identifier
(allow e.g. to extract the name of a statement like "exists x, P x").
- New printing of Ltac call trace for better debugging.
- The C-zar (formerly know as declarative) proof language is now properly
documented.
Tactics
- New tactics "apply -> term", "apply <- term", "apply -> term in
ident", "apply <- term in ident" for applying equivalences (iff).
- "apply" and "rewrite" now take open terms (terms with undefined existentials)
as input.
- Slight improvement of the hnf and simpl tactics when applied on
expressions with explicit occurrences of match or fix.
- New tactics "eapply in", "erewrite", "erewrite in".
- New tactics "ediscriminate", "einjection", "esimplify_eq".
- Tactics "discriminate", "injection", "simplify_eq" now support any
term as argument. Clause "with" is also supported.
- Unfoldable references can be given by notation's string rather than by name
in unfold.
- The "with" arguments are now typed using informations from the current goal:
allows support for coercions and more inference of implicit arguments.
- Application of "f_equal"-style lemmas works better.
- Tactics elim, case, destruct and induction now support variants eelim,
ecase, edestruct and einduction.
- Tactics destruct and induction now support the "with" option and the
"in" clause option. If the option "in" is used, an equality is added
to remember the term to which the induction or case analysis applied
(possible source of parsing incompatibilities when destruct or induction is
part of a let-in expression in Ltac; extra parentheses are then required).
- New support for "as" clause in tactics "apply in" and "eapply in".
- Some new intro patterns:
* intro pattern "?A" genererates a fresh name based on A.
Caveat about a slight loss of compatibility:
Some intro patterns don't need space between them. In particular
intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
is still legal but equivalent to intros ?a ?b.
* intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
for right-associative constructs like /\ or exists.
- Several syntax extensions concerning "rewrite":
* "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites
occur only on the first subgoal: in particular, side-conditions of the
"rewrite A" are not concerned by the "rewrite B,C".
* "rewrite A by tac" allows to apply tac on all side-conditions generated by
the "rewrite A".
* "rewrite A at n" allows to select occurrences to rewrite: rewrite only
happen at the n-th exact occurrence of the first successful matching of
A in the goal.
* "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A".
* "rewrite !A" means rewriting A as long as possible (and at least once).
* "rewrite 3?A" means rewriting A at most three times.
* "rewrite ?A" means rewriting A as long as possible (possibly never).
* many of the above extensions can be combined with each other.
- Introduction patterns better respect the structure of context in presence of
missing or extra names in nested disjunction-conjunction patterns [possible
source of rare incompatibilities].
- New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
- New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]"
to do induction-inversion on instantiated inductive families ? la BasicElim.
- Tactics "apply" and "apply in" now able to reason modulo unfolding of
constants (possible source of incompatibility in situations where apply
may fail, e.g. as argument of a try or a repeat and in a ltac function);
versions that do not unfold are renamed into "simple apply" and
"simple apply in" (usable for compatibility or for automation).
- Tactics "apply" and "apply in" now able to traverse conjunctions and to
select the first matching lemma among the components of the conjunction;
tactic "apply" also able to apply lemmas of conclusion an empty type.
- Tactic "apply" now supports application of several lemmas in a row.
- Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
- New tactic "instantiate" (without argument).
- Tactic firstorder "with" and "using" options have their meaning swapped for
consistency with auto/eauto (source of incompatibility).
- Tactic "generalize" now supports "at" options to specify occurrences
and "as" options to name the quantified hypotheses.
- New tactic "specialize H with a" or "specialize (H a)" allows to transform
in-place a universally-quantified hypothesis (H : forall x, T x) into its
instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
versions of Coq, but was undocumented, and had a slightly different behavior.
- New tactic "contradict H" can be used to solve any kind of goal as long as
the user can provide afterwards a proof of the negation of the hypothesis H.
If H is already a negation, say ~T, then a proof of T is asked.
If the current goal is a negation, say ~U, then U is saved in H afterwards,
hence this new tactic "contradict" extends earlier tactic "swap", which is
now obsolete.
- Tactics f_equal is now done in ML instead of Ltac: it now works on any
equality of functions, regardless of the arity of the function.
- New options "before id", "at top", "at bottom" for tactics "move"/"intro".
- Some more debug of reflexive omega (romega), and internal clarifications.
Moreover, romega now has a variant "romega with *" that can be also used
on non-Z goals (nat, N, positive) via a call to a translation tactic named
zify (its purpose is to Z-ify your goal...). This zify may also be used
independantly of romega.
- Tactic "remember" now supports an "in" clause to remember only selected
occurrences of a term.
- Tactic "pose proof" supports name overwriting in case of specialization of an
hypothesis.
- Semi-decision tactic "jp" for first-order intuitionistic logic moved to user
contributions (subsumed by "firstorder").
Program
- Moved useful tactics in theories/Program and documented them.
- Add Program.Basics which contains standard definitions for functional
programming (id, apply, flip...)
- More robust obligation handling, dependent pattern-matching and
well-founded definitions.
- Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer
which argument decreases structurally.
- Program Lemma, Axiom etc... now permit to have obligations in the statement
iff they can be automatically solved by the default tactic.
- Renamed "Obligations Tactic" command to "Obligation Tactic".
- New command "Preterm [ of id ]" to see the actual term fed to Coq for
debugging purposes.
- New option "Transparent Obligations" to control the declaration of
obligations as transparent or opaque. All obligations are now transparent
by default, otherwise the system declares them opaque if possible.
- Changed the notations "left" and "right" to "in_left" and "in_right" to hide
the proofs in standard disjunctions, to avoid breaking existing scripts when
importing Program. Also, put them in program_scope.
Type Classes
- New "Class", "Instance" and "Program Instance" commands to define
classes and instances documented in the reference manual.
- New binding construct "`{Class_1 param_1 .. param_n, Class_2 ...}"
for binding type classes, usable everywhere.
- New command " Print Classes " and " Print Instances some_class " to
print tables for typeclasses.
- New default eauto hint database "typeclass_instances" used by the default
typeclass instance search tactic.
- New theories directory "theories/Classes" for standard typeclasses
declarations. Module Classes.RelationClasses is a typeclass port of
Relation_Definitions plus a generic development of algebra on
n-ary heterogeneous predicates.
Setoid rewriting
- Complete (and still experimental) rewrite of the tactic
based on typeclasses. The old interface and semantics are
almost entirely respected, except:
- Import Setoid is now mandatory to be able to call setoid_replace
and declare morphisms.
- "-->", "++>" and "==>" are now right associative notations
declared at level 55 in scope signature_scope.
Their introduction may break existing scripts that defined
them as notations with different levels.
- One can use [Typeclasses Opaque/Transparent [cst]] to indicate
that [cst] should not be unfolded during unification for morphism
resolution, by default all constants are transparent.
- The [setoid_rewrite]'s semantics change when rewriting with
a lemma: it can rewrite two different instantiations of the lemma
at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics.
[setoid_rewrite] will also try to rewrite under binders now, and can
succeed on different terms than before. In particular, it will unify under
let-bound variables. When called through [rewrite], the semantics are
unchanged though.
- [Add Morphism term : id] has different semantics when used with
parametric morphism: it will try to find a relation on the parameters
too. The behavior has also changed with respect to default relations:
the most recently declared Setoid/Relation will be used, the documentation
explains how to customize this behavior.
- Parametric Relation and Morphism are declared differently, using the
new [Add Parametric] commands, documented in the manual.
- Setoid_Theory is now an alias to Equivalence, scripts building objects
of type Setoid_Theory need to unfold (or [red]) the definitions
of Reflexive, Symmetric and Transitive in order to get the same goals
as before. Scripts which introduced variables explicitely will not break.
- The order of subgoals when doing [setoid_rewrite] with side-conditions
is now always the same: first the new goal, then the conditions.
- New standard library modules Classes.Morphisms declares
standard morphisms on refl/sym/trans relations.
Classes.Morphisms_Prop declares morphisms on propositional
connectives and Classes.Morphisms_Relations on generalized predicate
connectives. Classes.Equivalence declares notations and tactics
related to equivalences and Classes.SetoidTactics defines the
setoid_replace tactics and some support for the "Add *" interface,
notably the tactic applied automatically before each "Add Morphism"
proof.
- User-defined subrelations are supported, as well as higher-order morphisms
and rewriting under binders. The tactic is also extensible entirely in Ltac.
The documentation has been updated to cover these features.
- [setoid_rewrite] and [rewrite] now support the [at] modifier to select
occurrences to rewrite, and both use the [setoid_rewrite] code, even when
rewriting with leibniz equality if occurrences are specified.
Extraction
- Improved behavior of the Caml extraction of modules: name clashes should
not happen anymore.
- The command Extract Inductive has now a syntax for infix notations. This
allows in particular to map Coq lists and pairs onto Caml ones:
Extract Inductive list => list [ "[]" "(::)" ].
Extract Inductive prod => "(*)" [ "(,)" ].
- In pattern matchings, a default pattern "| _ -> ..." is now used whenever
possible if several branches are identical. For instance, functions
corresponding to decidability of equalities are now linear instead of
quadratic.
- A new instruction Extraction Blacklist id1 .. idn allows to prevent filename
conflits with existing code, for instance when extracting module List
to Ocaml.
CoqIDE
- CoqIDE font defaults to monospace so as indentation to be meaningful.
- CoqIDE supports nested goals and any other kind of declaration in the middle
of a proof.
- Undoing non-tactic commands in CoqIDE works faster.
- New CoqIDE menu for activating display of various implicit informations.
- Added the possibility to choose the location of tabs in coqide:
(in Edit->Preferences->Misc)
- New Open and Save As dialogs in CoqIDE which filter *.v files.
Tools
- New stand-alone .vo files verifier "coqchk".
- Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
- New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
- The binary "parser" has been renamed to "coq-parser".
coqdoc
- Improved coqdoc and dump of globalization information to give more
meta-information on identifiers. All categories of Coq definitions are
supported, which makes typesetting trivial in the generated documentation.
- A "--interpolate" option permits to use typesetting information from the
typechecked part of the file to typeset identifiers appearing in Coq escapings
inside the documentation.
- Better handling of utf8 ("--utf8" option) and respect of spaces in the source.
- Support for hyperlinking and indexing developments in the TeX output.
- New option "color" of the coqdoc style file to render identifiers using colors.
- Additional macros in the TeX ouput allowing to customize indentation and size of
empty lines. New environment "coqdoccode" for Coq code.
Miscellaneous
- Coq installation provides enough files so that Ocaml's extensions need not
the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
- New commands "Set Whelp Server" and "Set Whelp Getter" to customize the
Whelp search tool.
- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
"Test Printing Let for ref" and "Test Printing If for ref".
- An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
- Add -browser option to configure script.
- Build a shared library for the C part of Coq, and use it by default on
non-(Windows or MacOS) systems. Bytecode executables are now pure. The
behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and
-custom configure options.
- Complexity tests can be skipped by setting the environment variable
COQTEST_SKIPCOMPLEXITY.
Changes are:
- compatibility with recent versions of ocaml
- possible use of IFDEF and IFNDEF in record labels declarations
- addition of Plexer.utf8_lexing
Mono 2.4.2.3 is a bug fix release for Mono 2.4, which is the foundation
for Novell's own long-term support Mono-based product.
This release includes the following bug fixes from 2.4.2.2:
* 502016 (https://bugzilla.novell.com/show_bug.cgi?id=502016) - Simple
precompiled MVC app does not run on Mono 2.4.2
* 524726 (https://bugzilla.novell.com/show_bug.cgi?id=524726) -
Precompiling for / then deploying elsewhere causes failure for ASP.NET
apps.
Changes in Mono 2.4.2.3
XSP now has Silverlight mime types registered.
Updated the browser database.
The C# Shell (csharp) will now accept C# scripts specified on the command
line, like:
$ csharp demo.cs
A major bug was fixed for multi-threaded applications using XPath, if you
are using XPath in a multithreaded application, we strongly recommend that
you upgrade to this version.
Pkgsrc changes:
o Add patch-af and patch-ag so that the math library variant selection
actually works as intended.
Upstream changes:
- Core
+ Removed several deprecated functions and features
+ Removed bsr, jsr, branch_cs, and ret opcodes
+ Removed global stacks system
+ Changed OPS file format to include explicit preamble
+ Changed all "new 'Iterator'" instructions into 'iter' instructions
+ Removed Configure.pl options for specifying non-working GC cores
+ Removed unexecuting code as found by Coverity
+ Improvements to the Parrot Debugger
+ Added experimental fixed-size structure allocator to the GC
+ Added experimental lazy arena allocation to the GC
+ Removed the defunct PASM1 compiler object
+ Refactored hashes, keys, and iterators
+ Added "corevm" make target to build Parrot without all the
supporting libraries
+ Removed Random PMC type and added in a "rand" dynop
+ Optimization and Improvements to the NCI thunk generator
+ New include file libpaths.pasm
- Compilers
+ Multiple .local with same name and different type is now an
error on IMCC.
- Platforms
+ Improved support for detecting Fink and Macports
+ Updated search directories for libraries
- Documentation
+ "Parrot Developers Guide: PIR" released to publisher and
available to purchase
+ Improved documentation about Parrot Debugger
+ Update PGE Documentation
- Miscellaneous
+ Added tests
+ Fixes to code, documentation, and standards
Changes in 1.6.0_16 (6u16)
6u16 contains Olson time zone data version 2009i.
Bug Fixes
6862295 hotspot jvmti JDWP threadid changes during debugging session (leading to ignored breakpoints)
Changes in 1.6.0_15 (6u15)
Root Certificates
Root Certificates are included in this release.
* Added one new root certificate and removed 3 root certificates from Entrust. (Refer to 6805338.)
* Added three new root certificates from Keynectis. (Refer to 6845457.)
* Added three new root certificates from Quovadis. (Refer to 6846473.)
Blacklist Entries
This update release includes the following new entry to the Blacklist:
* JNLPAppletLauncher (See Sun Alert 263490 .)
Note: Users should install JDK and JRE 6 Update 15 or later on systems running JDK and JRE 5.0 and SDK and JRE 1.4.2 to take advantage of this blacklist feature. For more information see the Blacklist Jar Feature section in the 6u14 Release Notes.
Debug Issue
Java ™ Virtual Machine Tool Interface (JVM TI) breakpoints are reliable only when either the Parallel Scavenge garbage collector (-XX:+UseParallelGC) or the Parallel Compacting garbage collector (-XX:+UseParallelOldGC) is used.
When other collectors are used, breakpoints may stop functioning, and JVM TI object tags may become unusable after a full GC operation is performed. Java ™ Debug Interface (JDI) ThreadReferences have an embedded thread ID that depends on JVM TI object tags, thus the embedded thread ID may change unexpectedly. This may cause confusion in thread based JDI events.
Note that the Serial garbage collector (-XX:+UseSerialGC) is vulnerable to this problem and is selected by default on some platforms. The work around is to explicitly select the Parallel Scavenge collector using the command line option -XX:+UseParallelGC.
(Refer to 6862295.)
Bug Fixes
This release contains fixes for one or more security vulnerabilities. For more information, please see Sun Alerts 263408 , 263409 , 263428 , 263429 , 263488 , 263489 , and 264648.
Bug fixes for vulnerabilities are listed in the following table.
BugId Category Subcategory Description 6656610 java accessibility AccessibleResourceBundle.getContents exposes mutable static (findbugs)
6656586 java classes_awt Cursor.predefined is protected static mutable (findbugs)
6805231 java classes_awt Security Warning Icon is missing in Windows 2000 Prof from Jdk build 6u12
6818787 java classes_awt It is possible to reposition the security icon too far from the border of the window on X11
6823373 java classes_awt [ZDI-CAN-460] Java Web Start JPEG header parsing needs more scruity
6660539 java classes_beans Introspector cache mutable static
6777487 java classes_beans Encoder allows reading private variables with certain names
6801071 java classes_net Remote sites can compromise user privacy and possibly hijack web session
6801497 java classes_net Proxy is assumed to be immutable but is non-final
6657695 java classes_security AbstractSaslImpl.logger is a static mutable (findbugs)
6824440 java classes_security XML Signature HMAC issue
6657625 java classes_sound RmfFileReader/StandardMidiFileWriter.types are public mutable statics (findbugs)
6738524 java classes_sound JDK13Services allows read access to system properties from untrusted code
6777448 java classes_sound JDK13Services.getProviders creates instances with full privileges
6588003 java classes_swing LayoutQueue mutable statics
6660049 java classes_swing Synth Region.uiToRegionMap/lowerCaseNameMap are mutable statics
6849518 java classes_swing NPE is thrown in jemmy library since 6u15 b01 at javax.swing.plaf.synth.SynthContext.isSubregion()
6656625 java imageio ImageReaderSpi.STANDARD_INPUT_TYPE/ImageWriterSpi.STANDARD_OUTPUT_TYPE are mutable static (findbugs)
6657133 java imageio Mutable statics in imageio plugins (findbugs)
6830335 java jar Java JAR Pack200 Decompression Integer Overflow Vulnerability
6755840 java_plugin plugin Version selection allows old zip and certificate handling to be exploited
6848964 javawebstart general TCK jnlp test jnlp_file/appletDesc/index.html#misc fails with NPE starting 6u15 b01
6862844 javawebstart other java web start ActiveX control security problem caused by ATL PROP_ENTRY macro
6845701 jaxp parse Xerces2 Java XML library infinite loop with malformed XML input
6813167 jax-ws other 6u14 JAX-WS audit mutable static bugs
6736293 jmx classes OpenType checks can be bypassed through finalizer resurrection
6657619 jndi dns DnsContext.debug is public static mutable (findbugs)
Other bug fixes are listed in the following table.
BugId Category Subcategory Description 6786503 hotspot garbage_collector Overflow list performance can be improved
6787254 hotspot garbage_collector Work queue capacity can be increased substantially on some platforms
6805338 java classes_security Add 1 new Entrust root CA cert and remove 3 others with 1024 bit keys
6845457 java classes_security Add root certs for Keynectis CA
6846473 java classes_security Add QuoVadis root CA certs to the JRE
6848984 java classes_util_i18n (tz) Support tzdata2009i
6851214 java classes_util_i18n (tz) New Jordan rule creates a failure for SimpleTimeZone parsing post tzdata2009h
6845077 java install silent JDK should install JRE/Java DB silently
6846531 javawebstart other REGRESSION application from ocie.net does not work with 6.0_14
6461727 jce pkcs11_csp TripleDES KeyGenerators in SunPKCS11 and SunJCE do not agree on key length
Changes in 1.6.0_16 (6u16)
6u16 contains Olson time zone data version 2009i.
Bug Fixes
6862295 hotspot jvmti JDWP threadid changes during debugging session (leading to ignored breakpoints)
Changes in 1.6.0_15 (6u15)
Root Certificates
Root Certificates are included in this release.
* Added one new root certificate and removed 3 root certificates from Entrust. (Refer to 6805338.)
* Added three new root certificates from Keynectis. (Refer to 6845457.)
* Added three new root certificates from Quovadis. (Refer to 6846473.)
Blacklist Entries
This update release includes the following new entry to the Blacklist:
* JNLPAppletLauncher (See Sun Alert 263490 .)
Note: Users should install JDK and JRE 6 Update 15 or later on systems running JDK and JRE 5.0 and SDK and JRE 1.4.2 to take advantage of this blacklist feature. For more information see the Blacklist Jar Feature section in the 6u14 Release Notes.
Debug Issue
Java ™ Virtual Machine Tool Interface (JVM TI) breakpoints are reliable only when either the Parallel Scavenge garbage collector (-XX:+UseParallelGC) or the Parallel Compacting garbage collector (-XX:+UseParallelOldGC) is used.
When other collectors are used, breakpoints may stop functioning, and JVM TI object tags may become unusable after a full GC operation is performed. Java ™ Debug Interface (JDI) ThreadReferences have an embedded thread ID that depends on JVM TI object tags, thus the embedded thread ID may change unexpectedly. This may cause confusion in thread based JDI events.
Note that the Serial garbage collector (-XX:+UseSerialGC) is vulnerable to this problem and is selected by default on some platforms. The work around is to explicitly select the Parallel Scavenge collector using the command line option -XX:+UseParallelGC.
(Refer to 6862295.)
Bug Fixes
This release contains fixes for one or more security vulnerabilities. For more information, please see Sun Alerts 263408 , 263409 , 263428 , 263429 , 263488 , 263489 , and 264648.
Bug fixes for vulnerabilities are listed in the following table.
BugId Category Subcategory Description 6656610 java accessibility AccessibleResourceBundle.getContents exposes mutable static (findbugs)
6656586 java classes_awt Cursor.predefined is protected static mutable (findbugs)
6805231 java classes_awt Security Warning Icon is missing in Windows 2000 Prof from Jdk build 6u12
6818787 java classes_awt It is possible to reposition the security icon too far from the border of the window on X11
6823373 java classes_awt [ZDI-CAN-460] Java Web Start JPEG header parsing needs more scruity
6660539 java classes_beans Introspector cache mutable static
6777487 java classes_beans Encoder allows reading private variables with certain names
6801071 java classes_net Remote sites can compromise user privacy and possibly hijack web session
6801497 java classes_net Proxy is assumed to be immutable but is non-final
6657695 java classes_security AbstractSaslImpl.logger is a static mutable (findbugs)
6824440 java classes_security XML Signature HMAC issue
6657625 java classes_sound RmfFileReader/StandardMidiFileWriter.types are public mutable statics (findbugs)
6738524 java classes_sound JDK13Services allows read access to system properties from untrusted code
6777448 java classes_sound JDK13Services.getProviders creates instances with full privileges
6588003 java classes_swing LayoutQueue mutable statics
6660049 java classes_swing Synth Region.uiToRegionMap/lowerCaseNameMap are mutable statics
6849518 java classes_swing NPE is thrown in jemmy library since 6u15 b01 at javax.swing.plaf.synth.SynthContext.isSubregion()
6656625 java imageio ImageReaderSpi.STANDARD_INPUT_TYPE/ImageWriterSpi.STANDARD_OUTPUT_TYPE are mutable static (findbugs)
6657133 java imageio Mutable statics in imageio plugins (findbugs)
6830335 java jar Java JAR Pack200 Decompression Integer Overflow Vulnerability
6755840 java_plugin plugin Version selection allows old zip and certificate handling to be exploited
6848964 javawebstart general TCK jnlp test jnlp_file/appletDesc/index.html#misc fails with NPE starting 6u15 b01
6862844 javawebstart other java web start ActiveX control security problem caused by ATL PROP_ENTRY macro
6845701 jaxp parse Xerces2 Java XML library infinite loop with malformed XML input
6813167 jax-ws other 6u14 JAX-WS audit mutable static bugs
6736293 jmx classes OpenType checks can be bypassed through finalizer resurrection
6657619 jndi dns DnsContext.debug is public static mutable (findbugs)
Other bug fixes are listed in the following table.
BugId Category Subcategory Description 6786503 hotspot garbage_collector Overflow list performance can be improved
6787254 hotspot garbage_collector Work queue capacity can be increased substantially on some platforms
6805338 java classes_security Add 1 new Entrust root CA cert and remove 3 others with 1024 bit keys
6845457 java classes_security Add root certs for Keynectis CA
6846473 java classes_security Add QuoVadis root CA certs to the JRE
6848984 java classes_util_i18n (tz) Support tzdata2009i
6851214 java classes_util_i18n (tz) New Jordan rule creates a failure for SimpleTimeZone parsing post tzdata2009h
6845077 java install silent JDK should install JRE/Java DB silently
6846531 javawebstart other REGRESSION application from ocie.net does not work with 6.0_14
6461727 jce pkcs11_csp TripleDES KeyGenerators in SunPKCS11 and SunJCE do not agree on key length
Changes in 1.5.0_20
The full internal version number for this update release is 1.5.0_20-b02 (where
"b" means "build"). The external version number is 5.0u20.
OlsonData 2009i
This release contains Olson time zone data version 2009i. For more information,
refer to Timezone Data Versions in the JRE Software .
Security Baseline
This update release specifies the following security baseline:
JRE Family Version Java SE
Security Baseline Java SE for Business
Security Baseline 1.4.2 1.4.2_19 1.4.2_22
In December, 2008, Java SE 1.4.2 reached its end of service life with the
release of 1.4.2_19. Future revisions of Java SE 1.4.2 (1.4.2_20 and above)
include the Access Only option and are available to Java SE for Business
subscribers.
For more information about the security baseline, see Deploying Java Applets
With Family JRE Versions in Java Plug-in for Internet Explorer .
Root Certificates
Root Certificates are included in this release.
* Added one new root certificate and removed 3 root certificates from Entrust. (Refer to 6805338.)
* Added three new root certificates from Keynectis. (Refer to 6845457.)
* Added three new root certificates from Quovadis. (Refer to 6846473.)
Bug Fixes
This release contains fixes for one or more security vulnerabilities. For more
information, please see Sun Alerts 263408 , 263409 , 263488 , 263489 , and 264648.
Bug fixes for vulnerabilities are listed in the following table.
BugId Category Subcategory Description 6656610 java accessibility AccessibleResourceBundle.getContents exposes mutable static (findbugs)
6656586 java classes_awt Cursor.predefined is protected static mutable (findbugs)
6660539 java classes_beans Introspector cache mutable static
6446522 java classes_lang 3Y Race condition in reflection checks
6801071 java classes_net Remote sites can compromise user privacy and possibly hijack web session
6801497 java classes_net Proxy is assumed to be immutable but is non-final
6406003 java classes_security Security issues in the Provider class
6429594 java classes_security Fix for 6406003 can be circumvented
6444262 java classes_security Provider deserialization still has problems
6657695 java classes_security AbstractSaslImpl.logger is a static mutable (findbugs)
6657625 java classes_sound RmfFileReader/StandardMidiFileWriter.types are public mutable statics (findbugs)
6738524 java classes_sound JDK13Services allows read access to system properties from untrusted code
6777448 java classes_sound JDK13Services.getProviders creates instances with full privileges
6588003 java classes_swing LayoutQueue mutable statics
6660049 java classes_swing Synth Region.uiToRegionMap/lowerCaseNameMap are mutable statics
6656625 java imageio ImageReaderSpi.STANDARD_INPUT_TYPE/ImageWriterSpi.STANDARD_OUTPUT_TYPE are mutable static (findbugs)
6657133 java imageio Mutable statics in imageio plugins (findbugs)
6830335 java jar Java JAR Pack200 Decompression Integer Overflow Vulnerability
6862844 javawebstart other java web start ActiveX control security problem caused by ATL PROP_ENTRY macro
6845701 jaxp parse Xerces2 Java XML library infinite loop with malformed XML input
6657619 jndi dns DnsContext.debug is public static mutable (findbugs)
Other bug fixes are listed in the following table.
BugId Category Subcategory Description 6851379 java classes_2d font files not deleted upon exit
6805338 java classes_security Add 1 new Entrust root CA cert and remove 3 others with 1024 bit keys
6845457 java classes_security Add root certs for Keynectis CA
6846473 java classes_security Add QuoVadis root CA certs to the JRE
6848984 java classes_util_i18n (tz) Support tzdata2009i
6851214 java classes_util_i18n (tz) New Jordan rule creates a failure for SimpleTimeZone parsing post tzdata2009h
* Bugs fixed:
- si_{set,get}_finalizer were not exported from ecl.dll and thus the library
TRIVIAL-GARBAGE failed to build in Windows
- The MSVC port did not define @ECL_LDRPATH@ and failed to build ecl.dll
- The sequence functions did not understand the newest specialized array types.
* Visible changes:
- The configuration flag --with-__thread now defaults to NO because many
platforms do not support it and GCC does not complain, making reliable
detection impossible.
- For further compatibility with SBCL, ECL now supports two additional
buffer types :FULL and :LINE which are compatible with :FULLY-BUFFERED
and :LINE-BUFFERED (Thanks to Matthew Mondor)
- The sockets library can now be loaded using either (REQUIRE 'SOCKETS)
or (REQUIRE 'SB-BSD-SOCKETS).
Changes since previous packaged version are too long to list,
they include 1,5 years of continuous development, adding features,
compiler optimizations, and fixing bugs. See log at
http://www.sbcl.org/all-news.html
Changes in 0.9.9:
* bugfixes
* extend and improve support for attributes
* adapat to latest libfirm
Changes in 0.9.8:
* several bugfixes
* add/correct semantic checks
* improve error recovery
* support more GCC extensions
* add/improve/correct warnings
Changes in 1.8.7 (since 1.8.6)
* Bugs fixed
** Fix compilation with `--disable-deprecated'
** Fix %fast-slot-ref/set!, to avoid possible segmentation fault
** Fix MinGW build problem caused by HAVE_STRUCT_TIMESPEC confusion
** Fix build problem when scm_t_timespec is different from struct timespec
** Fix build when compiled with -Wundef -Werror
** More build fixes for `alphaev56-dec-osf5.1b' (Tru64)
** Build fixes for `powerpc-ibm-aix5.3.0.0' (AIX 5.3)
** With GCC, always compile with `-mieee' on `alpha*' and `sh*'
** Better diagnose broken `(strftime "%z" ...)' in `time.test' (bug #24130)
** Fix parsing of SRFI-88/postfix keywords longer than 128 characters
** Fix reading of complex numbers where both parts are inexact decimals
** Allow @ macro to work with (ice-9 syncase)
Previously, use of the @ macro in a module whose code is being
transformed by (ice-9 syncase) would cause an "Invalid syntax" error.
Now it works as you would expect (giving the value of the specified
module binding).
** Have `scm_take_locale_symbol ()' return an interned symbol (bug #25865)
** Fix potential deadlocks when running on multiple threads
** Fix problems building with the i586-mingw32msvc cross-compiler
It's now possible to build Guile for Windows by using the
i586-mingw32msvc cross-compiler on GNU/Linux. This kind of build
produces DLLs and a main program that can be copied to and used on a
Windows PC. For how to do this, see the `Cross building Guile'
section in `README'.
User-visible changes between 0.6.2 and 0.7.0:
Requirements:
At run-time requires libtool and gcc (for the libcc C interface) and
gdb (for the disassembler (SEE)) on some platforms.
License:
Changed to GPLv3
Bug fixes
Now works with address-space randomization.
The single-step debugger works again in some engines.
Many others.
Ports:
AMD64, ARM, IA-64 (Itanium): better performance
PPC, PPC64: disassembler and assembler
Gforth EC: R8C, 4stack, misc, 8086 work
MacOS X: better support
Invocation:
New flags --ignore-async-signals, --vm-commit (default overcommit)
--print-sequences
Forth 200x:
X:extension-query: produce true for all implemented extensions
X:required REQUIRED etc. (not new)
X:defined: [DEFINED] and [UNDEFINED]
X:parse-name: PARSE-NAME (new name)
X:deferred: deferred words (new: DEFER@ DEFER! ACTION-OF)
X:structures: +FIELD FIELD: FFIELD: CFIELD: etc.
X:ekeys: new: EKEY>FKEY K-SHIFT-MASK K-CTRL-MASK K-ALT-MASK K-F1...K-F12
X:fp-stack (not new)
X:number-prefixes (partially new, see below)
Number prefixes:
0x is a hex prefix: 0xff and 0XfF now produces (decimal) 255
# is a decimal prefix: #10 now produces (decimal) 10
Signs after the number prefix are now accepted, e.g, #-50.
' now only handles a single (x)char: 'ab is no longer accepted,
'a' now produces (decimal) 97
Unicode support (currently supports only uniform encoding):
added xchars words for dealing with variable-width multi-byte characters
provide 8bit (ISO Latin 1) and UTF-8 support for xchars
New words:
\C C-FUNCTION C-LIBRARY END-C-LIBRARY C-LIBRARY-NAME (libcc C interface)
LIB-ERROR (complements OPEN-LIB)
OUTFILE-EXECUTE INFILE-EXECUTE BASE-EXECUTE (limited change of global state)
16-bit and 32-bit memory acces: UW@ UL@ SW@ SL@ W! L! W@ L@ /W /L
NEXT-ARG SHIFT-ARGS (OS command-line argument processing)
NOTHROW (for backtrace control)
FTRUNC FMOD (undocumented)
SEE-CODE SEE-CODE-RANGE (show generated dynamic native code)
Improvements/changes of existing words:
S\", .\" now support \l, \m, \z, and limits hex and octal character specs.
OPEN-FILE with W/O no longer creates or truncates files (no compat. file)
OPEN-LIB now understands ~ at the start, like OPEN-FILE.
TRY...ENDTRY changed significantly, compatibility files available (see docs).
The disassembler (DISCODE) can now use gdb to disassemble code
Uninitialized defered words now give a warning when executed
Division is floored (disable with "configure --enable-force-cdiv")
Gforth (not gforth-fast) reports division by zero and overflow on division
on all platforms.
Newly documented words:
S>NUMBER? S>UNUMBER?
EKEY keypress names: K-LEFT K-RIGHT K-UP K-DOWN K-HOME K-END K-PRIOR
K-NEXT K-INSERT K-DELETE
CLEARSTACKS
FORM
Environment variable GFORTHSYSTEMPREFIX (used by word SYSTEM and friends)
C interface:
exported symbols now start with "gforth_" (for referencing them from C code)
libcc C function call interface (requires libtool and gcc at run-time)
alternative: undocumented libffi-based interface
Libraries:
depth-changes.fs: report stack depth changes during interpretation
ans-report.fs now reports CfV extensions
fsl-util.4th: FSL support files (undocumented)
regexp.fs for regular expressions (undocumented)
complex.fs for complex numbers (undocumented)
fft.fs for Fast Fourier Transform (undocumented)
wf.fs, a Wiki implementation (undocumented)
httpd.fs, a web server (undocumented)
status.fs, show interpreter status in separate xterm (undocumented)
profile.fs for profiling (undocumented, incomplete)
endtry-iferror.fs, recover-endtry.fs to ease the TRY change transition
test/tester.fs: Now works with FP numbers (undocumented)
test/ttester.fs: Version of tester.fs with improved interface (T{...}T).
compat library:
compat/execute-parsing.fs
Speed improvements:
automatic performance tuning on building
static stack caching (good speedup on PPC)
mixed-precision division is now faster
support for int128 types on AMD64
workarounds for gcc performance bugs (in particular, PR 15242)
branch target alignment (good speedup on Alpha).
Changes since previous packaged version (8.12.0) include half year
of very active development:
- The dynamic FFI is now implemented using libffi.
- Support of UNICODE.
- Multithreading (provided Boehm-GC built with threads support).
- Command line flags to control the different memory limits:
--heap-size, --lisp-stack, --frame-stack and --c-stack.
- The stack size is now measured in bytes, not in lisp words.
- The out of memory error (ext:storage-exhausted) can now be recovered.
By default a correctable error is signaled and the user is given the
chance to increase the heap size.
- Better compiler, optimizer, debugger.
- Improved handling of compiler errors.
- New and more easily extensible implementation of streams.
- *STANDARD-INPUT*, *{STANDARD,ERROR,TRACE}-OUTPUT* are no longer synonyms to
*TERMINAL-IO* but directly the input or output streams associated to stdin,
stdout and stderr.
- Improved numerics.
- Read-only readtables.
- Numerous bug fixes.
Changes
* Add support for static properties.
* Add support for delegate properties.
* Support virtual default handler for signals.
* Add limited support for derived compact classes.
* Add libgdata bindings (Víctor Manuel Jáquez Leal).
* Add libusb-1.0 bindings (Evan Nemerson).
* Many bug fixes and binding updates.
Vala 0.7.4
Changes
* Add support for array properties.
* Support implicit and explicit GValue casts.
* Add initial support for generic methods.
* Add postgres bindings.
* Many bug fixes and binding updates.
Vala 0.7.3
Changes
* Add initial support for POSIX profile.
* Add --vapi and --gir commandline options.
* Add initial x11, xcb, and cairo-xcb bindings.
* Many bug fixes and binding updates.
Vala 0.7.2
Changes
* Improvements to the .gir reader and writer (Didier Ptitjes).
* Many bug fixes and binding updates.
Vala 0.7.1
Changes
* Introduce new syntax to connect/disconnect signal handlers.
* Add experimental support for fixed-length arrays.
*
Update Genie parser (Jamie McCracken).
* Updates to the GLib, Cairo, GTK+, GStreamer, and POSIX bindings.
* Many bug fixes.
Vala 0.7.0
Changes
* Do not generate header files unless requested by the -H commandline
o option. This requires changes in the build system of Vala projects.
* Support conditional compilation.
Vala 0.6.1
Changes
* Updates to the GLib, Cairo, GTK+, GStreamer, and POSIX bindings.
* Minor bug fixes.
Vala 0.6.0
Changes
* Improvements to the .gir reader and writer (Didier Ptitjes).
* Add librsvg-2.0 bindings (Evan Nemerson).
* Add Maemo libosso bindings (Jukka-Pekka Iivonen).
* Add V4L2 bindings (Matías De la Puente).
* Many bug fixes.
