|
From: Michael N. <Mic...@ni...> - 2005-09-27 06:21:42
|
We're pleased to announce the release of the latest version of the HOL4 theorem-proving system, Kananaskis-3. It is available for download from http://hol.sourceforge.net A source tarball is available for all platforms (Unixes, Windows and Mac OS 10), as well as a Windows self-extracting archive executable. ---------------------------------------------------------------------- Notes on HOL 4, Kananaskis-3 release New features: * 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 installati= on (before build): mosml < tools/smart-configure.sml * The term and type parsers now report errors with an indication a= s to where in the parse they have occurred. If the error is found during a run of Holmake, the location includes the line number i= n the file where the error is. Pragma comments of the form (*#loc 100 5*) allow the line and column numbers to be overridde= n, =E0 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 mod= e. 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 implementation= s. For example, one can define a variable OBJS, OBJS =3D 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 o= f 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= =2E 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= =2E 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=5Fdollar=5Fescapes". * 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=5Flistform, whose type has changed, for more detail on t= his. (Thanks to Lockwood Morris for this feature suggestion.) * There are two new simpset fragments in realSimps. REAL=5FREDUCE=5F= ss performs calculations over ground rational values. Thus, SIMP=5FCONV (std=5Fss ++ REAL=5FREDUCE=5Fss) [] ``1/3 - 3/7`` returns > val it =3D |- 1 / 3 - 3 / 7 =3D ~2 / 21 : thm When realSimps is loaded, REAL=5FREDUCE=5Fss is automatically ad= ded 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=5FARITH=5Fss, w= hich embodies the RealArith decision procedure for universal Presburg= er 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 norma= l rewrites with the functions simpLib.AC and simpLib.Cong. Thus, - SIMP=5FCONV bool=5Fss [AC ADD=5FCOMM ADD=5FASSOC] ``3 + x + = y + 1``; > val it =3D |- 3 + x + y + 1 =3D 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 t= he DESCRIPTION for more details. * Support for abbreviations in goals, via tactics such as Q.ABBREV=5FTAC, is now a deal richer. Abbbreviations are now specially marked as such in a goal's assumptions, protecting the= m against being removed by tactics such as RW=5FTAC or SRW=5FTAC. = There are also new tactics for establishing abbreviations, such as MATCH=5FABBREV=5FTAC and PAT=5FABBREV=5FTAC. For more on these a= nd other new tactics, see the REFERENCE (or the online help). To support old code, the old implementations of these tactics ar= e available in a structure OldAbbrevTactics. Thus, it is possible = to restore a file to its old behaviour by including: structure Q =3D struct open Q open OldAbbrevTactics end; at the top of an affected file. Bugs fixed: * Hol=5Fdatatype would fail if called on to define a type with a single nullary constructor. * pred=5FsetLib.UNION=5FCONV (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=5Ftheory declaration, causing these effects not to persist w= ith 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 correctl= y. * Adding a user-supplied pretty-printer caused polymorphic terms t= o fail to print. (The interface for adding pretty-printers is also= now slightly richer, see the REFERENCE manual for details.) * DECIDE=5FTAC didn't pay attention to goal assumptions. * A bug in ARITH=5FCONV's handling of conditional expressions caus= ed 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 th= is bug.) * SPEC=5FVAR and theory export caused bound variables with the sam= e 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 rule= s. 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 Nipk= ow for useful discussion about this bug.) * pairLib.PAIRED=5FETA=5FCONV was broken. Thanks to Viktor Sabelfe= ld for the bug report. * Q.UNDISCH=5FTHEN was behaving more as if it were Q.PAT=5FUNDISCH= =5FTHEN; it was finding matches in the assumptions rather than equal term= s. Thanks to Lockwood Morris for the bug report. * The order in which type arguments appeared as arguments to polymorphic type operators defined by Hol=5Fdatatype was previou= sly undefined. For example, if one wrote: Hol=5Fdatatype `sum =3D left of 'a | right of 'b`; it was not specified that ('a,'b)sum was the type which associat= ed the variable 'a with the left constructor. Now, the type picks u= p the type variable arguments in Hol=5Fdatatype in alphabetical or= der. 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.)= New theories: * A theory of co-inductive (possibly infinite) labelled transition= paths in pathTheory. * A theory of sorting and list permutations in sortingTheory. New tools: * A new first-order proof tactic (called METIS=5FTAC) 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= =2E New examples: * 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. Incompatibilities: * The four HOL executables have had their names adjusted. We now think that using HOL with the quotation filter is the appropriat= e default for all users. To reflect this, the executable hol now includes the quotation filter. (This executable used to be calle= d 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 =3D f v has been removed from std=5Fss and later simplification sets. (Simpsets arith=5Fss, list=5Fss and srw=5Fss() are all affected.= ) Old behaviours can be restored with code such as val std=5Fss =3D std=5Fss ++ simpLib.rewrites [LET=5FTHM] * Rewrite rules for arithmeticTheory's MIN and MAX constants have been made more general; they will now match more often. For example, MIN=5FLE has changed from m <=3D MIN m n =3D m <=3D n to p <=3D MIN m n =3D p <=3D m /\ p <=3D n * For reasons of efficiency, all conversions in the system may now= potentially raise the special exception Conv.UNCHANGED to indica= te that they haven't changed the input term, and that they should b= e treated as if they had returned the theorem |- t =3D t, for inpu= t t. Conversion connectives (such as THENC, ORELSEC and TRY=5FCONV) a= ll 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=5FRULE and CONV=5FTAC handle the excep= tion appropriately, and the new function QCONV (of type : conv -> con= v) can make any conversion handle UNCHANGED. QCONV's implementation= is fun QCONV c t =3D c t handle UNCHANGED =3D> 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 =3D let val th =3D someconv t val .. =3D <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=5FTO=5FSET 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=5Fbit/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. =5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F= =5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F= =5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F |