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.
Michael
From: Haitao Zhang <zhtp...@gmail.com>
Date: Sunday, 3 March 2019 at 11:29
To: Thomas Tuerk <tho...@tuerk-brechen.de>
Cc: hol-info <hol-info@lists.sourceforge.net>
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!
Haitao
On Sat, Mar 2, 2019 at 3:26 PM Thomas Tuerk
<tho...@tuerk-brechen.de<mailto:tho...@tuerk-brechen.de>> 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".
Best
Thomas
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
Hmm?!
On Sat, Mar 2, 2019 at 2:34 PM Haitao Zhang
<zhtp...@gmail.com<mailto:zhtp...@gmail.com>> 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?
Thanks,
Haitao
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
