It’s available at

I believe you can install packages directly into Sublime Text by providing such 


From: Thomas Lacroix <>
Date: Tuesday, 5 March 2019 at 19:17
To: "Norrish, Michael (Data61, Acton)" <>
Cc: hol-info <>
Subject: Re: [Hol-info] library visibility

Hi Michael,

You mentioned an editor mode for SublimeText, can you share a link to it?

Also, I will share this since I didn't notice before: with Vim, you can "load" 
files with hl and hL, if they are in directories included in the Holmakefile 
INCLUDES variable.

Thank you,

On 03/03/2019 11.51,<> wrote:
I recommend writing “uses” of modules/theories/libraries into your HOL script 
and copying those into your interactive HOL sessions with M-h M-r.

A “use” is either an open declaration or the use of a qualified name.  For 
example, writing fooTheory.bar_def and then using M-h M-r on that string will 
cause fooTheory to be loaded if it hasn’t been already. Similarly, writing

  open realTheory

will cause realTheory to be loaded.  You can manually write things like

  load “realTheory”;

into the REPL but you should try to avoid uses of load in your script files.

See §4.5 “Turning the script into a theory” in the TUTORIAL manual for a chatty 
description of what should be in a script file.  But then, note that it’s good 
style to always be working with Script files that can be built with Holmake 
from the outset.  That way that there is no separate step required to do what 
is described in §4.5.  The various editor modes (Emacs/vim/SublimeText) are all 
designed to make this as easy as possible.


From: Haitao Zhang <><>
Date: Sunday, 3 March 2019 at 11:29
To: Thomas Tuerk <><>
Cc: hol-info 
Subject: Re: [Hol-info] library visibility

Dear Thomas,

Thanks! You are right that there is no difference between "M-h M-r" and typing 
in the console. I must have used some print command (which I no longer remember 
the name) before to poke into the theories. I think my script is working 
because pred_set and combin (the only two I am accessing through the . field 
accessor) are loaded by default.

> ancestry "-";
val it =
   ["ConseqConv", "quantHeuristics", "patternMatches", "ind_type", "while",
    "one", "sum", "option", "pair", "combin", "sat", "normalForms",
    "relation", "min", "bool", "marker", "num", "prim_rec", "arithmetic",
    "numeral", "basicSize", "numpair", "pred_set", "list", "rich_list",
    "indexedLists"]: string list

It seems if I want to access other theories I need to "load namestr" first and 
it is important that the name is a string and not a label.

Thanks for the help!


On Sat, Mar 2, 2019 at 3:26 PM Thomas Tuerk 
<<>> wrote:

Dear Haito,

what are you trying to do? HOL theories are ML modules. If you type a value, 
the Polyml REPL replies the value. However, as your error message correctly 
states, modules are not values. So, the error is what I expect and not a sign 
that a module is no longer visible.

So, "combinTheory" is a (known and loaded) module and you get an error. 
"combineTheory.K_DEF" is a value (of type thm) and it works. I does not make 
sense to me that you say it works in the emacs mode though. There are a few 
hacks in of loading and opening modules, but nothing that should lead to the 
behaviour you describe (as far as I'm aware). For me, I get the same error also 
within emacs. I do not have a recent version of HOL installed currently, though.

By the way, it is not HOL theory specific. Try e.g. the module "List" and 
"List.hd". For opening a module you need to use "open".



On 03.03.19 00:06, Haitao Zhang wrote:
And even more weird:

> combinTheory;
poly: : error: Value or constructor (combinTheory) has not been declared
Found near combinTheory
Static Errors
> combinTheory.K_DEF;
val it = ⊢ K = (λx y. x): thm


On Sat, Mar 2, 2019 at 2:34 PM Haitao Zhang 
<<>> wrote:
For some reason in my hol session system libraries are no longer visible. If I 
directly type into the hol console:

> pred_setTheory;
poly: : error: Value or constructor (pred_setTheory) has not been declared
Found near pred_setTheory
Static Errors

But when I evaluates through emacs 'M-h' 'M-r' everything still works. The only 
difference I can tell is that in the emacs case hol is reading and evaluating a 
temporarily created script sml file.

I definitely remember I could do the above in the hol console as well and I had 
not played with any settings/env variables intentionally. It is possible that 
sometimes by hitting the wrong key sequence in emacs I had sent very erroneous 
strings to be evaluated.

Where should I look to resolve this?



hol-info mailing list<>
hol-info mailing list<>


hol-info mailing list<>
hol-info mailing list

Reply via email to