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
