Re: [Hol-info] library visibility

[Michael.Norrish]

It’s available at https://github.com/HOL-Theorem-Prover/SublimeHOL

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

Michael

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,

Thomas
On 03/03/2019 11.51, 
michael.norr...@data61.csiro.au<mailto: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 <mailto:zhtp...@gmail.com>
Date: Sunday, 3 March 2019 at 11:29
To: Thomas Tuerk <mailto:tho...@tuerk-brechen.de>
Cc: hol-info 
<mailto: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 
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 
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 eva

Re: [Hol-info] library visibility

[Thomas Lacroix]

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 
*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!

Haitao

On Sat, Mar 2, 2019 at 3:26 PM Thomas Tuerk <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 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

Re: [Hol-info] library visibility

[Michael.Norrish]

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 
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!

Haitao


On Sat, Mar 2, 2019 at 3:26 PM Thomas Tuerk 
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 
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

Re: [Hol-info] library visibility

[Haitao Zhang]

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  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  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 
> listhol-info@lists.sourceforge.nethttps://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

Re: [Hol-info] library visibility

[Thomas Tuerk]

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  > 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
> 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

Re: [Hol-info] library visibility

[Haitao Zhang]

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  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
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] library visibility

[Haitao Zhang]

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
https://lists.sourceforge.net/lists/listinfo/hol-info