1<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN"> 2<html> 3<head> 4<meta http-equiv="content-type" 5 content="text/html ; charset=UTF-8"> 6<title>Release Notes for Kananaskis-5 version of HOL 4</title> 7<style type="text/css"> 8<!-- 9 body {color: #333333; background: #FFFFFF; 10 margin-left: 1em; margin-right: 1em } 11 code, pre {color: #660066; font-weight: bold; /* font-size: smaller */} 12--> 13</style> 14 15</head> 16 17<body> 18<h1>Notes on HOL 4, Kananaskis-5 release</h1> 19 20<p> We are pleased to announce the release of the latest HOL4 system. We 21believe there are a number of exciting new features (runs on Poly/ML, 22looks prettier thanks to Unicode support), as well as the usual bug 23fixes.</p> 24 25<!-- maybe announce HOL-�� here --> 26<p> A new version of the HOL4 theorem prover is also now available, 27called HOL-Omega (or HOL<sub>��</sub>). While backwards compatible, 28the HOL-Omega theorem prover implements a more powerful logic, capable 29of modelling concepts not expressible in normal higher order logic, 30such as monads and concepts from category theory. See 31the <a href="#new-versions">New versions</a> section below for more. 32</p> 33 34<h2 id="contents">Contents</h2> 35<ul> 36 <li> <a href="#new-features">New features</a> </li> 37 <li> <a href="#bugs-fixed">Bugs fixed</a> </li> 38 <li> <a href="#new-theories">New theories</a> </li> 39 <li> <a href="#new-tools">New tools</a> </li> 40 <li> <a href="#new-examples">New examples</a> </li> 41 <li> <a href="#new-versions">New versions</a> </li> 42 <li> <a href="#incompatibilities">Incompatibilities</a> </li> 43</ul> 44 45 46 47<h2 id="new-features">New features:</h2> 48 49<ul> 50<li> <p> There is now a <a href="http://polyml.org">Poly/ML</a> 51implementation of HOL4 available for users on platforms other than 52Windows. Users should build from the same source-tree, and have 53version 5.2 of Poly/ML installed. The build process is similar. 54Start with </p> 55<pre> 56 poly < tools/smart-configure.sml 57</pre> 58<p> Continue with </p> 59<pre> 60 bin/build 61</pre> 62<p>Most of the features of the Moscow ML implementation should work in 63the Poly/ML version, but as it is still rather young, users may 64encounter some rough edges. The advantage of the Poly/ML 65implementation is that it is considerably quicker than the Moscow ML 66implementation. Many thanks to Scott Owens for doing most of the work 67on this port.</p></li> 68 69<li id="syntactic-patterns"><p>Overloading can now target ���syntactic 70patterns���, which are terms other than just constants. Typically a 71pattern will be a lambda-abstraction. For example, one can overload 72the symbol <code><></code> (meant to represent ���not equal to���) 73to the term <code>(\x y. ~(x = y))</code>. The call would be </p> 74<pre> 75 overload_on ("<>", ``\x y. ~(x = y)``) 76</pre> 77<p> It is then possible to write terms such 78as <code>``<> a 3``</code>. This will actually 79translate to the term <code>``~(a = 3)``</code> internally. 80Pretty-printing will reverse the transformation so that what was typed 81will also be printed. (One can check that the term really has been 82translated as desired with calls to term destructors 83like <code>dest_term</code> and <code>strip_comb</code>.) </p> 84 85<p>Of course, in the case of <code><></code>, one would want 86this as an infix. To do this one would use <code>set_fixity</code> as 87usual. In this case, </p> 88<pre> 89 set_fixity "<>" (Infix(NONASSOC, 450)) 90</pre> 91<p> would be appropriate. (See 92the <a href="#incompatibilities">Incompatibilities section</a> below 93on the change to the associativity of grammar level 450.)</p> 94 95<p>Finally, overloading can be type-specific. In this way, the 96default system now overloads the ASCII <code><=></code> to 97equality over the booleans. Various operators over strings now use 98the same technology as well (see 99<a href="#strings-as-charlists">below</a>). </p> 100 101<p>The system has syntactic patterns built-in for not-equal (as 102above), iff (the <code><=></code> symbol), not-iff 103(<code><=/=></code>), and not-an-element-of 104(<code>NOTIN</code>). The Unicode variants 105(see <a href="#unicode">later item</a>) for these 106are <code>���</code>, <code>���</code>, <code>���</code>, 107and <code>���</code>. </p></li> 108 109<li id="strings-as-charlists"><p>The <code>:string</code> type is now 110an alias for <code>:char list</code>, meaning that strings inherit all 111of the list operations ���for free���. Existing string operators that are 112effectively duplicates of operations on lists 113(like <code>STRLEN</code> and <code>STRCAT</code>) are now 114type-specific overloads of the list constants.</p> 115 116<p>Note that this means that the <code>IMPLODE</code> 117and <code>EXPLODE</code> functions are now identities, and that 118theorems that used to print as </p> 119<pre> 120 ��� STRLEN s = LENGTH (EXPLODE s) 121</pre> 122<p> are still true, but are now looping rewrites. 123(The <code>STRLEN</code> in the theorem is the same term as 124the <code>LENGTH</code>, and in fact the theorem (now 125called <code>STRLEN_EXPLODE_THM</code>) prints 126with <code>STRLEN</code> in both positions.)</p> 127 128<p>The <code>EXPLODE</code> and <code>IMPLODE</code> constants are 129still useful if theorems are to be exported to ML, where strings are 130not the same type as lists of characters.</p> 131</li> 132 133<li> <p> Types can now be numerals, as long as <code>fcpTheory</code> 134(the theory of finite cartesian products) is loaded. A numeral type 135has no interesting properties except that the cardinality of its 136universe has exactly the size given by the numeral. This implies that 137negative number types and the type :0 do not exist. The 138pretty-printing of numeral types can be turned off with the trace 139flag <code>pp_num_types</code>. </p> 140 141<p> This removes the need for type abbreviations <code>i32</code> and 142others, and also the function <code>fcpLib.mk_index_type</code>, which 143has been removed. </p></li> 144 145<li> <p> The finite cartesian product “array” type can now 146be written with square brackets rather than with the 147infix <code>**</code> operator. This combines well with the numeric 148types above. For example, <code>:bool[32]</code> is a type of 32 149booleans, and indeed is now the type used for what had been previously 150called <code>word32</code>. The pretty-printing of array types can be 151turned off with the trace flag <code>pp_array_types</code>. </p> 152 153<p> Unfortunately, because of lists, at the term level one can not 154index arrays with square brackets. Instead, we recommend the 155infix <code>'</code> operator (that���s an apostrophe, ASCII character 156#39). For example, <code>array ' 3</code> is the value of the fourth 157element of <code>array</code> (indexing starts at zero!)</p> 158</li> 159 160<li> <p> Errors in inductive relation definitions (made 161with <code>Hol_reln</code>) are now accompanied by better location 162information. </p></li> 163 164<li> <p> Errors in quotient type definitions (made with entry-points 165in <code>quotientLib</code>) are now accompanied by better 166diagnostics about problems like missing respectfulness results.</p></li> 167 168<li><p> If HOL is started in a directory with 169<code>INCLUDES</code> specified in a <code>Holmakefile</code>, then 170those same includes are put onto the <code>loadPath</code> that is 171used interactively. This should help interactive debugging of 172multiple-directory developments.</p> 173 174<p>If <code>Holmake</code> is run in a directory 175with <code>INCLUDES</code> specified in a <code>Holmakefile</code>, 176then it will call itself recursively in those directories before 177working in the current directory. This behaviour can be prevented by 178using the <code>--no_prereqs</code> option on the command-line, or by 179including <code>NO_PREREQS</code> as an <code>OPTION</code> in 180the <code>Holmakefile</code>.</p> 181</li> 182 183<li> <p> The <code>tautLib</code> decision procedure for propositional 184 logic now uses external SAT solvers (through 185the <code>HolSatLib</code> code) for all but the smallest goals, 186translating proofs back through the HOL kernel.</p></li> 187 188<li> <p> In the Emacs mode: provide a new option to the 189work-horse <code>M-h M-r</code> command: if you precede it by 190hitting <code>C-u</code> twice, it will 191toggle <code>quietdec</code> around what is to be pasted into the HOL 192session. This can be useful if you���re opening a whole slew of big 193theories and don���t want to have to watch grammar guff scroll 194by.</p></li> 195 196<li> <p> The termination prover under <code>Define</code> is now 197smarter. It now does a better job of guessing termination relations, 198using a relevance criterion to cut down the number of lexicographic 199combinations that are tried. It can handle <code>DIV</code> 200and <code>MOD</code> now, through the <code>termination_simps</code> 201variable, which can be added to in order to support other destructor 202functions.</p> 203 204<p> Termination proofs for functions defined recursively over words 205are also supported. The system knows about subtracting 1 and also 206right-shifting. </p></li> 207 208<li> <p> Post processing for word parsing is supported with the function:</p> 209<pre> 210 wordsLib.inst_word_lengths : term -> term 211</pre> 212<p> 213When possible, word lengths are guessed for the extract and 214concatenate functions. That is, <code>``(a >< b) w``</code> is given 215type <code>``:(a+1-b) word``</code> and <code>``(a: a word) @@ (b: b word)``</code> is 216given type <code>``:(a + b) word``</code>.</p> 217 218<p>For example:</p> 219<pre> 220 - val _ = Parse.post_process_term := wordsLib.inst_word_lengths; 221 - ``(3 >< 0) a @@ (7 >< 4) a @@ (16 >< 8) a``; 222 <<HOL message: inventing new type variable names: 'a, 'b, 'c, 'd, 'e, 'f>> 223 <<HOL message: assigning word length(s): 'a <- 4, 'b <- 13, 'c <- 17, 'e <- 4 and 'f <- 9>> 224 > val it = ``(3 >< 0) a @@ (7 >< 4) a @@ (16 >< 8) a`` : term 225</pre> 226<p> 227The assignment message is controlled by the trace variable 228<code>"notify word length guesses"</code>.</p> 229</li> 230 231<li> 232<p> <code>wordsLib</code> now supports evaluation over non-standard 233word-sizes:</p> 234<pre> 235 - load "wordsLib"; 236 > val it = () : unit 237 - EVAL ``123w + 321w:bool[56]``; 238 > val it = |- 123w + 321w = 444w : thm 239</pre> 240<p>Non-standard word sizes will evaluate more slowly when first used. 241However, size theorems are then added to the compset, so subsequent 242evaluations will be quicker. 243</p></li> 244 245<li id="unicode"> 246<p> HOL now supports Unicode symbols as part of its parsing and 247printing. In addition, there are now appropriate Unicode symbols, 248such as <code>���</code> and <code>���</code> built in to the system. To 249enable their printing and parsing, you must set the trace 250variable <code>Unicode</code>. If this is done, you will see, for 251example</p> 252<pre> 253 - FORALL_DEF; 254 > val it = |- $��� = (��P. P = (��x. T)) : thm 255</pre> 256<p> If you turn Unicode on, and see gibberish when you print terms and 257theorems, your fonts and system are not Unicode and UTF-8 compatible. 258Emacs versions past 22 can be made to work, as can normal shells on 259MacOS and Linux. The latest versions of Emacs on Windows support 260UTF-8, and so running HOL inside Emacs on Windows gives a pleasant 261Unicode experience there too. </p> 262 263<p>The <code>Unicode</code> trace controls the use of Unicode symbols 264that are set up as explicit alternatives for ASCII equivalents. To 265set up such an aliasing, use the function</p> 266<pre> 267 Unicode.unicode_version : {u:string,tmnm:string} -> unit 268</pre> 269<p> where the string <code>u</code> is the Unicode, and 270where <code>tmnm</code> is the name of the term being aliased. Note 271that you can also alias the names of syntactic patterns 272(<a href="#syntactic-patterns">see above</a>). </p> 273<p> You are also free to use the standard grammar manipulation 274functions to define pretty Unicode syntax that has no ASCII equivalent 275if you wish, and this can be done whether or not 276the <code>Unicode</code> trace is set.</p> 277</li> 278 279<li> 280 <p> A new function <code>limit</code>:</p> 281<pre> 282 limit : int -> simpset -> simpset 283</pre> 284 <p> can be used to limit the number of rewrites a simpset applies. 285 By default a simpset will allow the simplifier to apply as many 286 rewrites as match, possibly going into an infinite loop thereby. 287 The <code>limit</code> function puts a numeric limit on this, 288 usually guaranteeing the simplifier���s termination (it will still 289 loop if a user-provided conversion or decision procedure loops).</p> 290</li> 291 292<li id="unary-minus"> 293<p> Operators (<i>e.g.</i> <code>&</code> and <code>-</code>) can 294now be both prefix and infix operators simultaneously. In particular, 295the subtraction operator (<code>-</code>) is now also a prefix in all 296theories descended from <code>arithmetic</code>. In order to use this 297as a negation, you must overload the 298string <code>"numeric_negate"</code>, which is the abstract syntax 299name of the unary minus. Thus, in <code>integerTheory</code>, the 300line </p> 301<pre> 302 val _ = overload_on("numeric_negate", ``int_neg``) 303</pre> 304<p>sets up unary minus as a symbol for negation over the integers.</p> 305 306<p>This change allows one to input terms such 307as <code>``-x + y``</code> even in the theory of natural 308numbers. In this context, the unary negation maps to a variable 309called <code>numeric_negate</code>, which is unlikely to be helpful. 310Luckily, the variable will likely be polymorphic and the warning about 311invention of type variables will serve as a clue that something 312dubious is being attempted.</p> 313 314<p>In the existing numeric theories, we have kept <code>~</code> as a 315unary negation symbol as well (following SML���s example), but the 316unary minus is now the preferred printing form.</p> 317 318<p>If you wish to add an existing binary operator as a prefix, it is 319important that you <em>not</em> use the <code>set_fixity</code> 320command to do it. This command will clear the grammar of your binary 321operator before adding the unary one. Better to 322use <code>add_rule</code> (for which, see the Reference Manual). This 323will also allow you to map the unary form to a different name. With 324subtraction, for example, the binary operator maps to the 325name <code>"-"</code>, and the unary operator maps 326to <code>"numeric_negate"</code>.</p> 327 328<p>Finally, note that in the HOL language, unary minus and binary 329minus are inherently ambiguous. Is <code>x-y</code> the application 330of binary minus to arguments <code>x</code> and <code>y</code>, or is 331it the application of function <code>x</code> to 332argument <code>-y</code>? In this situation, the implementation of 333this feature treats these dual-purpose operators as infixes by 334default. In order to obtain the second reading above, one has to 335write <code>x(-y)</code>. </p> 336 337<p>(<a href="#unary-minus-incompat">See below</a> for discussion of 338the backwards incompatibility this causes to users of 339the <code>words</code> theory.)</p> 340</li> 341 342<li> 343<p>It is now possible to use the simplifier to rewrite terms with 344respect to arbitrary pre-orders. The entry-point is the function</p> 345<pre> 346 simpLib.add_relsimp : 347 {trans: thm, refl: thm, subsets: thm list, 348 rewrs: thm list, weakenings: thm list} -> 349 simpset -> simpset 350</pre> 351<p>where the <code>trans</code> and <code>refl</code> fields are the 352theorems stating that some relation is a pre-order. 353The <code>weakenings</code> field is a list of congruences justifying 354the switch from equality reasoning to reasoning over the pre-order. 355For example, all equivalences (<code>���</code>, say) will have the 356following be true 357</p> 358<pre> 359 |- (M1 ��� M2) ==> (N1 ��� N2) ==> ((M1 ��� N1) <=> (M2 ��� N2)) 360</pre> 361<p>With the above installed, when the simplifier sees a term of the 362form <code>M1 ��� N1</code> it will rewrite both sides using 363the relation <code>���</code>.</p> 364<p>See the Description manual���s section on the simplifier for more.</p> 365 366</li> 367 368</ul> 369 370<h2 id="bugs-fixed">Bugs fixed:</h2> 371 372<ul> 373<li> <code>EVAL ``BIGUNION {}``</code> now works.</li> 374 375<li> <p> Fixed a subtle bug in termination condition extraction, 376whereby multiple <code>let</code>-bindings for a variable would 377cause <code>Define</code> to be unpredictable and sometimes broken. 378Now variables get renamed in order to make the definition process 379succeed. </p></li> 380 381<li> <p> <code>ASM_MESON_TAC</code> (which lives 382beneath <code>PROVE_TAC</code>) now properly pays attention to the 383controlling reference variable <code>max_depth</code>.</p></li> 384 385<li><p> Fixed an error in the build process when 386building <code>mlyacc</code> from sources on Windows.</p></li> 387 388</ul> 389 390 391<h2 id="new-theories">New theories:</h2> 392<ul> 393<li>A theory of Patricia trees, due to Anthony Fox.</li> 394</ul> 395 396<h2 id="new-tools">New tools:</h2> 397 398<ul> 399<li>A new library <code>HolSmtLib</code> provides an oracle interface 400to external SMT solvers. 401</li> 402 403<li><p>There are a number of new facilities in <code>wordsLib</code>. 404The main additions are:</p> 405 406<dl> 407<dt><code>WORD_ss</code>:</dt> <dd> Does some basic simplification, 408evaluation and AC rewriting 409(over <code>*</code>, <code>+</code>, <code>&&</code> 410and <code>!!</code>). For example, 411<pre> 412 ``a * 3w + a`` --> ``4w * a`` 413</pre> 414and 415<pre> 416 ``a && 3w !! a && 2w`` --> ``3w && a`` 417</pre></dd> 418 419<dt><code>BIT_ss</code>:</dt> <dd>For example, <code>``BIT n 3`` --> ``n IN {0; 1}``</code></dd> 420 421<dt><code>WORD_MUL_LSL_ss</code>:</dt> 422<dd>Converts multiplications to left-shifts e.g. 423 <code>``2w * a`` --> ``a << 1``</code></dd> 424 425<dt><code>WORD_BIT_EQ_ss</code>:</dt> 426<dd>Can be used to establish bit-wise (in)equality <i>e.g.</i> 427 <code>``a && ~a = 0w`` --> ``T``</code> 428Does not work with <code>*</code>, <code>+</code> <i>etc.</i></dd> 429 430<dt><code>WORD_ARITH_EQ_ss</code>:</dt> 431<dd> Can be used to establish arithmetic (in)equality <i>e.g.</i> 432 <code>``~(b + 1w = b + 4294967295w:word32)`` --> ``T``</code> 433</dd> 434 435<dt><code>WORD_EXTRACT_ss</code>:</dt> 436<dd> 437Simplification for shifts and bit extraction. 438Simplifies <code>--</code>, <code>w2w</code>, <code>sw2sw</code>, <code>#>></code>, <code>@@</code> <i>etc.</i> and expresses operations 439 using <code>><</code>, <code><<</code> and <code>!!</code>.</dd> 440 441<dt><code>WORD_DECIDE</code>:</dt> 442<dd>A decision procedure. Will solve Boolean (bitwise) problems 443 and some problems over <, <+ etc.</dd> 444</dl> 445</li> 446</ul> 447 448<h2 id="new-versions">New versions:</h2> 449 450<ul> 451<li> 452<p> 453The HOL-Omega or HOL<sub>��</sub> system presents a more powerful version 454of the widely used HOL theorem prover. This system implements a new logic, 455which is an extension of the existing higher order logic of HOL4. The logic 456is extended to three levels, adding kinds to the existing levels of types 457and terms. New types include type operator variables and universal types 458as in System F. Impredicativity is avoided through the stratification of 459types by ranks according to the depth of universal types. The HOL-Omega 460system is a merging of HOL4, HOL2P by Völker, and major aspects of 461System F<sub>��</sub> from chapter 30 of 462<i>Types and Programming Languages</i> by Pierce. 463As in HOL4, HOL-Omega was constructed according to the design principles 464of the LCF approach, for the highest degree of soundness. 465</p> 466 467<p> 468The HOL-Omega system is described in the paper 469<a href="http://www.trustworthytools.com/holw/holw-lncs5674.pdf"><i>The HOL-Omega Logic</i></a>, 470by Homeier, P.V., in Proceedings of TPHOLs 2009, LNCS vol. 5674, pp. 244-259. 471The paper presents the abstract syntax and semantics for the ranks, kinds, 472types, and terms of the logic, as well as the new fundamental axioms 473and rules of inference. It also presents examples of using the HOL-Omega 474system to model monads and concepts from category theory such as functors 475and natural transformations. As an example, 476here is the definition of functors, as a type abbreviation and a term predicate: 477</p> 478 479<pre> 480 (*--------------------------------------------------------------------------- 481 Functor type abbreviation 482 ---------------------------------------------------------------------------*) 483 484 val _ = type_abbrev ("functor", Type `: \'F. !'a 'b. ('a -> 'b) -> 'a 'F -> 'b 'F`); 485 486 (*--------------------------------------------------------------------------- 487 Functor predicate 488 ---------------------------------------------------------------------------*) 489 490 val functor_def = new_definition("functor_def", Term 491 `functor (F': 'F functor) = 492 (* Identity *) 493 (!:'a. F' (I:'a->'a) = I) /\ 494 (* Composition *) 495 (!:'a 'b 'c. !(f:'a -> 'b) (g:'b -> 'c). 496 F' (g o f) = F' g o F' f) 497 `); 498</pre> 499 500<p> 501The HOL-Omega implementation may be downloaded by the command</p> 502<pre> 503 svn checkout https://hol.svn.sf.net/svnroot/hol/branches/HOL-Omega 504</pre> 505<p>Installation instructions are in the top directory. 506HOL-Omega may be built using either the standard or the experimental kernel, 507and either Moscow ML or Poly/ML, by the same process as for HOL4. 508This implementation is still in development but is currently useful. 509This provides a practical workbench for developments in the HOL-Omega 510logic, integrated in a natural and consistent manner with the existing HOL4 511tools and libraries that have been refined and extended over many years. 512Examples using the new features of HOL-Omega may be found in the directory 513<code>examples/HolOmega</code>. 514</p> 515 516<p> 517This implementation was designed with particular concern for backward 518compatibility with HOL4. This was almost entirely achieved, which was 519possible only because the fundamental data types representing types and 520terms were originally encapsulated. This meant that the underlying 521representation could be changed without affecting the abstract view of 522types and terms by the rest of the system. Virtually all existing HOL4 523code will build correctly, including the extensive libraries. 524The simplifiers have been upgraded, including higher-order matching of 525the new types and terms and automatic type beta-reduction. Algebraic 526types with higher kinds and ranks may be constructed using the familiar 527<code>Hol_datatype</code> tool. Not all of the tools will work as 528expected on the new terms and types, as the revision process is ongoing, 529but they will function identically on the classic terms and types. 530So nothing of HOL4���s existing power has been lost. 531</p> 532 533<p> 534More information may be found at 535<a href="http://www.trustworthytools.com">http://www.trustworthytools.com</a>. 536</li> 537</ul> 538 539<h2 id="new-examples">New examples:</h2> 540 541<ul> 542<li><p><code>examples/machine-code</code> contains a development of 543verified Lisp implementations on top of formal models of hardware 544instruction sets for the ARM, PowerPC and x86 chips. This is work 545done by Magnus Myreen. <strong>Note:</strong> This 546example <em>must</em> be built with Poly/ML. </p></li> 547 548 549<li> <p> <code>examples/hol_dpllScript.sml</code> contains a very 550simplistic HOL implementation of DPLL with unit propagation, with 551proofs of termination, completeness and soundness. </p> </li> 552 553<li><p><code>examples/misc/PropLogicScript.sml</code> contains 554soundness and completeness results for a classical propositional 555logic.</p></li> 556 557<li><p>A formalisation of Symbolic Trajectory Evaluation, contributed 558by Ashish Darbari.</p></li> 559 560</ul> 561 562<h2 id="incompatibilities">Incompatibilities:</h2> 563 564<ul> 565 566<li><p> The <code>emacs</code> mode is now found in the 567 file <code>tools/hol-mode.el</code> (rather 568 than <code>hol98-mode.el</code>) and all of the occurrences of the 569 string <code>hol98</code> there have been replaced 570 by <code>hol</code>.</p> </li> 571 572<li> <p> The <code>muddy</code> code, and the packages that depend on it 573(<code>HolBdd</code> and <code>HolCheck</code>) have moved from 574the <code>src</code> directory into <code>examples</code>. If you 575wish to use any of these packages, you will now have to both build 576them (see below), and then explicitly include the directories in 577your <code>Holmakefile</code>s. For example, the following line at 578the top of a <code>Holmakefile</code> will give access 579to <code>HolBdd</code> (and its dependency, <code>muddy</code>):</p> 580<pre> 581 INCLUDES = $(protect $(HOLDIR)/examples/muddy) $(protect $(HOLDIR)/examples/HolBdd) 582</pre> 583<p> To build these libraries: </p> 584<ol> 585<li> On Windows, copy <code>tools\win-binaries\muddy.so</code> 586to <code>examples\muddy\muddyC</code>. On other platforms, 587type <code>make</code> in <code>examples/muddy/muddyC</code>.</li> 588<li> Do <code>Holmake</code> in <code>examples/muddy</code>.</li> 589<li> Do <code>Holmake</code> in <code>examples/HolBdd</code>.</li> 590<li> Do <code>Holmake</code> in <code>examples/HolCheck</code>.</li> 591</ol> 592 593<p> On 64-bit Unices, users report having to add 594the <code>-fPIC</code> option to the <code>CFLAGS</code> variable 595at</p> 596<ul> 597<li> <code>src/muddy/muddyC/Makefile</code> 598 <li> <code>src/muddy/muddyC/buddy/config</code> 599</ul> 600 601 602</li> 603 604<li> <p>The <code>FIRSTN</code> and <code>BUTFIRSTN</code> constants from 605the theory <code>rich_list</code> are now defined in the 606theory <code>list</code>, with names <code>TAKE</code> 607and <code>DROP</code>. If you load <code>rich_listTheory</code>, then 608the old names are overloaded so that parsing existing theories should 609continue to work. The change may cause pain if you have code that 610expects the constants to have their old names (for a call 611to <code>mk_const</code> say), or if you have variables or constants 612of your own using the names <code>TAKE</code> 613and <code>DROP</code>.</p> 614 615<p>Similarly, the <code>IS_PREFIX</code> constant 616from <code>rich_listTheory</code> is now actually an overload to a 617pattern referring to the constant <code>isPREFIX</code> 618in <code>listTheory</code> (this was the name of the corresponding 619constant in <code>stringTheory</code> 620(see <a href="#strings-as-charlists">above</a>). The new constant 621takes its arguments in the reverse order (smaller list first), and 622prints with the infix symbol <code><<=</code>. The 623quotation <code>`IS_PREFIX l1 l2`</code> will produce a term 624that prints as <code>``l2 <<= l1``</code>, preserving the 625appropriate semantics. (The Unicode symbol for this infix 626is <code>���</code>.)</p> 627</li> 628 629<li> <p> The <code>SET_TO_LIST</code> constant is now defined 630in <code>listTheory</code> (moved from <code>containerTheory</code>), 631which now depends on the theory of sets (<code>pred_setTheory</code>). 632The <code>LIST_TO_SET</code> constant is now also overloaded to the 633easier-to-type name <code>set</code>. A number of theorems about both 634functions are now in <code>listTheory</code>, and because the theory 635of lists depends on that of sets, so too does the standard HOL 636environment loaded by <code>bossLib</code>. All of the theorems 637from <code>containerTheory</code> are still accessible in the same 638place, even though they are now just copies of theorems proved 639in <code>listTheory</code>.</p> 640 641<p>If the presence of a constant called <code>set</code> causes pain 642because you have used the same string as a variable name and don���t 643wish to change it, the constant can be hidden, and the interference 644halted, by using <code>hide</code>:</p> 645<pre> 646 hide "set"; 647</pre> 648</li> 649 650<li><p>The <code>parse_in_context</code> function (used heavily in 651the <code>Q</code> structure) is now pickier about its parses. Now 652any use of a free variable in a quotation that is parsed must be 653consistent with its type in the provided context.</p></li> 654 655<li><p>The user-specified pretty-printing functions that can be added 656to customise printing of terms (using <code>add_user_printer</code>), 657now key off term patterns rather than types. Previously, if a term 658was of a the type specified by the user, the user���s function would be 659called. Now, if the term matches the provided pattern, the function 660is called. The old behaviour can be emulated by simply giving as the 661pattern a variable of the desired type.</p> 662 663<p>Additionally, the user���s function now gets access to a richer 664context of arguments when the system printer calls it.</p> 665 666</li> 667 668<li> <p>Precedence level 450 in the standard term grammar is now 669non-associative, and suggested as an appropriate level for binary 670relations, such as <code>=</code>, <code><</code> 671and <code>���</code>. The list cons operators <code>::</code> has moved 672out of this level to level 490, and the <code>++</code> operator used 673as a shorthand for list concatenation (<code>APPEND</code>) has moved 674to 480. (This preserves their relative positioning.) 675</p></li> 676 677<li id="unary-minus-incompat"> 678<p> The <a href="#unary-minus">new feature allowing unary minus</a> 679causes the way unary minus was handled in <code>wordsTheory</code> to 680fail. There the unary minus (���twos complement��� in fact) could be 681accessed by writing things like <code>``$- 3w + x``</code>. One 682should now write <code>``-3w + x``</code>. If converting 683one���s script files is going to be too arduous, the old behaviour can 684be achieved by including the line</p> 685<pre> 686 val _ = temp_overload_on ("-", ``word_2comp``) 687</pre> 688<p>at the top of the given script file. </p> 689</li> 690 691</ul> 692 693 694 695 696<hr> 697 698<p> <em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-5</a></em> </p> 699 700</body> </html> 701