on github

HOL Frequently Asked Questions

Contents


Build Failures and Warnings

Poly/ML and HOL fail to build with recent Xcode on Apple Macs.

To build HOL on polyml 5.9.1 on MacOS M1, when the standard invocation fails with

  poly < tools/smart-configure.sml
  ...
  Making mllex
  ld: LINKEDIT overlap of start of LINKEDIT and symbol table in '/private/var/folders/k5/_29n92td6yqcvzm2pf69n1n40000gn/T/polyobj.8335.o' in '/private/var/folders/k5/_29n92td6yqcvzm2pf69n1n40000gn/T/polyobj.8335.o'
  clang: error: linker command failed with exit code 1 (use -v to see invocation)
  Failed to make mllex (Fail "Command failed")
The problem is in polyc. What to do:
  1. Build poly, except in the ./configure invocation, do

           $ LDFLAGS=-ld_classic ./configure
    
    After that, invoke make in polyml/. This creates file polyc
  2. Edit EXTRALDFLAGS in polyc

    
            LINK="g++"  # line 5
            LINKOPT="-std=gnu++11"  # new line 6
    
            EXTRALDFLAGS=-ld_classic # line 16
    

    Edit line 44 and 46 so those lines begin with

            "${LINK}" ${LINKOPT}
    
    instead of
            "${LINK}"
    

    Invoke

            make install
    
    as per usual.
  3. Add the line

            val EXTRA_POLY_LDFLAGS = ["-ld_classic"];
    

    to file

            tools-poly/poly-includes.ML
    
  4. Now you can build HOL via the usual invocation

    
           $ poly < tools/smart-configure.sml
           $ bin/build
    
I can’t build on Ubuntu (or some other recent Linux), where I have Moscow ML executables in /usr/bin/, and the Moscow ML library files in /usr/lib/.

If configure is not guessing the correct directories, you will need to write a config-override file in the root directory of the HOL installation, and put in it the line

    val mosmldir = "/usr/bin/"

You should then be able to run

    $ mosml < tools/smart-configure.sml

and

    $ bin/build

as normal.

Moscow ML is raising a Chr exception when trying to build my (large) theories!

This is a known problem in Moscow ML 2.01. There is a patch, and some instructions on how to apply it.

HOL is failing to complete the build process. It stops when trying to create the HolBdd theory. Why is this, and what should I do?

The problem is almost certainly that your copy of MoscowML hasn’t been built with dynamic linking correctly enabled. This in turn means that the Muddy BDD package that HolBdd uses can’t load. You can test that this is the problem by running hol, and then trying

    - load "HolBdd";

This should fail with an error message about not being able to load muddy.so.

If you decide you do want HolBdd (there is nothing else in HOL that depends on dynamic linking) you will probably need to build Moscow ML yourself. Binaries from the central site in Denmark don’t seem to work. However the install.txt file in the distribution does talk about things you need to do to binaries in order to get dynamic linking to work for them, and it would be interesting to hear that someone had got this to work. In any case, to build from sources, you must make sure that you alter the src/Makefile.inc in the MoscowML distribution in line with the instructions in the comments there.

This advice seems to solve this problem for 90% of the people reporting it. If it doesn’t in your case, please get back to us.

Should I be concerned by error messages during the build process?

Neither

   > File "Term.sml", line 1328, characters 10-42:
   > !   let val {const=Const(r1,_),theory,place} = const_decl name
   > !           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   > ! Warning: pattern matching is not exhaustive

nor the following sort of output, when configuring the system before building:

   > /local/scratch/kxs/144/bin/mosmlyac: 4 shift/reduce conflicts.

represent problems.

How do I stop Holmake from proving false theorems?!

The default behaviour of Holmake is to cause failing proofs (from calls to prove and store_thm) to be asserted as true with mk_thm (such results get oracle tags recording this fact). This behaviour allows for more of a script file to be checked because the first failing proof doesn’t abort the script.

If you don’want this behaviour, use the --qof (“quit on failure”) flag to Holmake, or use an OPTIONS = QUIT_ON_FAILURE line in a Holmakefile.

