1<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/x 2html1/DTD/xhtml1-strict.dtd"> 3<html xmlns="http://www.w3.org/1999/xhtml"> 4<head> 5<meta http-equiv="content-type" 6 content="text/html ; charset=US-ASCII" /> 7<title>Release Notes for Kananaskis-3 version of HOL 4</title> 8</head> 9 10<body> 11<h1>Notes on HOL 4, Kananaskis-3 release</h1> 12 13<h2 id="contents">Contents</h2> 14<ul> 15 <li> <a href="#new-features">New features</a> </li> 16 <li> <a href="#bugs-fixed">Bugs fixed</a> </li> 17 <li> <a href="#new-theories">New theories</a> </li> 18 <li> <a href="#new-tools">New tools</a> </li> 19 <li> <a href="#new-examples">New examples</a> </li> 20 <li> <a href="#incompatibilities">Incompatibilities</a> </li> 21</ul> 22 23 24 25<h2 id="new-features">New features:</h2> 26 27<ul> 28<li> <p> Configuration and installation of the system is easier. 29 Instead of having to edit <code>configure.sml</code> yourself, 30 just pipe <code>tools/smart-configure</code> into 31 <code>mosml</code> as the first step of installation (before 32 build):</p> 33<pre> 34 mosml < tools/smart-configure.sml 35</pre></li> 36 37<li> <p> The term and type parsers now report errors with an indication as 38 to where in the parse they have occurred. If the error is found 39 during a run of Holmake, the location includes the line number in 40 the file where the error is. Pragma comments of the form 41 <code>(*#loc 100 5*)</code> allow the line and column 42 numbers to be overridden, à la C’s <code>#line</code> 43 directive. (Many thanks to Keith Wansbrough for the 44 implementation of this feature.) The lexer is also much faster 45 than it used to be.</p></li> 46 47<li> <p> The system better distinguishes interactive and non-interactive 48 use (the latter occurs with building things with Holmake). 49 Diagnostic output is now rather different in non-interactive mode. 50 Holmake comes with a new <code>-i</code> or 51 <code>--interactive</code> flag to flip the underlying flag back 52 to interactive, if you want to see "interactive mode" output.</p></li> 53 54<li> <p> Holmake now supports the use of user-specified variables, in a 55 manner analogous to that done by traditional make implementations. 56 For example, one can define a variable <code>OBJS</code>,</p> 57 58<pre> 59 OBJS = foo bar baz 60</pre> 61 62 <p>and then refer to this variable elsewhere by writing 63 <code>$(OBJS)</code> Holmake also provides some functions like 64 those in GNU make for manipulating text (performing pattern-based 65 substitutions, for example). See the DESCRIPTION for more 66 details. </p></li> 67 68<li> <p> Performance when defining large record types (where the number of 69 fields is greater than a user-adjustable reference variable), is 70 now much improved. Part of this change was to remove update 71 functions as separate constants (they are now encoded using 72 functional update functions), though the concrete syntax remains. 73 See the DESCRIPTION for more details.</p></li> 74 75<li> <p>In addition to the traditional $-prefix for making identifiers 76 ignore their status as special forms in the grammar, HOL now 77 supports the Caml method of enclosing identifiers in parentheses. 78 Thus, instead of</p> 79<pre> 80 $/\ p 81</pre> 82 one can also write 83<pre> 84 (/\) p 85</pre> 86 87<p> By default, the pretty-printer continues to print using the old 88 $-syntax. This can be changed by setting the trace variable 89 <code>"pp_dollar_escapes"</code>.</p></li> 90 91 92 93<li> <p> Pretty-printing of “list forms” (e.g., lists, 94 sets and bags) is now under more user-control. See the REFERENCE 95 (or online help) for <code>add_listform</code>, whose type has 96 changed, for more detail on this. (Thanks to Lockwood Morris for 97 this feature suggestion.)</p></li> 98 99<li> <p>There are two new simpset fragments in realSimps. 100 <code>REAL_REDUCE_ss</code> 101 performs calculations over ground rational values. Thus,</p> 102<pre> 103 SIMP_CONV (std_ss ++ REAL_REDUCE_ss) [] ``1/3 - 3/7`` 104</pre> 105 returns 106<pre> 107 > val it = |- 1 / 3 - 3 / 7 = ~2 / 21 : thm 108</pre> 109 110 <p>When <code>realSimps</code> is loaded, <code>REAL_REDUCE_ss</code> 111 is automatically added to the stateful-rewriting simpset, and 112 <code>bossLib</code>’s <code>EVAL</code> is also augmented 113 with this functionality. This code also removes common factors 114 from fractions even when there are no other arithmetic operations 115 being performed.</p> 116 117 <p> The second simpset fragment in <code>realSimps</code> is 118 <code>REAL_ARITH_ss</code>, which embodies the 119 <code>RealArith</code> decision procedure for universal Presburger 120 arithmetic over the real numbers.</p></li> 121 122<li> <p>The simplifier now provides simpler interfaces for the addition of 123 AC-rewriting and congruence rules. They can be added as if normal 124 rewrites with the functions <code>simpLib.AC</code> and 125 <code>simpLib.Cong</code>. Thus,</p> 126<pre> 127 - SIMP_CONV bool_ss [AC ADD_COMM ADD_ASSOC] ``3 + x + y + 1``; 128 > val it = |- 3 + x + y + 1 = x + (y + (1 + 3)) : thm 129</pre> 130 <p><code>Cong</code> is used similarly. Both functions are further 131 described in the REFERENCE.</p></li> 132 133<li> <p> Holmake now supports a new command-line option 134 <code>--logging</code>, which tells it to record running times for 135 the building of theories. These times are stored in a file in the 136 current directory. See the DESCRIPTION for more 137 details. </p></li> 138 139<li> <p> Support for abbreviations in goals, via tactics such as 140 <code>Q.ABBREV_TAC</code>, is now a deal richer. Abbbreviations 141 are now specially marked as such in a goal’s assumptions, 142 protecting them against being removed by tactics such as 143 <code>RW_TAC</code> or <code>SRW_TAC</code>. There are also new 144 tactics for establishing abbreviations, such as 145 <code>MATCH_ABBREV_TAC</code> and <code>PAT_ABBREV_TAC</code>. 146 For more on these and other new tactics, see the REFERENCE (or the 147 online help). </p> 148 149 <p> To support old code, the old implementations of these tactics 150 are available in a structure <code>OldAbbrevTactics</code>. Thus, 151 it is possible to restore a file to its old behaviour by 152 including: </p> 153<pre> 154 structure Q = struct open Q open OldAbbrevTactics end; 155</pre> 156 <p> at the top of an affected file. </p> </li> 157 158</ul> 159 160<h2 id="bugs-fixed">Bugs fixed:</h2> 161 162<ul> 163 164 <li> <p><code>Hol_datatype</code> would fail if called on to define 165 a type with a single nullary constructor.</p></li> 166 167<li> <p><code>pred_setLib.UNION_CONV</code> (and other functions in this 168 library) failed to work as advertised. (Thanks to Lockwood Morris 169 for the report of this bug.)</p></li> 170 171<li> <p>It was too easy to do significant parser things before a 172 <code>new_theory</code> declaration, causing these effects not to 173 persist with the export of the theory. Now, attempting to do this 174 causes a strong warning to be issued.</p></li> 175 176<li> <p><code>let</code> terms with bodies that were abstractions didn’t 177 print correctly.</p></li> 178 179<li> <p>The type grammar didn’t print stored type abbreviations 180 correctly.</p></li> 181 182<li> <p> Adding a user-supplied pretty-printer caused polymorphic terms to 183 fail to print. (The interface for adding pretty-printers is also 184 now slightly richer, see the REFERENCE manual for details.) 185 </p></li> 186 187<li> <p><code>DECIDE_TAC</code> didn’t pay attention to goal 188 assumptions.</p></li> 189 190<li> <p>A bug in <code>ARITH_CONV</code>’s handling of conditional 191 expressions caused some quantified goals to fail to be proved.</p></li> 192 193<li> <p> The lexer got confused if a token made up of non-aggregating 194 characters (e.g., including ";") was used, but not as part of 195 special concrete syntax. I.e., <code>;;</code> was OK as an 196 infix, but not as a normal constant. (Thanks to Klaus Schneider 197 for the report of this bug.)</p></li> 198 199<li> <p><code>SPEC_VAR</code> and theory export caused bound variables 200 with the same name as constants to get changed. (Thanks to 201 Lockwood Morris for the report of this bug.)</p></li> 202 203<li> <p> Many, many documentation typos and bugs were fixed. (Thanks to 204 Carl Witty for the report of most of these.)</p></li> 205 206<li> <p> Two fixes for the simplifier’s implementation of congruence rules. 207 With deep nesting, congruence rules could lead to an exponential 208 increase in time taken. Also, terms that included variables used 209 in a rule’s statement could cause the rule to fail to fire.</p></li> 210 211<li> <p>The simplifier’s AC-rewriting could cause it to go into an 212 infinite loop. While the new behaviour does AC-normalise 213 everywhere (we hope!), it is not necessarily the same as the old 214 behaviour on examples which used to work. (Thanks to Tobias Nipkow 215 for useful discussion about this bug.)</p></li> 216 217<li> <p> <code>pairLib.PAIRED_ETA_CONV</code> was broken. Thanks to 218 Viktor Sabelfeld for the bug report.</p> </li> 219 220<li> <p> <code>Q.UNDISCH_THEN</code> was behaving more as if it were 221 <code>Q.PAT_UNDISCH_THEN</code>; it was finding matches in the 222 assumptions rather than equal terms. Thanks to Lockwood Morris 223 for the bug report. </p> </li> 224 225<li> <p> The order in which type arguments appeared as arguments to 226 polymorphic type operators defined by <code>Hol_datatype</code> 227 was previously undefined. For example, if one wrote:</p> 228<pre> 229 Hol_datatype `sum = left of 'a | right of 'b`; 230</pre> 231 <p> it was not specified that <code>('a,'b)sum</code> was the type 232 which associated the variable <code>'a</code> with the 233 <code>left</code> constructor. Now, the type picks up the type 234 variable arguments in <code>Hol_datatype</code> in alphabetical 235 order. <em>This may break code that relied on what was an 236 unspecified behaviour.</em></p></li> 237 238<li><p> The quotation filter didn’t recognise text of the form</p> 239<pre> 240 ``: 241 foo 242 `` 243</pre> 244 <p> with a newline immediately following the colon as a type 245 quotation. (Thanks to Steve Brackin for the report of this bug.) 246 </p> 247</li> 248 249 250</ul> 251 252 253<h2 id="new-theories">New theories:</h2> 254<ul> 255<li> <p> A theory of co-inductive (possibly infinite) labelled transition 256 paths in <code>pathTheory</code>. </p> </li> 257<li> <p> A theory of sorting and list permutations in 258 <code>sortingTheory</code>. </p> </li> 259</ul> 260 261<h2 id="new-tools">New tools:</h2> 262 263<ul> 264 265 <li> <p> A new first-order proof tactic (called 266 <code>METIS_TAC</code>) that uses ordered resolution and 267 paramodulation, specifically tailored for subgoals that require 268 equality reasoning.</p></li> 269 270<li> <p> A ‘boolification’ tool that automatically defines 271 functions that map datatypes to boolean vectors. These kind of 272 functions are needed for sending HOL subgoals to a model-checker 273 or SAT solver.</p></li> 274</ul> 275 276<h2 id="new-examples">New examples:</h2> 277<ul> 278<li> <p> An extension of the existing lambda calculus example 279 (examples/lambda) to include mechanisations of chapters 2 & 3 of 280 Hankin’s lambda calculus text, and the standardisation theorem 281 from Barendregt’s chapter 11.</p></li> 282 283<li> <p> A formalization of the probabilistic guarded command language 284 (pGCL) in higher-order logic, including a tool for deriving 285 sufficient verification conditions for partial correctness.</p></li> 286</ul> 287 288<h2 id="incompatibilities">Incompatibilities:</h2> 289 290<ul> <li> <p> The four HOL executables have had their names adjusted. 291We now think that using HOL with the quotation filter is the 292appropriate default for all users. To reflect this, the executable 293<code>hol</code> now includes the quotation filter. (This executable 294used to be called <code>hol.unquote</code>.) To avoid using the 295quotation filter, use <code>hol.noquote</code>. Analogous changes 296have been made to <code>hol.bare</code>; <em>i.e.,</em> 297<code>hol.bare</code> now includes the filter, and 298<code>hol.bare.noquote</code> does not. </p></li> 299 300<li> <p> The rewrite theorem for <code>LET</code>, </p> 301<pre> 302 LET f v = f v 303</pre> 304<p> has been removed from <code>std_ss</code> and later simplification 305 sets. (Simpsets <code>arith_ss</code>, <code>list_ss</code> and 306 <code>srw_ss()</code> are all affected.)</p> 307 <p> Old behaviours can be restored with code such as </p> 308<pre> 309 val std_ss = std_ss ++ simpLib.rewrites [LET_THM] 310</pre> 311</li> 312 313<li> <p>Rewrite rules for <code>arithmeticTheory</code>’s 314 <code>MIN</code> and <code>MAX</code> constants have been made 315 more general; they will now match more often. For example, 316 <code>MIN_LE</code> has changed from</p> 317<pre> 318 m <= MIN m n = m <= n 319</pre> 320 to 321<pre> 322 p <= MIN m n = p <= m /\ p <= n 323</pre></li> 324 325<li> <p>For reasons of efficiency, all conversions in the system may now 326 potentially raise the special exception 327 <code>Conv.UNCHANGED</code> to indicate that they haven’t changed 328 the input term, and that they should be treated as if they had 329 returned the theorem <code>|- t = t</code>, for 330 input <code>t</code>. Conversion connectives (such as 331 <code>THENC</code>, <code>ORELSEC</code> and 332 <code>TRY_CONV</code>) all do the appropriate thing in the 333 presence of this exception. Previously, sub-systems such as the 334 simplifier, rewriter and arithmetic decision procedures have used 335 this idea to make them work faster, but couldn’t share information 336 about unchangedness.</p> 337 338<p> For interactive use, <code>CONV_RULE</code> and 339 <code>CONV_TAC</code> handle the exception appropriately, and the 340 new function <code>QCONV</code> (of type 341 <code>: conv -> conv</code>) can make any 342 conversion handle <code>UNCHANGED</code>. <code>QCONV</code>’s 343 implementation is</p> 344<pre> 345 fun QCONV c t = c t handle UNCHANGED => REFL t 346</pre> 347 348 If you have code implementing conversions of your own, you may 349 need to fix code if it uses the following idiom: 350<pre> 351 fun myconv t = 352 let val th = someconv t 353 val .. = <fiddle with th> 354 in 355 <resulting theorem> 356 end 357</pre> 358 359 If <code>someconv</code> raises <code>UNCHANGED</code>, then 360 <code>myconv</code> will too, causing expressions such as 361 362<pre> 363 myconv THENC <something else> 364</pre> 365 366 <p> to treat <code>myconv</code> as if it hadn’t done anything 367 (because the <code><fiddle with th></code> code 368 never got called).</p> 369 370 <p>This can be relatively difficult to track down, but the fix is 371 simple enough: change <code>someconv t</code> to 372 <code>QCONV someconv t</code>.</p></li> 373 374<li> <p> The constant <code>LIST_TO_SET</code> is now defined in 375 <code>listTheory</code>.</p></li> 376 377<li> <p> The <code>word32</code> theory is not built by default. 378 Instead, a general <code>word</code><em>n</em>-theory creating 379 executable, <code>mkword.exe</code> is available in the 380 <code>hol/bin/</code> directory. This can be invoked to create 381 word theories of various sizes. For example,</p> 382<pre> 383 $ mkword.exe 32 384</pre> 385 <p> will create a <code>word32Theory</code> in the current 386 directory. These new theories don’t have corresponding 387 <code>Script</code> files, so <code>Holmake</code> doesn’t 388 automatically update these theories. If this is a concern, the 389 <code>Holmakefile</code> in 390 <code>hol/src/n_bit/help/Holmakefile.example-32</code> demonstrates how to 391 ensure word theories are rebuilt.</p></li> 392 393<li> <p> The type <code>simpLib.ssdata</code> is now called 394 <code>simpLib.ssfrag</code> and the constructor for this type that 395 used to be called <code>SIMPSET</code> is now called 396 <code>SSFRAG</code>.</p> </li> 397 398</ul> 399 400 401<hr /> 402 403<p> <em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-3</a></em> </p> 404 405</body> </html> 406