1% Release notes for HOL4, Kananaskis-10 2 3<!-- search and replace ?????? strings corresponding to release name --> 4<!-- indent code within bulleted lists to column 11 --> 5 6(Released: 10 November 2014) 7 8We are pleased to announce the Kananaskis-10 release of HOL 4. 9 10Contents 11-------- 12 13- [New features](#new-features) 14- [Bugs fixed](#bugs-fixed) 15- [New theories](#new-theories) 16- [New tools](#new-tools) 17- [Examples](#examples) 18- [Incompatibilities](#incompatibilities) 19 20New features: 21------------- 22 23* Our *TUTORIAL* and *LOGIC* manuals are now available in Italian translations. Work on the *DESCRIPTION* manual is also far advanced. Many, many thanks to Domenico Masini for doing this work. 24 25* The abbreviation tactics (`Q.ABBREV_TAC` and others) now handle abstractions as abbreviations better. In particular, if one sets up an abstraction as an abbreviation (*e.g.*, ``Q.ABBREV_TAC `f = (��n. 2 * n + 10)` ``), then the simplifier will find and replace instances not just of the abstraction itself (the old behaviour), but also instances of applications of the abstraction to arguments. For example, given the abbreviation for `f` above, the simplifier would turn a goal such as `2 * (z + 1) + 10 < 100` into `f (z + 1) < 100`. 26 27* The `MAX_SET` function in `pred_setTheory` is now defined (to have value `0`) on the empty set. 28 29* There is an alternative syntax for specifying datatypes. Instead of the `Hol_datatype` entry-point, one can also use `Datatype`, which takes a slightly different syntax, inspired by Haskell. This does away with the use of the (somewhat confusing) `of` and `=>` tokens. 30 31 For example, one would define a simple type of binary tree with 32 33 Datatype`tree = Lf num | Node tree tree` 34 35 If the arguments to a constructor are not just simple types (expressible as single tokens), then they need to be enclosed in parentheses. For example: 36 37 Datatype`mytype = Constr mytype ('a -> bool) | BaseCase` 38 39 The `Hol_datatype` entry-point can continue to be used. However, the LaTeX output of `EmitTeX` uses the new format, and the various `DATATYPE` constructors used in the `EmitML` module take quotations in the new format, rather than the old. 40 41* The arithmetic decision procedure for natural numbers will now prove slightly more goals by doing case-splits on boolean sub-terms that are not in the Presburger subset. This means that goals such as 42 43 0 < y ��� x < x + (if P then y else y + 1) 44 45 are now provable. 46 47* The Vim mode for HOL now supports multiple simultaneous sessions. See its `README` for details. 48 49* Many of the standard libraries now provide an `add_X_compset : compset -> unit` (*e.g.*, `add_pred_set_compset`) to ease building of custom call-by-name evaluation conversions that don't, like `EVAL`, include everything in `the_compset()`. 50 51* `Holmake` has a new function, `wildcard` which allows expansion of ���glob��� patterns (*e.g.*, `*Script.sml`) into lists of matching filenames. 52 53* The standard pretty-printer now annotates constants with their types as well as variables. (Note that these annotations are typically only visible by using mouse-over tooltips in the emacs mode.) The annotation also includes the constant���s real name, in the form `thy$name`, making overloads easier to tell apart. 54 55 For example, this means that it is possible to have integers, reals and numbers all in scope, to write something like `MAP (+)`, and to then see what constants are involved by using the mouse. (See [Github issue #39](https://github.com/HOL-Theorem-Prover/HOL/issues/39).) 56 57* Unicode is handled slightly better on Windows systems. By default, the pretty-printer avoids printing with Unicode characters there, but can still parse Unicode input successfully. This is important because many of the examples distributed with HOL use Unicode characters in their scripts (nothing in `src/` does). This behaviour can be adjusted by toggling the `PP.avoid_unicode` trace. On Windows this trace is initialised to true; elsewhere it is initialised to false. 58 59Bugs fixed: 60----------- 61 62* `Holmake` was unnecessarily quiet when it compiled certain SML files. 63 64* The ���munging��� code for turning HOL into LaTeX now does a better job of rendering data type definition theorems. (This change is independent of the new underlying syntax described earlier.) 65 66* Pretty-printers added to the system with `add_user_printer` weren���t having terms-to-be-printed tested against the supplied patterns (except by the gross approximation provided by the built-in term-net structure). Thanks to Ramana Kumar for the [bug report](https://github.com/mn200/HOL/issues/172). 67 68* Character literals weren���t pretty-printing to LaTeX. We also improved the handling of string literals. Thanks to Ramana Kumar for the [bug reports](http://github.com/HOL-Theorem-Prover/HOL/issues/190). 69 70* Piotr Trojanek found and fixed many documentation bugs in our various manuals. 71 72* The `remove_rules_for_term` and `temp_remove_rules_for_term` functions tended to remove rules for binders as well as the desired rules. 73 74New theories: 75------------- 76 77* A theory of ���list ranges��� (`listRangeTheory`). A range is a term written `[ lo ..< hi ]`, meaning the list consisting of the (natural) numbers from `lo` up to, but not including, `hi`. The theory comes with some basic and obvious theorems, such as 78 79 MEM i [lo ..< hi] ��� lo ��� i ��� i < hi 80 81 and 82 83 LENGTH [lo ..< hi] = hi - lo 84 85* A new development in `src/floating-point`, which is a reworking of the theories in `src/float`. Key differences are listed below. 86 87 1. The data representation: 88 89 - The old `ieeeTheory` uses a pair ` ``:num # num`` ` to represent the exponent and fraction widths and a triple ` ``:num # num # num`` ` to represent sign, exponent and fraction values. 90 91 - The new `binary_ieeeTheory` makes use of HOL records and bit-vectors. The floating-point type ` ``:(��, ��) float`` ` has values of the form 92 93 <| Sign : word1; Exponent : �� word; Significand : �� word |> 94 95 The fraction and exponent widths are now constrained by the type, which facilitates type-checking and avoids having to pass size arguments to operations. 96 97 2. The new development now supports standard bit-vector encoding schemes. The theory `machine_ieeeTheory` defines floating-point operations over 16-bit, 32-bit and 64-bit values. For example, the 16-bit floating point operations are defined by mapping to and from the type ``:(10, 5) float``, which is given the type abbreviation ``:half``. Theories for other sizes can be built using `machine_ieeeLib.mk_fp_encoding`. 98 99 3. There is now syntax support via the structures `binary_ieeeSyntax` and `machine_ieeeSyntax`. 100 101 4. Ground term evaluation is now supported for most operations. This can be enabled by loading `binary_ieeeLib`. 102 103 5. The full development does not build under Moscow ML 2.01, as it makes use of the `IEEEReal` and `PackRealBig` basis structures. 104 105* A theory of ���simple Patricia trees��� (`sptreeTheory`). This theory implements a type `�� sptree`, which is a finite map from natural numbers to values of type `��`. (This type is not really a Patricia tree at all; for those, see the other theories in `src/patricia`.) Values of type `�� sptree` feature efficient lookup, insertion, deletion and union (efficient when evaluated with `EVAL` or simplified). Though there is a efficient (linear-time) fold operation, it does not iterate over the key-value pairs in key-order. 106 107New tools: 108---------- 109 110- New libraries `enumLib` and `fmapalLib` provide representations in `pred_set` and finite map types of enumerated constant sets and maps as minimum-depth binary search trees. A suitable total order on the set elements (map arguments) must be supplied, with a conversion for evaluating it; assistance with this is provided. The primary objective has been an `IN_CONV`, and a similar `FAPPLY_CONV`, operating with a logarithmic number of comparisons, but additional operations such as `UNION_CONV`, `INTER_CONV`, and `FUPDATE_CONV` are included and have reasonable asymptotic running times. A conversion `TC_CONV` implements Warshall���s algorithm for transitive closure of a binary relation (treated as a set-valued finite map). 111 112 113Examples: 114--------- 115 116- The `miniml` example has been removed. This work has evolved into the [CakeML project](http://cakeml.org). That project���s `git` repository contains all of the material that was once in the HOL distribution, and, given its continuing evolution, much more besides. 117 118 119Incompatibilities: 120------------------ 121 122- In `relationTheory`, the theorems `TC_CASES1` and `TC_CASES2` have been renamed to `TC_CASES1_E` and `TC_CASES2_E` respectively, where the `_E` suffix indicates that these are elimination rules. In other words, these theorems are of the form `TC R x y ��� ...`. This has been done so that new equivalences can be introduced under the old names. For example, `TC_CASES1` now states 123 124 TC R x z ��� R x z ��� ���y. R x y ��� TC R y z 125 126 This change makes the naming consistent with similar theorems `RTC_CASES1` and `RTC_CASES2` about the reflexive and transitive closure. 127 128- A theorem stating 129 130 ��� ��(0 < n) ��� (n = 0) 131 132 (for `n` a natural number) has been added to the automatic rewrites used by `SRW_TAC` and `srw_ss()`. 133 134- Some new automatic rewrites from `pred_setTheory`: 135 136 * `��� DISJOINT (x INSERT s) t ��� DISJOINT s t ��� x ��� t` (and the version of this with `DISJOINT s (x INSERT t)` as the l.h.s.) 137 * `��� ���f s. INJ f ��� s` 138 * `��� ���f s. INJ f s ��� ��� (s = ���)` 139 140- The `add_binder` and `temp_add_binder` entry-points in `Parse` have been removed. They are subsumed by `set_fixity <name> Binder` and `temp_set_fixity <name> Binder` respectively. In addition, `add_binder` was broken, creating an unloadable theory on export. 141 142- There is a new automatic rewrite from `oneTheory`: 143 144 ��� ���v:one. v = () 145 146 stating that every value in the type `one` (analogue of SML���s `unit` type) is equal to the designated value `()`. 147 148- Constants that print to the TeX backend as symbolic identifiers (*e.g.*, non-alphanumeric tokens like `+`, `**`) are now annotated there with the `\HOLSymConst` command rather than `\HOLConst`. The default behaviour of `\HOLSymConst` (defined in `holtexbasic.sty`) is to do nothing. 149 150- If 151 * `Holmake` is called in a directory with a `Holmakefile`, **and** 152 * that `Holmakefile` has at least one explicit target, **and** 153 * `Holmake` is called with no command-line targets, 154 155 **then:** `Holmake` will attempt to build *only* the first target in that `Holmakefile`. We believe that this will cause problems in only a relatively small number of scenarios. The advantage of this change is that it makes `Holmake` easier to control from a `Holmakefile`. It also makes `Holmake`���s behaviour rather more like that of normal `make`. 156 157 One scenario, among others, where this change may cause problems is where Poly/ML users have set up a rule to create a HOL heap. The fix is to prepend something like the following to your `Holmakefile`: 158 159 THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml)) 160 TARGETS = $(patsubst %.sml,%.uo,$(THYFILES)) 161 162 all: $(TARGETS) ... 163 .PHONY: all 164 165 so that `all` becomes the first target of the `Holmakefile`. Any previous targets, such as HOL heaps, should be inserted where the `...` occurs above. 166 167 Note that `Holmakefile`s that only include variable declarations such as `OPTIONS = ...`, `INCLUDES = ...`, and `HOLHEAP = ...` don���t have any targets at all, so that `Holmake`���s behaviour in such files��� directories will not change. 168 169 170* * * * * 171 172<div class="footer"> 173*[HOL4, Kananaskis-10](http://hol.sourceforge.net)* 174 175[Release notes for the previous version](kananaskis-9.release.html) 176 177</div> 178