How do you "open it using hol.bat"?
There are a few ways to feed files to HOL. One way is with a command line
redirect:
$ hol < myfile
Another is by calling use within HOL:
> use "myfile";
However, the best way is to set the file up so that its can be compiled with
Holmake. For this, see section 6.3 of the Description manual and/or section
4.5 of the Tutorial. Once this is done, you will have renamed your base file
to myfile.sml or myScript.sml, and you will also have a file in your directory
named
myfile.uo
or
myTheory.uo
You will then be able to work with this file in future uses of Holmake, and to
load it interactively with
load "myfile";
or
load "myTheory";
I hope this helps.
Michael
On 16/04/2013, at 4:47, "J. J. W." <[email protected]> wrote:
> Dear all,
>
> I have a small question regarding loading SML files, I have some difficulties
> loading them using hol.bat from the hol installer for Windows.
>
> I have written a file with the following contents:
>
> (* Test loading file *)
>
> set_trace "Unicode" 0;
>
> val test = Define `identityList a = a`;
>
> Now I save the file and open it using hol.bat, however I get Unbound value
> identifier Define, even though if I do not load the file and just input it
> hol.bat manually, it works perfectly.
>
> It seems that it has something to do with end-init-boss.sml, since I don't
> get that part after it fails loading the val test.
>
> Can someone point me in the right direction how I can solve this rather
> elementary problem? Or refer me to a page?
>
> Yours sincerely,
>
> Jun Jie
> ------------------------------------------------------------------------------
> Precog is a next-generation analytics platform capable of advanced
> analytics on semi-structured data. The platform includes APIs for building
> apps and a phenomenal toolset for data science. Developers can use
> our toolset for easy data analysis & visualization. Get a free account!
> http://www2.precog.com/precogplatform/slashdotnewsletter
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
