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,
Thomas
On 03/03/2019 11.51, michael.norr...@data61.csiro.au 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.
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
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
