Dear Lockwood,
First, thank you for taking the time to try out HOL-Omega. You are a
pioneer!
Yes, you are correct in all you are reporting about the examples in the
HOL-Omega Tutorial, that they work correctly for interactive use, but will
fail when inserted directly, without modification, into a disk file and
then processed ("built") by the Holmake tool. It turns out the file
versions will need some alterations from the interactive versions. The
conversion of an interactive script into a disk file to be processed by
Holmake is explained in the HOL4 DESCRIPTION manual, available at
http://sourceforge.net/projects/hol/files/hol/kananaskis-8/kananaskis-8-description.pdf/download
Please see section 6.3, "Maintaining HOL Formalizations with Holmake".
In order to ensure that you are using the correct version of Holmake for
HOL-Omega, please make sure that the directory <HOL-Omega root>/bin is
located in your path before any other directory that contains a Holmake
executable. Thus, if you have both HOL4 and HOL-Omega installed (as I do),
you need to set your PATH shell variable to look in the right directory
first.
If you're interested, just as a tip, I have both the HOL4 and HOL-Omega
root directories contained within one higher directory, where I also have a
symbolic link to the theorem prover I am using at the moment:
-bash-3.2$ ls -lt
total 214744
drwxr-xr-x 22 palantir palantir 748 Apr 4 20:28 hol-omega
drwxr-xr-x 18 palantir palantir 612 Apr 21 2012 kananaskis-8
drwxr-xr-x 18 palantir palantir 612 Apr 29 2011 kananaskis-7
lrwxr-xr-x 1 palantir palantir 9 Apr 6 2011 hol -> hol-omega
Here hol-omega contains the HOL-Omega system, and kananaskis-8 and
kananaskis-7 contain recent versions of the HOL4 system. I normally choose
to work in the HOL-Omega system, and so the link named "hol" points to
hol-omega. Then in my .profile or .bashrc file, I set my path to include
"<provers-dir>/hol/bin", so that the search for the Holmake executable goes
through the symbolic link to the right directory of binaries for the system
I am currently using. This makes it easy to switch between systems, by just
changing the symbolic link.
Getting back to the examples in the HOL-Omega tutorial, the tutorial was
written from the point of view of an interactive user, typing in each
expression or block of code in turn, interactively watching them be
processed by the system and produce output. The exact input of the chapter
was not intended to be directly copied into a file without changes. As
explained in DESCRIPTION, storing a development in a file is how HOL-Omega
is normally used, when after some interactive exploration, a script file
is constructed with the mathematical development which is then processed by
Holmake in a batch style.
I did not mean for the user to themselves have to create all these files
for the tutorial examples! Rather, it has been arranged that for each of
the chapters of the HOL-Omega tutorial that describe examples using the new
features, the corresponding source code is provided in one or more disk
files already made up and available. These files accomplish the very same
development as that chapter, but in a form fully suitable for Holmake.
These disk files are found in the directory
<HOL-Omega root directory>/examples/HolOmega/
The names of the files, with the chapter that they relate to, are as
follows:
Chapter 4: HOL-Omega Appetizers
appetizersScript.sml
Chapter 10: Example: Abstract Data Types
type_specScript.sml
Chapter 11: Example: The Category of Types
functorScript.sml
aopScript.sml
monadScript.sml
Chapter 12: Example: Packages
packageScript.sml
These and other files that are found in the examples/HolOmega directory are
described briefly in chapter 13, "More Examples," near the end of the
tutorial. These files are all built automatically when HOL-Omega is built.
The code inside can be copied piece by piece into an interactive
session, if one wishes to avoid some of the laborious typing. Or, if they
wish to examine the logic and reasoning in more detail, the user may find
it instructive to trace through these files step by step.
For most of these files, the building process leaves behind an HTML file
containing a record of the types, constants, and theorems constructed and
saved as part of that theory. For example, for the file
appetizersScript.sml, there is deposited a file appetizersTheory.html,
which can be viewed in a normal web browser to inspect the details of the
theory.
Comparing these script files to what you see in the tutorial should help
illustrate how one can turn an interactive script into a disk file version.
I hope this clarifies the process of going through the tutorial, Lockwood.
The file you were trying to create is already there in
examples/HolOmega/type_specScript.sml. Hopefully this will ease working
through the examples.
If you have any further questions, Lockwood, please do not hesitate to
share, and I will do my best to respond. I appreciate the feedback.
Peter
On Thu, Apr 4, 2013 at 6:00 PM, F.Lockwood Morris <[email protected]> wrote:
> I have had HOL Omega installed, asking that the instructions of Section
> 1.3 of the HOL Omega System Tutorial be followed (what I am unfortunately
> too ignorant to attempt myself), and have been working my way through the
> Tutorial with great interest, Holmake-ing the example theories as I go. All
> goes well through Chapter 8, although when I invoke what should be the
> Holmake of
> the HOL Omega distribution, I get a preliminary message:
>
> *** Switching to execute /usr/local/hol-kananaskis-8/bin/Holmake .
>
> I have skipped Chapter 9. In Chapter 10, Abstract Data Types (where for
> the first time I am using
> features specific to HOL Omega) everything of course goes through
> interactively without complaint.
>
> But when I then run Holmake, if I do not wrap the file up with
>
> structure bit_vector = struct ... end;
>
> then I get, at the first theorem with a type quantification,
>
> Exception- HOL_ERR {message = "on line 131, characters 4-6:\nLexical error
> - Term idents can't begin with prime characters", origin_function =
> "Absyn", origin_structure = "Parse"} raised
> /usr/local/hol-kananaskis-8/bin/Holmake: Failed script build for
> bit_vectorScript - exited with code 1
>
> whereas if I do make a structure out of it, I get for the complete output:
>
> Linking bit_vectorScript.uo to produce theory-builder executable
> Poly/ML 5.5.0 Release
> > Error- in '.HOLMK/bit_vectorScript.sml', line 156.
> Value or constructor (TY_EXISTS_TAC) has not been declared
> Found near
> store_thm
> ("vect_exists", (Parse.Term [... ...]), ... THEN ... THEN ... ...)
> Error- in '.HOLMK/bit_vectorScript.sml', line 162.
> Value or constructor (new_type_specification) has not been declared
> Found near new_type_specification ("vect", ["vect"], vect_exists)
> Static Errors
> /usr/local/hol-kananaskis-8/bin/Holmake: Failed script build for
> bit_vectorScript - exited with code 1
>
> Can anyone suggest where the installation has gone wrong, or I have
> blundered?
>
> Many thanks,
>
> Lockwood
> |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |-
> |- |- |- |- |-
> Lockwood Morris [email protected] (315)443-3046 Rm. 4-125 CST
> EECS Syracuse University 111 College Place Syracuse NY 13244-4100
>
>
> ------------------------------------------------------------------------------
> Minimize network downtime and maximize team effectiveness.
> Reduce network management and security costs.Learn how to hire
> the most talented Cisco Certified professionals. Visit the
> Employer Resources Portal
> http://www.cisco.com/web/learning/employer_resources/index.html
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
Minimize network downtime and maximize team effectiveness.
Reduce network management and security costs.Learn how to hire
the most talented Cisco Certified professionals. Visit the
Employer Resources Portal
http://www.cisco.com/web/learning/employer_resources/index.html
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