How do I build old versions of HOL, such as Taupo-6 and Kananaskis-1?

These versions of the system no longer build successfully because of the Overflow bug, caused by the fact that more than 230 seconds have passed since 1 January 1970.

In the file src/portableML/Portable.sml, replace the local-in-end block that defines mk_time, dest_time and some others with

    local open Time
          val two_30 = Math.pow(2.0, 30.0)
    in
      val timestamp : unit -> time = now
      val time_to_string : time -> string = toString
      fun dest_time t =
         let val adjusted = Real.-(toReal t, two_30)
             val sec = Real.trunc adjusted
         in
            {sec=sec, usec=0}
         end
      fun mk_time {sec,usec} = fromReal (Real.+(real sec, two_30))
      fun time_eq (t1:time) t2 = (t1 = t2)
      fun time_lt (t1:time) t2 = Time.<(t1,t2)
    end

(In Kananaskis-1 this is at line 89; in Taupo-6, it is at line 85.)

If you are using Windows, you will also have to upgrade to Moscow ML 2.01.

Holmake is being “M-KILLED” after theories have been built successfully!

This is a Poly/ML bug and seems to preponderantly affect Linux installations ; recent repository versions (later than 5.7.1) make the problem go away. Check the github page for Poly/ML for recent commits.


Parsing and Printing

HOL output is all garbled!

You are probably seeing mis-interpreted UTF8. You can either turn Unicode off, or fix the environment in which you are running HOL.

