Configuration and installation of the system is easier.
Instead of having to edit configure.sml yourself,
just pipe tools/smart-configure into
mosml as the first step of installation (before
build):
mosml < tools/smart-configure.sml
The term and type parsers now report errors with an indication as
to where in the parse they have occurred. If the error is found
during a run of Holmake, the location includes the line number in
the file where the error is. Pragma comments of the form
(*#loc 100 5*) allow the line and column
numbers to be overridden, à la C’s #line
directive. (Many thanks to Keith Wansbrough for the
implementation of this feature.) The lexer is also much faster
than it used to be.
The system better distinguishes interactive and non-interactive
use (the latter occurs with building things with Holmake).
Diagnostic output is now rather different in non-interactive mode.
Holmake comes with a new -i or
--interactive flag to flip the underlying flag back
to interactive, if you want to see "interactive mode" output.
Holmake now supports the use of user-specified variables, in a
manner analogous to that done by traditional make implementations.
For example, one can define a variable OBJS,
OBJS = foo bar baz
and then refer to this variable elsewhere by writing
$(OBJS) Holmake also provides some functions like
those in GNU make for manipulating text (performing pattern-based
substitutions, for example). See the DESCRIPTION for more
details.
Performance when defining large record types (where the number of fields is greater than a user-adjustable reference variable), is now much improved. Part of this change was to remove update functions as separate constants (they are now encoded using functional update functions), though the concrete syntax remains. See the DESCRIPTION for more details.
In addition to the traditional $-prefix for making identifiers ignore their status as special forms in the grammar, HOL now supports the Caml method of enclosing identifiers in parentheses. Thus, instead of
$/\ p
one can also write
(/\) p
By default, the pretty-printer continues to print using the old
$-syntax. This can be changed by setting the trace variable
"pp_dollar_escapes".
Pretty-printing of “list forms” (e.g., lists,
sets and bags) is now under more user-control. See the REFERENCE
(or online help) for add_listform, whose type has
changed, for more detail on this. (Thanks to Lockwood Morris for
this feature suggestion.)
There are two new simpset fragments in realSimps.
REAL_REDUCE_ss
performs calculations over ground rational values. Thus,
SIMP_CONV (std_ss ++ REAL_REDUCE_ss) [] ``1/3 - 3/7``
returns
> val it = |- 1 / 3 - 3 / 7 = ~2 / 21 : thm
When realSimps is loaded, REAL_REDUCE_ss
is automatically added to the stateful-rewriting simpset, and
bossLib’s EVAL is also augmented
with this functionality. This code also removes common factors
from fractions even when there are no other arithmetic operations
being performed.
The second simpset fragment in realSimps is
REAL_ARITH_ss, which embodies the
RealArith decision procedure for universal Presburger
arithmetic over the real numbers.
The simplifier now provides simpler interfaces for the addition of
AC-rewriting and congruence rules. They can be added as if normal
rewrites with the functions simpLib.AC and
simpLib.Cong. Thus,
- SIMP_CONV bool_ss [AC ADD_COMM ADD_ASSOC] ``3 + x + y + 1``;
> val it = |- 3 + x + y + 1 = x + (y + (1 + 3)) : thm
Cong is used similarly. Both functions are further
described in the REFERENCE.
Holmake now supports a new command-line option
--logging, which tells it to record running times for
the building of theories. These times are stored in a file in the
current directory. See the DESCRIPTION for more
details.
Support for abbreviations in goals, via tactics such as
Q.ABBREV_TAC, is now a deal richer. Abbbreviations
are now specially marked as such in a goal’s assumptions,
protecting them against being removed by tactics such as
RW_TAC or SRW_TAC. There are also new
tactics for establishing abbreviations, such as
MATCH_ABBREV_TAC and PAT_ABBREV_TAC.
For more on these and other new tactics, see the REFERENCE (or the
online help).
To support old code, the old implementations of these tactics
are available in a structure OldAbbrevTactics. Thus,
it is possible to restore a file to its old behaviour by
including:
structure Q = struct open Q open OldAbbrevTactics end;
at the top of an affected file.
Hol_datatype would fail if called on to define
a type with a single nullary constructor.
pred_setLib.UNION_CONV (and other functions in this
library) failed to work as advertised. (Thanks to Lockwood Morris
for the report of this bug.)
It was too easy to do significant parser things before a
new_theory declaration, causing these effects not to
persist with the export of the theory. Now, attempting to do this
causes a strong warning to be issued.
let terms with bodies that were abstractions didn’t
print correctly.
The type grammar didn’t print stored type abbreviations correctly.
Adding a user-supplied pretty-printer caused polymorphic terms to fail to print. (The interface for adding pretty-printers is also now slightly richer, see the REFERENCE manual for details.)
DECIDE_TAC didn’t pay attention to goal
assumptions.
A bug in ARITH_CONV’s handling of conditional
expressions caused some quantified goals to fail to be proved.
The lexer got confused if a token made up of non-aggregating
characters (e.g., including ";") was used, but not as part of
special concrete syntax. I.e., ;; was OK as an
infix, but not as a normal constant. (Thanks to Klaus Schneider
for the report of this bug.)
SPEC_VAR and theory export caused bound variables
with the same name as constants to get changed. (Thanks to
Lockwood Morris for the report of this bug.)
Many, many documentation typos and bugs were fixed. (Thanks to Carl Witty for the report of most of these.)
Two fixes for the simplifier’s implementation of congruence rules. With deep nesting, congruence rules could lead to an exponential increase in time taken. Also, terms that included variables used in a rule’s statement could cause the rule to fail to fire.
The simplifier’s AC-rewriting could cause it to go into an infinite loop. While the new behaviour does AC-normalise everywhere (we hope!), it is not necessarily the same as the old behaviour on examples which used to work. (Thanks to Tobias Nipkow for useful discussion about this bug.)
pairLib.PAIRED_ETA_CONV was broken. Thanks to
Viktor Sabelfeld for the bug report.
Q.UNDISCH_THEN was behaving more as if it were
Q.PAT_UNDISCH_THEN; it was finding matches in the
assumptions rather than equal terms. Thanks to Lockwood Morris
for the bug report.
The order in which type arguments appeared as arguments to
polymorphic type operators defined by Hol_datatype
was previously undefined. For example, if one wrote:
Hol_datatype `sum = left of 'a | right of 'b`;
it was not specified that ('a,'b)sum was the type
which associated the variable 'a with the
left constructor. Now, the type picks up the type
variable arguments in Hol_datatype in alphabetical
order. This may break code that relied on what was an
unspecified behaviour.
The quotation filter didn’t recognise text of the form
``:
foo
``
with a newline immediately following the colon as a type quotation. (Thanks to Steve Brackin for the report of this bug.)
A theory of co-inductive (possibly infinite) labelled transition
paths in pathTheory.
A theory of sorting and list permutations in
sortingTheory.
A new first-order proof tactic (called
METIS_TAC) that uses ordered resolution and
paramodulation, specifically tailored for subgoals that require
equality reasoning.
A ‘boolification’ tool that automatically defines functions that map datatypes to boolean vectors. These kind of functions are needed for sending HOL subgoals to a model-checker or SAT solver.
An extension of the existing lambda calculus example (examples/lambda) to include mechanisations of chapters 2 & 3 of Hankin’s lambda calculus text, and the standardisation theorem from Barendregt’s chapter 11.
A formalization of the probabilistic guarded command language (pGCL) in higher-order logic, including a tool for deriving sufficient verification conditions for partial correctness.
The four HOL executables have had their names adjusted.
We now think that using HOL with the quotation filter is the
appropriate default for all users. To reflect this, the executable
hol now includes the quotation filter. (This executable
used to be called hol.unquote.) To avoid using the
quotation filter, use hol.noquote. Analogous changes
have been made to hol.bare; i.e.,
hol.bare now includes the filter, and
hol.bare.noquote does not.
The rewrite theorem for LET,
LET f v = f v
has been removed from std_ss and later simplification
sets. (Simpsets arith_ss, list_ss and
srw_ss() are all affected.)
Old behaviours can be restored with code such as
val std_ss = std_ss ++ simpLib.rewrites [LET_THM]
Rewrite rules for arithmeticTheory’s
MIN and MAX constants have been made
more general; they will now match more often. For example,
MIN_LE has changed from
m <= MIN m n = m <= n
to
p <= MIN m n = p <= m /\ p <= n
For reasons of efficiency, all conversions in the system may now
potentially raise the special exception
Conv.UNCHANGED to indicate that they haven’t changed
the input term, and that they should be treated as if they had
returned the theorem |- t = t, for
input t. Conversion connectives (such as
THENC, ORELSEC and
TRY_CONV) all do the appropriate thing in the
presence of this exception. Previously, sub-systems such as the
simplifier, rewriter and arithmetic decision procedures have used
this idea to make them work faster, but couldn’t share information
about unchangedness.
For interactive use, CONV_RULE and
CONV_TAC handle the exception appropriately, and the
new function QCONV (of type
: conv -> conv) can make any
conversion handle UNCHANGED. QCONV’s
implementation is
fun QCONV c t = c t handle UNCHANGED => REFL t
If you have code implementing conversions of your own, you may
need to fix code if it uses the following idiom:
fun myconv t =
let val th = someconv t
val .. = <fiddle with th>
in
<resulting theorem>
end
If someconv raises UNCHANGED, then
myconv will too, causing expressions such as
myconv THENC <something else>
to treat myconv as if it hadn’t done anything
(because the <fiddle with th> code
never got called).
This can be relatively difficult to track down, but the fix is
simple enough: change someconv t to
QCONV someconv t.
The constant LIST_TO_SET is now defined in
listTheory.
The word32 theory is not built by default.
Instead, a general wordn-theory creating
executable, mkword.exe is available in the
hol/bin/ directory. This can be invoked to create
word theories of various sizes. For example,
$ mkword.exe 32
will create a word32Theory in the current
directory. These new theories don’t have corresponding
Script files, so Holmake doesn’t
automatically update these theories. If this is a concern, the
Holmakefile in
hol/src/n_bit/help/Holmakefile.example-32 demonstrates how to
ensure word theories are rebuilt.
The type simpLib.ssdata is now called
simpLib.ssfrag and the constructor for this type that
used to be called SIMPSET is now called
SSFRAG.