If you are using Emacs, you should add the following lines to your .emacs:

    (set-selection-coding-system 'utf-8)
    (set-next-selection-coding-system 'utf-8)
    (setq process-coding-system-alist '((".*" . utf-8)))

If you are using a Windows console, you might try issuing the command

    chcp 65001

before starting HOL. According to Albert Lai, one should be aware that even then, the console font lacks some pretty common symbols.

If you are using a Unix shell, you should make sure that your LANG environment variable includes the string UTF-8 as a suffix.

How do I turn Unicode off?

Use

    val _ = set_trace "Unicode" 0;

You can put this line into a .hol-config.sml file in your home directory in Kananaskis-6 and later.

How do I understand the output of term_grammar()?

The term_grammar() function returns the grammar controlling the parsing and printing of HOL terms. Its printed form doesn’t capture everything inside the grammar, but does provide a pretty good picture of what happens to your string when it’s parsed, and what happens to your term when it’s printed.

The first part of the grammar output is something that looks like:

   (0)    TM  ::=  "LEAST" <..binders..> "." TM |
                   "?!" <..binders..> "." TM | "?" <..binders..> "." TM |
                   "!" <..binders..> "." TM | "@" <..binders..> "." TM |
                   "\" <..binders..> "." TM
   (2)    TM  ::=  "let" TM "in" TM  [ _ let]
   (4)    TM  ::=  TM "::" TM (restricted quantification operator)
   (5)    TM  ::=  TM TM  (binder argument concatenation)
   (7)    TM  ::=  "case" TM "of" TM  [case__magic]
...
   (50)   TM  ::=  TM "," TM   (R-associative)
   (70)   TM  ::=  "if" TM "then" TM "else" TM  [COND]
   (80)   TM  ::=  TM ":-" TM   (non-associative)
   (100)  TM  ::=  TM "<=/=>" TM | TM "<=>" TM | TM "=" TM
                   (non-associative)
   (200)  TM  ::=  TM "==>" TM   (R-associative)
...
   (450)  TM  ::=  TM "<<=" TM | TM "PSUBSET" TM | TM "SUBSET" TM |
                   TM ">=" TM | TM "<=" TM | TM ">" TM | TM "<" TM |
                   TM "RSUBSET" TM | TM "<>" TM (non-associative)
   (460)  TM  ::=  TM "with" TM  [record update] | ... (R-associative)
   (480)  TM  ::=  TM "++" TM   (L-associative)
   (490)  TM  ::=  TM "::" TM  [CONS] | TM "INSERT" TM | TM "LEX" TM |
                   TM "##" TM (R-associative)
   (500)  TM  ::=  TM "DELETE" TM | TM "DIFF" TM | TM "UNION" TM |
                   TM "-" TM | TM "+" TM | TM "RUNION" TM
                   (L-associative)
...

This is a description of the way in which terms can be constructed from tokens and recursive invocations. For example, the rule at precedence level 70 is

   TM  ::=  "if" TM "then" TM "else" TM  [COND]

This rule is saying that if you input ``if P then Q else R``, the concrete syntax phase treatment of this phrase will turn it into COND P Q R. If there is no name in square brackets after a rule, then the head operator name is the same as the (one) token in the rule. Thus the rule for + is just TM  ::=  TM "+" TM.

The numbers associated with rules indicate their precedence. The higher the number, the more tightly the operators “pull at” TMs to their left or right. Because + is at level 500, and * is at 600, arithmetic expressions such as ``2 * x + 1`` parse as you’d expect. Rules that can pull in both directions at once (“infixes”, such as + and <=) are also given associativities. Because /\ is right-associative, ``p /\ q /\ r`` parses to (/\ p (/\ q r)).

The next section of the term_grammar() output is the list of known constants. For example:

   Known constants:
     ! ## & () * ** *, + ++ , - /\ 0 :- :> < <<= <= <=/=> <=> <> = =+ ==> >
     >= ? ?! @ ABS_num ABS_prod ABS_sum AC ALL_DISTINCT APPEND ARB ASSOC
     Abbrev BIGINTER BIGUNION BIJ BIT1 BIT2 BOUNDED CARD CHOICE COMM COMPL
     COND CONS CR CROSS CURRY Cong DATATYPE DELETE DIFF DISJOINT DIV DIV2
     DIVMOD DIV_2EXP DROP EL EMPTY EMPTY_REL EQC EVEN EVERY EXISTS EXP
...
     stmarker sum_case sum_size symmetric the_fun the_value total
     transitive tri trichotomous unint wellfounded ~

This is the list of names that cannot be used to name free variables. Instead, if this name occurs (after concrete syntax has been processed away), it will turn into a constant (or a pattern form, see below). Thus, you cannot write ``EQC + 6`` (when relationTheory is loaded) because the EQC is the name of a constant, and it does not have a numeric type. If a name appears in a binding position, it can be anything. So you can write ``λEQC. EQC + 6``. I wouldn’t recommend it, but it’s allowed.

The final section is a list of mappings from constant “names” (in the sense of the previous paragraph) to actual term values. Not every such binding is listed. In particular, if a string maps to one constant that has the same name, then this listing will not appear. Each line is of the form

    <name>        ->  <constant1> ... <constantn>

For example, there is a line

    **            ->  EXP

meaning that the name ** will map to the constant EXP (from arithmeticTheory). Note that there is also a mapping from the string EXP to the same constant. This mapping isn’t listed because there is less cause for confusion there.

Another sort of situation is illustrated with the line

    ++            ->  APPEND ++

which means that the name ++ can map to either the list constant APPEND or the constant ++. (How do you find out which constant that last one is? Try map dest_thy_const (decls "++").)

Finally, an overloading mapping may also take a string to a pattern, which is a λ-expression. This is illustrated by the line for <>:

    <>            ->  (\(x :'a) (y :'a). bool$~ (min$= x y))

This means that the name <> maps to a pattern taking two arguments and turning them into a negated equality.

What’s the difference between `...` and ``...`` — it seems like some functions want one and others the other, but there’s no obvious difference between the uses to me ...

The ``...`` form is really the application of the function Parse.Term to the quotation `...`. A quotation is really just a string (except it also supports anti-quotations, see below). The reason it isn’t just a string is that SML strings require you to backslash quote backslashes, and to backslash quote newlines. Both of these would interfere with HOL syntax (conjunction, disjunction, and lambda in our ASCII notation all involve backslashes; we often want to input goals over multiple lines).

The Term function turns a quotation into a term. It’s the system’s parser.

If you write something like

         tactic_taking_argument ``my term``  THEN some_other_tactic

the `my term` quotation is parsed entirely independently of the goal. This can be a pain. Say, you’re proving something about numbers, and your goal includes variables x and y. If your quotation is `x ≠ y`, you’d like those variables to have the type :num. But they won’t because the parser’s default behaviour is to assign variables polymorphic types.

But, the tactics that take quotations can arrange to call the parser in a special way, passing in information about the goal’s free variables, so that when you write

         Q.tactic_taking_argument `x ≠ y` THEN some_other_tactic

you get x and y parsing to have type :num instead of :'a.

Most things that take quotations are tactics, but there are some other situations where it makes sense to be parsing the terms in augmented contexts. Also, some functions (e.g., proofManagerLib.g, Q.store_thm and Q.prove) don’t exploit a context, but do enforce a type on what is parsed (goals must be of type :bool). They also reduce screen-clutter.

$∉ isn’t recognised as the “not-an-element” term, but $NOTIN is.

The following session seems to exhibit a strange behaviour:

         - type_of ``$NOTIN``;
         <<HOL message: inventing new type variable names: 'a>>
         > val it = ``:α -> (α -> bool) -> bool`` : hol_type

         - type_of ``$∉``;
         > val it = ``:α`` : hol_type

         - dest_term ``$∉``;
         <<HOL message: inventing new type variable names: 'a>>
         > val it = VAR ("∉", ``:'a``) : lambda

In fact, this is a known consequence of the design. The $-quoting of symbols turns them into things that aren’t treated specially by the surface syntax parsing (which handles infix operators etc). Thus, when dollar-quoted, the gets passed through to the name resolution phase unchanged. The name resolution phase then decides that is not a name it knows anything about, so it passes through that phase and becomes a variable.

Name resolution doesn’t know anything about because the system is set up so that the surface syntax phase turns it into the name NOTIN. You can see this by examining the output of term_grammar():

         - term_grammar();
         > val it =
               ...
               (425) TM  ::=  ... | TM "∉" TM [NOTIN] | ...
               ...

The presence of NOTIN in the square brackets indicates that this rule maps the form with into the name NOTIN.

A similar mapping from surface syntax to name happens to turn if-then-else into COND. If you write $if, you get a variable called if, not the constant COND.

How do I add a new symbol <->?

The problem looks like this:

         - ``<->``;
         Don't expect to find a -> in this position after a <
         on line 1318, characters 3-4 and at line 1318, character 2.
         ! Uncaught exception:
         ! HOL_ERR

The treatment of - changed to support unary minus, and so you get this odd splitting behaviour if you give the parser <-> when it’s “unprepared”. You can “prepare” it by making calls to set_fixity and/or overload_on.

Thus:

         val _ = set_fixity "<->" (Infixl 500);

         val _ = overload_on ("<->", ``myconst``);

Either of these will do the trick; doing both (a common use-case) is also fine.

I defined an infix “and”. This works OK, but it seems to not get the precedence I gave it. Is this an interaction with let-and declaration syntax? I don’t use let-and much, so is there a way to remove the let-and treatment of “and” from the term grammar?

Yes, if the let-and syntax is enabled (as it is by default), there will be a competing “and” infix at fixity level 9 in the grammar. (You can see this if you look at the output of a call to term_grammar().) The way to get rid of it is with

    remove_termtok {term_name = GrammarSpecials.and_special, tok = "and"};
Why can’t I write ``MAP ~ x``?
When you attempt this, you will get the error message
    No rule for [~]
meaning that the parser wants to do a reduction involving just the special symbol ~, and it can’t find a rule that allows this. The rule in the grammar is
    TM ::= ~ TM

~ is treated specially, and not just as a function that you’d apply to arguments normally, for two reasons:

  • it can have precedence weaker than just function application. This means that when you write ~f x, this is parsed as ~(f x).

  • it can group without needing extra parentheses, so you can write ~~b; you don’t need to write ~(~b).

To make ~ lose its special status, you should prefix it with a $. ``MAP $~ x`` will work in the example, assuming that x has type :bool list.

I’d like to use MEM as an infix, not a Prefix.

Use grammar manipulation functions such as set_fixity to alter its parsing information. These changes can be made to persist when the current theory is exported. For example:

   - load "listTheory";
   - set_fixity "MEM" (Infix(NONASSOC,425));
   > val it = () : unit
   - listTheory.MEM;
   > val it =
           |- (!x. x MEM [] = F) /\ !x h t. x MEM h::t = (x = h) \/ x MEM t
           : thm
How do I print a term with all the pretty-printing turned off?

To print a term t try

   print_term_by_grammar boolTheory.bool_grammars t

This still retains pretty-printing for all of the constants in boolTheory, including COND. If you really want to see even /\, ! etc in their raw form, try

   print_term_by_grammar min_grammars t

For example:

   - print_term_by_grammar min_grammars  (concl AND_CLAUSES);
   bool$!
     (\t.
        bool$/\ (bool$/\ bool$T t = t)
          (bool$/\ (bool$/\ t bool$T = t)
             (bool$/\ (bool$/\ bool$F t = bool$F)
                (bool$/\ (bool$/\ t bool$F = bool$F) (bool$/\ t t = t)))))
   > val it = () : unit

and

   - print_term_by_grammar min_grammars  (concl COND_CLAUSES);
   bool$!
     (\t1.
        bool$!
          (\t2.
             bool$/\ (bool$COND bool$T t1 t2 = t1)
               (bool$COND bool$F t1 t2 = t2)))
   > val it = () : unit

Note that even in min_grammars, =, @ and ==> are treated specially.

I want to have the parser transform the concrete syntax ``P[e/v]`` into ``(\v. P) e``.

First a warning: this is not likely to do what you want. For example, you wouldn’t get any nice way of stating the Hoare assignment axiom.

    { P[e/v] } v := e { P }
In order to state the above, you’d need to actually write
    { (P v)[e/v] } v := e { P v }

to make it clear that v might exist in the post-condition.

And given this, you might as well write:

    { P e } v := e { P v }
(The problem boils down to the fact that the literal HOL term
    ``(\v. P) x``
where P is a variable, reduces under beta-conversion to P.)

Incidentally, if this is the sort of thing you are doing, you might be interested in looking at Peter Homeier’s Sunrise system which implements a VCG in HOL.

If you really do want to implement your parsing trick above (turning ``P[e/v]`` into ``(\v. P) e``), you could do this by implementing your own parser. Moreover, this might not be impossibly difficult, because the various phases of the existing parser can be called independently. Here’s a sketch of what you’d need to do:

  1. add a rule to the grammar corresponding to your concrete syntax above. Map the syntax to some arbitrary identifier, "foo" say (see the Reference entry for add_rule). Note that your particular choice of syntax, involving square brackets and / will conflict with the use of these symbols in the theories of lists and integers. The best way around these problems is to explicitly load these theories, remove their syntax (see remove_termtok), and then install your own. This will ensure that things won’t break if someone loads your theory/library and then later loads lists and/or integers.
  2. The first phase of your new parser will be to call Absyn, which will turn P[e/v] into abstract syntax corresponding to

    ``foo P e v``

    You then traverse the term looking for this pattern and turning it into (\v. P) e. You would also raise an error at this stage if v wasn’t a variable.
  3. You would then pass your modified abstract syntax "term" onto the next stages of the built-in parser (type-checking etc). To do this, you would use
       Parse.absyn_to_term (term_grammar())
             
I hope this makes sense. The definition of the standard parser from Parse.sml is just
   fun Term q = absyn_to_term (term_grammar()) (Absyn q)
So all you are doing is inserting an extra phase into the process after calling Absyn, but before calling absyn_to_term.

Quotes and Antiquotes

How do I antiquote types?
Antiquoting types works as you would expect when parsing types, so that it is fine to write:
    - val ty = Type`:bool`;
and then
    - Type`:num -> ^ty`;
However, you may wish to also introduce type antiquotations into term parses (as a type constraint on a variable for example). The problem is that you can’t just write ^ty in this context, because the parsing function’s type insists that all antiquotes be of type term. You must use the ty_antiq function, which magically makes a type appear as a term:
    - val antity = ty_antiq ty;
    > val antity = `(ty_antiq(`:bool`))` : term
Then:
    - val x = Term `x:^antity`;
It’s quite easy to figure out when and why ty_antiq is required if one understands the type of the parsing functions. For example, Term and (fn q => -- q --) have type
    term frag list -> term
While Type and (fn q => == q ==) have type
    hol_type frag list -> hol_type
The frag list refers to the fact that there is a quotation being consumed. A quotation is something that appears between back-quotes. A quotation consists of strings and antiquotations. A term frag list must have antiquotations that are of type term. A hol_type frag list must have antiquotations that are of type hol_type. Thus, if you use Term to parse a term, you can’t directly antiquote in types, because this would violate the typing rules (you can only antiquote in terms if you call Term, because it requires a term frag list).

So, in order to antiquote types into terms there is a bit of magic called ty_antiq, which if you look at its type (hol_type -> term) turns a type into a term. The term formed is completely bogus in a logical sense (it’s actually a variable with a special name and the given type), but can be pushed into the parsing function Term so as to give the effect of antiquoting a type.

The function Hol_datatype takes a hol_type frag list, so if you want to antiquote a type into the quotations it takes, you will not need to use ty_antiq.


Tactics

I want to just write tac1 THEN tac2 instead of tac1 THENL ((fn t => [t,t]) tac2) but when I tried the version with THEN I got an error

The fact that the infixes THEN, THEN1 (a version of THENL) are left-associative occasionally causes problems. (That there is a problem stems from the fact that the THEN/THENL combination is not associative.) You can usually get around this problem by bracketing your tactics differently.

The typical problem is when you apply tac1, generating two goals. You then apply tac2 to one of these generating a further two goals. You construct tac3 and tac4 to handle these. Then you realise that

    tac2 THENL [tac3, tac4]

would correctly handle the second goal that was generated by tac1 as well. So, you write

    tac1 THEN tac2 THENL [tac3, tac4]

and are annoyed when it fails with a THENL error. The reason is that at the point when the THENL gets applied, there are actually four goals to work with, not just two. The same sort of thing happens with THEN1 instead of THENL. You can solve the problem by writing

    tac1 THEN (tac2 THENL [tac3, tac4])

But your problem is superficially slightly different. You say that

    tac1 THENL (fn t => [t,t]) tac2

works, but

    tac1 THEN tac2

doesn’t. This will be because tac2 involves a THENL or a THEN1. Say, it is

    tac21 THEN1 tac22 THEN tac23

When inside a THENL branch, the two copies of this tactic do the right thing. When you use THEN, you have

    tac1 THEN tac21 THEN1 tac22 THEN tac23

After tac1 has been applied you have two goals. After tac21 you have four goals. After tac22, you have three goals, the second of which you wanted to be solved by tac22. From that point on, the tactics behave differently. In particular, tac23 may well do the wrong thing when applied to the goal that tac22 was supposed to see but didn’t.

The fix: write

    tac1 THEN (tac21 THEN1 tac22 THEN tac23)
What is the difference between simplifying with p ⇔ q and the two theorems p ⇒ q and q ⇒ p?

If the simplifier has been told to rewrite p ⇔ q, then if it sees occurrences of terms matching (the pattern) p, it will rewrite to q. Thus, simplifying with the theorem

    ⊢ (LENGTH l = 0)  ⇔  (l = [])

will find instances of LENGTH l = 0 in the goal and rewrite those instances to l = [].

If you instead provide the theorem ⊢ (LENGTH l = 0) ⇒ (l = []), the simplifier will look for occurrences of l and attempt to rewrite them to [], after first attempting to prove LENGTH l = 0 as a side condition. An instance of l (a variable) is any term of list type, so this rewrite may be attempted a great many times. Similarly, if you give

    ⊢ (l = [])  ⇒  (LENGTH l = 0)

the system will attempt to rewrite occurrences of LENGTH l to 0 by proving the side condition l = [].

In almost all circumstances, the iff-rewrite will be better, and trying to use the implications will just cause pain.

Manipulating Hypotheses

How do I put HOL in a state so that theorem assumptions are printed?

Use

    show_assums := true;

This flag, along with several others that control HOL behaviour can be found in the Globals structure.

How do I select assumptions in proof steps?

This has been a much-discussed topic by HOL users over the years. The info-hol archives have the details. The received opinion seemed to be that numbered assumptions were great at proof-creation time, but had potential for being a nightmare when existing proofs had to be changed.

In any case, the assumptions have to be dealt with. My current favourite approach is to use "PAT_ASSUM", as follows:

    PAT_ASSUM tm MATCH_MP_TAC
or
    Q.PAT_ASSUM q MATCH_MP_TAC

PAT_ASSUM is like UNDISCH_THEN in that it removes an assumption and makes it available as a theorem. However, it is better than UNDISCH_THEN since the quotation argument it takes is treated as a pattern to match against. The free variables of the goal to help constrain the match. It is often the case that very complex assumptions can be singled out by giving quite simple patterns to PAT_ASSUM.

If you are unsatisfied with the way hypotheses are handled in proofs, numbered (or named) assumptions can be added in a number of ways. Perhaps the simplest is to write a version of UNDISCH_THEN, call it UNDISCH_NTH having type

    int -> (thm -> tactic) -> tactic

UNDISCH_NTH k ttac grabs the kth assumption, converts it to a theorem thk, and applies ttac to thk to get the desired tactic. Here’s one way to define it:

    fun UNDISCH_NTH k ttac (g as (asl,_)) =
        UNDISCH_THEN (Lib.el (k+1)(rev asl)) ttac g;

Locating Things

How do I get a datatype’s axiom after using Hol_datatype?

Use

    TypeBase.axiom_of ``:mytypename``

Hopefully you won’t need to do this very much because many of the contexts in which you previously needed the axiom are dealt with more smoothly. For example, cases, induction, one-one and distinctness theorems are now proved automatically, and are available from the TypeBase. For example,

    TypeBase.one_one_of ``:mytypename``

Is there documentation on computeLib.add_convs?

Best thing currently is to look at the implementation of REDUCE_CONV, which uses add_convs to deal with DIV and MOD: the invocation

    add_conv (M,n,c) compset

means (roughly):

when you see constant M applied to n subterms (i.e., M is fully applied to its arguments), apply conversion c

I can’t find help on IN. What theory defined is it defined in?

IN is declared in boolTheory. IN is not an ML identifier, so we don’t index it. Perhaps we could index constants to their place of definition though.

You can always figure out the originating theory by

   dest_thy_const : term -> {Theory : string, Name : string, Ty : hol_type}

Using decls name will give you all the declared constants that have the given name.


Editor Modes

How do I change the colours used to print free (bound, type) variables?

In the emacs mode, you should use M-x customize-face, and then type in the name of the “face” that you wish to change. For example, there are faces hol-free-variable, hol-bound-variable, hol-type-variable and hol-type.

If using the vim mode, the colour-printing comes from ANSI sequences being sent to the terminal that HOL is running in. You should put something like the following in your .hol-config.sml file:

val my_colours = let open term_pp_types in {
  bv = OrangeRed, fv = VividGreen, tyv = PinkPurple, tyop = White,
  tysyn = White
} end
val mybackend = PPBackEnd.ansi_terminal "mybackend" my_colours
val _ = Parse.current_backend := mybackend
The colour names are given in src/parse/term_pp_types.sml (and correspond to those officially supported by ANSI).

Miscellaneous

How can I find out more information about a HOL_ERR exception?

If expression M is causing the grief, then write

    (M) handle e => Raise e
Often the parentheses around M will not be required.

It is sometimes convenient to use the try function as well. It takes a function and an argument, applies the function to the argument, and (on success) returns the result or (on failure) prints the exception. Note however, that try f x will not catch errors arising from the evaluations that lead to f or x.

How do I quit? (The system hangs when I type quit())

This arises because the quotation-filter, which handles the ``...`` and ``:...`` syntax, doesn’t understand the quit command’s significance. Rather than use quit(), end your interactive process by sending an EOF signal. On Unix, type Control-D; on Windows, type Control-Z, followed by RETURN.

How do I create theories in more than one directory?

Both the Holmake program and the various hol scripts take -I <dir> flags to indicate that the system should look in the specified directories for object files (whether theories or libraries). You can rebuild theories in later directories by calling Holmake with the appropriate -I flags. Directories that should be examined for “include files” can also be specified with an INCLUDES= directive in a Holmakefile. See the DESCRIPTION manual for more on this.

How do I specify a new theory’s ancestors?

This is done implicitly in a script file, usually by implicitly referring to an ancestor theory’s theorems in the course of proof. If you want a theory to be an ancestor because you use an exported type (say string from stringTheory), but never refer to any of the theory’s theorems, then you can explicitly refer to it. The standard idiom we have adopted is to write

   local open stringTheory in end;

This makes the dependency on the ancestor theory explicit. If you omit this, and have no other ML-level dependency in your script file, then Holmake will fail to build your script, probably failing with a parse exception when it encounters a type name such as string that it doesn’t think is in scope.

How can I print my *HOL* buffer (in emacs), complete with Unicode characters?

The following elisp code is (will be) part of the standard hol-mode.

   (defcustom hol-unicode-print-font-filename
     "/usr/share/fonts/truetype/ttf-dejavu/DejaVuSans.ttf"
     "File name of font to use when printing HOL output to a PDF file."
     :group 'hol
     :type '(file :must-match t))

   (defun hol-region-to-unicode-pdf (filename beg end)
        "Print region to FILE as a PDF, handling Unicode characters."
        (interactive "FFile to write to: \nr")
        (if (and transient-mark-mode (not mark-active))
            (error "No active region"))
        (let* ((temp-ps-file (make-temp-file "annot" nil ".ps"))
               (lpr-switches
                (list "-font" hol-unicode-print-font-filename
                      "-out" temp-ps-file))
               (lpr-add-switches nil)
               (lpr-command "uniprint"))
          (lpr-region beg end)
          (shell-command (concat "ps2pdf " temp-ps-file " " filename))
          (delete-file temp-ps-file)))

This relies on having the uniprint and ps2pdf tools installed. On Debian-based systems such as Ubuntu, the former is part of the yudit package, which can be installed with a command like

   sudo apt-get install yudit

The code also relies on a hard-coded path pointing to a font file (the hol-unicode-print-font-filename). This can be adjusted using M-x customize and navigating to the hol group (see the External sub-category).

To use this code, select a region of an emacs buffer, and type

   M-x hol-region-to-unicode-pdf

The command will prompt for a file to save to, and then write a PDF file to that location.

Thanks to Dan Synek for the problem, and subsequent inspiration for the code above.

How to rewrite with a theorem the other way round?

Use GSYM.

How do I prove strings equal or inequal?

To achieve exactly this objective, use stringLib.string_EQ_CONV, which reduces equalities over string literals to either T or F. For example, to demonstrate that ``(if "foo" = "bar" then 3 else 1) = 1``, you could write:

   - val t = ``(if "foo" = "bar" then 3 else 1)``;
   > val t = ``(if "foo" = "bar" then 3 else 1)`` : Term.term
   - (DEPTH_CONV stringLib.string_EQ_CONV THENC REWRITE_CONV []) t;
   > val it = |- (if "foo" = "bar" then 3 else 1) = 1 : Thm.thm

Note though that the stateful simplification set behind SRW_TAC and srw_ss() will automatically handle equalities of this form, so that SIMP_CONV (srw_ss()) [] would serve just as well above.