Hi All,
I (think I) just successfully got HOL light built, but I'm now getting the
following error:
# `x+1`;;
File "", line 1, characters 0-5:
Error: Unbound value parse_term
Note that as per a previous thread, I did the following, to use ocamlnum:
user:~ owenlewis$ cd Documents/hol_stuff/trunk
user:trunk owenlewis$ ocamlmktop -o ocamlnum nums.cma
user:trunk owenlewis$ ./ocamlnum
I included below the whole output I got when loading hol inside ocaml - I
apologize for dumping this all on you, but I wasn't sure which parts are
relevant. I should mention that I had a few problems with previous
installation/build steps, so it's possible that some component system isn't
installed as it needs to be. Also, I've been using ocaml batteries; I
don't know if this could cause any problems. I'm using:
Mac 10.6.8
ocaml 4.00.1
camlp5 (strict mode)
HOL light 158
Thanks for your help,
Owen
OCaml version 4.00.1
_____________________________
[| + | | Batteries 2.0 - |
|_____|_|____________________|
_____________________________
| - Type '#help;;' | | + |]
|______________________|_|___|
# #use "hol.ml";;
val hol_version : string = u"2.20++"
val hol_dir : string Batteries.ref =
{contents = u"/Users/owenlewis/Documents/
hol_stuff/trunk"}
val temp_path : string Batteries.ref = {contents = u"/tmp"}
- : unit = ()
- : unit = ()
val use_file : string -> unit = <fun>
val hol_expand_directory : string -> string = <fun>
val load_path : string list Batteries.ref = {contents = [u"."; u"$"]}
val loaded_files : '_a list Batteries.ref = {contents = []}
val file_on_path : string list -> string -> string = <fun>
val load_on_path : string list -> string -> unit = <fun>
val loads : string -> unit = <fun>
val loadt : string -> unit = <fun>
val needs : string -> unit = <fun>
- : unit = ()
- : unit = ()
val quotexpander : string -> string = <fun>
- : unit = ()
- : bool = true
type num =
Num.num =
Int of int
| Big_int of Big_int.big_int
| Ratio of Ratio.ratio
type t = num
val zero : num = <num 0>
val one : num = <num 1>
val neg : num -> num = <fun>
val abs : num -> num = <fun>
val add : num -> num -> num = <fun>
val sub : num -> num -> num = <fun>
val mul : num -> num -> num = <fun>
val div : num -> num -> num = <fun>
val modulo : num -> num -> num = <fun>
val pow : num -> num -> num = <fun>
val compare : num -> num -> int = <fun>
val ord : num -> num -> BatOrd.order = <fun>
val equal : num -> num -> bool = <fun>
val of_int : int -> num = <fun>
val to_int : num -> int = <fun>
val of_float : float -> num = <fun>
val to_float : num -> float = <fun>
val of_string : string -> num = <fun>
val to_string : num -> string = <fun>
val ( + ) : num -> num -> num = <fun>
val ( - ) : num -> num -> num = <fun>
val ( * ) : num -> num -> num = <fun>
val ( / ) : num -> num -> num = <fun>
val ( ** ) : num -> num -> num = <fun>
val max_num : num -> num -> num = <fun>
val min_num : num -> num -> num = <fun>
val quo : num -> num -> num = <fun>
val square : num -> num = <fun>
val succ : num -> num = <fun>
val pred : num -> num = <fun>
val is_integer : num -> bool = <fun>
val round : num -> num = <fun>
val floor : num -> num = <fun>
val ceil : num -> num = <fun>
val approx : num -> num = <fun>
val sign : num -> int = <fun>
val operations : num BatNumber.numeric =
{BatNumber.zero = <num 0>; BatNumber.one = <num 1>; BatNumber.neg = <fun>;
BatNumber.succ = <fun>; BatNumber.pred = <fun>; BatNumber.abs = <fun>;
BatNumber.add = <fun>; BatNumber.sub = <fun>; BatNumber.mul = <fun>;
BatNumber.div = <fun>; BatNumber.modulo = <fun>; BatNumber.pow = <fun>;
BatNumber.compare = <fun>; BatNumber.of_int = <fun>;
BatNumber.to_int = <fun>; BatNumber.of_string = <fun>;
BatNumber.to_string = <fun>; BatNumber.of_float = <fun>;
BatNumber.to_float = <fun>}
val ( =/ ) : num -> num -> bool = <fun>
val ( </ ) : num -> num -> bool = <fun>
val ( >/ ) : num -> num -> bool = <fun>
val ( <=/ ) : num -> num -> bool = <fun>
val ( >=/ ) : num -> num -> bool = <fun>
val ( <>/ ) : num -> num -> bool = <fun>
val eq_num : num -> num -> bool = <fun>
val lt_num : num -> num -> bool = <fun>
val le_num : num -> num -> bool = <fun>
val gt_num : num -> num -> bool = <fun>
val ge_num : num -> num -> bool = <fun>
val approx_num_fix : int -> num -> string = <fun>
val approx_num_exp : int -> num -> string = <fun>
val nat_of_num : num -> Nat.nat = <fun>
val num_of_nat : Nat.nat -> num = <fun>
val num_of_big_int : Big_int.big_int -> num = <fun>
val big_int_of_num : num -> Big_int.big_int = <fun>
val ratio_of_num : num -> Ratio.ratio = <fun>
val num_of_ratio : Ratio.ratio -> num = <fun>
val float_of_num : num -> float = <fun>
val print : 'a BatInnerIO.output -> t -> unit = <fun>
module TaggedInfix :
sig
val ( =/ ) : num -> num -> bool
val ( </ ) : num -> num -> bool
val ( >/ ) : num -> num -> bool
val ( <=/ ) : num -> num -> bool
val ( >=/ ) : num -> num -> bool
val ( <>/ ) : num -> num -> bool
val ( +/ ) : num -> num -> num
val ( -/ ) : num -> num -> num
val ( */ ) : num -> num -> num
val ( // ) : num -> num -> num
val ( **/ ) : num -> num -> num
end
module Infix :
sig
type bat__infix_t = t
val ( + ) : bat__infix_t -> bat__infix_t -> bat__infix_t
val ( - ) : bat__infix_t -> bat__infix_t -> bat__infix_t
val ( * ) : bat__infix_t -> bat__infix_t -> bat__infix_t
val ( / ) : bat__infix_t -> bat__infix_t -> bat__infix_t
val ( ** ) : bat__infix_t -> bat__infix_t -> bat__infix_t
val ( -- ) : bat__infix_t -> bat__infix_t -> bat__infix_t BatEnum.t
val ( --- ) : bat__infix_t -> bat__infix_t -> bat__infix_t BatEnum.t
val ( =/ ) : num -> num -> bool
val ( </ ) : num -> num -> bool
val ( >/ ) : num -> num -> bool
val ( <=/ ) : num -> num -> bool
val ( >=/ ) : num -> num -> bool
val ( <>/ ) : num -> num -> bool
val ( +/ ) : num -> num -> num
val ( -/ ) : num -> num -> num
val ( */ ) : num -> num -> num
val ( // ) : num -> num -> num
val ( **/ ) : num -> num -> num
end
module Compare :
sig
type bat__compare_t = t
val ( <> ) : bat__compare_t -> bat__compare_t -> bool
val ( >= ) : bat__compare_t -> bat__compare_t -> bool
val ( <= ) : bat__compare_t -> bat__compare_t -> bool
val ( > ) : bat__compare_t -> bat__compare_t -> bool
val ( < ) : bat__compare_t -> bat__compare_t -> bool
val ( = ) : bat__compare_t -> bat__compare_t -> bool
end
val ( +/ ) : num -> num -> num = <fun>
val add_num : num -> num -> num = <fun>
val minus_num : num -> num = <fun>
val ( -/ ) : num -> num -> num = <fun>
val sub_num : num -> num -> num = <fun>
val ( */ ) : num -> num -> num = <fun>
val mult_num : num -> num -> num = <fun>
val square_num : num -> num = <fun>
val ( // ) : num -> num -> num = <fun>
val div_num : num -> num -> num = <fun>
val quo_num : num -> num -> num = <fun>
val mod_num : num -> num -> num = <fun>
val ( **/ ) : num -> num -> num = <fun>
val power_num : num -> num -> num = <fun>
val abs_num : num -> num = <fun>
val succ_num : num -> num = <fun>
val pred_num : num -> num = <fun>
val incr_num : num ref -> unit = <fun>
val decr_num : num ref -> unit = <fun>
val is_integer_num : num -> bool = <fun>
val integer_num : num -> num = <fun>
val floor_num : num -> num = <fun>
val round_num : num -> num = <fun>
val ceiling_num : num -> num = <fun>
val sign_num : num -> int = <fun>
val string_of_num : num -> string = <fun>
val num_of_string : string -> num = <fun>
val int_of_num : num -> int = <fun>
val num_of_int : int -> num = <fun>
val compare_num : num -> num -> int = <fun>
val print_num : num -> unit = <fun>
- : unit = ()
val fail : unit -> 'a = <fun>
val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c = <fun>
val I : 'a -> 'a = <fun>
val K : 'a -> 'b -> 'a = <fun>
val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c = <fun>
val W : ('a -> 'a -> 'b) -> 'a -> 'b = <fun>
val o : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>
val f_f_ : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd = <fun>
val hd : 'a list -> 'a = <fun>
val tl : 'a list -> 'a list = <fun>
val map : ('a -> 'b) -> 'a list -> 'b list = <fun>
val last : 'a list -> 'a = <fun>
val butlast : 'a list -> 'a list = <fun>
File "", line 66, characters 30-31:
Error: This expression has type int but an expression was expected of type
num = Num.num
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/lib.ml
- : unit = ()
- : unit = ()
module type Hol_kernel =
sig
type hol_type = private Tyvar of string | Tyapp of string * hol_type
list
type term = private
Var of string * hol_type
| Const of string * hol_type
| Comb of term * term
| Abs of term * term
type thm
val types : unit -> (string * int) list
val get_type_arity : string -> int
val new_type : string * int -> unit
val mk_type : string * hol_type list -> hol_type
val mk_vartype : string -> hol_type
val dest_type : hol_type -> string * hol_type list
val dest_vartype : hol_type -> string
val is_type : hol_type -> bool
val is_vartype : hol_type -> bool
val tyvars : hol_type -> hol_type list
val type_subst : (hol_type * hol_type) list -> hol_type -> hol_type
val bool_ty : hol_type
val aty : hol_type
val constants : unit -> (string * hol_type) list
val get_const_type : string -> hol_type
val new_constant : string * hol_type -> unit
val type_of : term -> hol_type
val alphaorder : term -> term -> int
val is_var : term -> bool
val is_const : term -> bool
val is_abs : term -> bool
val is_comb : term -> bool
val mk_var : string * hol_type -> term
val mk_const : string * (hol_type * hol_type) list -> term
val mk_abs : term * term -> term
val mk_comb : term * term -> term
val dest_var : term -> string * hol_type
val dest_const : term -> string * hol_type
val dest_comb : term -> term * term
val dest_abs : term -> term * term
val frees : term -> term list
val freesl : term list -> term list
val freesin : term list -> term -> bool
val vfree_in : term -> term -> bool
val type_vars_in_term : term -> hol_type list
val variant : term list -> term -> term
val vsubst : (term * term) list -> term -> term
val inst : (hol_type * hol_type) list -> term -> term
val rand : term -> term
val rator : term -> term
val dest_eq : term -> term * term
val dest_thm : thm -> term list * term
val hyp : thm -> term list
val concl : thm -> term
val REFL : term -> thm
val TRANS : thm -> thm -> thm
val MK_COMB : thm * thm -> thm
val ABS : term -> thm -> thm
val BETA : term -> thm
val ASSUME : term -> thm
val EQ_MP : thm -> thm -> thm
val DEDUCT_ANTISYM_RULE : thm -> thm -> thm
val INST_TYPE : (hol_type * hol_type) list -> thm -> thm
val INST : (term * term) list -> thm -> thm
val axioms : unit -> thm list
val new_axiom : term -> thm
val definitions : unit -> thm list
val new_basic_definition : term -> thm
val new_basic_type_definition :
string -> string * string -> thm -> thm * thm
end
File "", line 126, characters 25-30:
Error: Unbound value assoc
File "lib.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/fusion.ml
- : unit = ()
- : unit = ()
File "", line 19, characters 26-31:
Error: This expression has type int but an expression was expected of type
num = Num.num
File "fusion.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/basics.ml
- : unit = ()
- : unit = ()
type term_label =
Vnet
| Lcnet of (string * int)
| Cnet of (string * int)
| Lnet of int
type 'a net = Netnode of (term_label * 'a net) list * 'a list
val empty_net : 'a net = Netnode ([], [])
File "", line 40, characters 18-28:
Error: Unbound value strip_comb
File "basics.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/nets.ml
- : unit = ()
- : unit = ()
File "", line 25, characters 17-23:
Error: Unbound value itlist
File "nets.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/printer.ml
- : unit = ()
- : unit = ()
val ignore_constant_varstruct : bool Batteries.ref = {contents = true}
val type_invention_warning : bool Batteries.ref = {contents = true}
val type_invention_error : bool Batteries.ref = {contents = false}
File "", line 33, characters 41-49:
Error: Unbound type constructor hol_type
File "printer.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/preterm.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 0-14:
Error: Unbound value parse_as_infix
File "preterm.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/parser.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 12-16:
Error: Unbound type constructor term
File "printer.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/equal.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 0-15:
Error: Unbound value parse_as_prefix
File "equal.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/bool.ml
- : unit = ()
- : unit = ()
File "", line 17, characters 9-13:
Error: Unbound type constructor term
File "bool.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/drule.ml
- : unit = ()
- : unit = ()
File "", line 17, characters 27-40:
Error: Unbound type constructor instantiation
File "drule.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/tactics.ml
- : unit = ()
- : unit = ()
File "", line 17, characters 14-24:
Error: Unbound value term_unify
File "tactics.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/itab.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 19-23:
Error: Unbound type constructor conv
File "itab.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/simp.ml
- : unit = ()
- : unit = ()
File "", line 17, characters 14-19:
Error: Unbound value prove
File "simp.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
theorems.ml
- : unit = ()
- : unit = ()
File "", line 19, characters 14-23:
Error: Unbound value dest_comb
File "theorems.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
ind_defs.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 13-22:
Error: Unbound value new_axiom
File "ind_defs.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/class.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 0-14:
Error: Unbound value parse_as_infix
File "class.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/trivia.ml
- : unit = ()
- : unit = ()
File "", line 17, characters 2-18:
Error: Unbound value GEN_REWRITE_CONV
File "trivia.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/canon.ml
- : unit = ()
- : unit = ()
val meson_depth : bool Batteries.ref = {contents = false}
val meson_prefine : bool Batteries.ref = {contents = true}
val meson_dcutin : int Batteries.ref = {contents = 1}
val meson_skew : int Batteries.ref = {contents = 3}
val meson_brand : bool Batteries.ref = {contents = false}
val meson_split_limit : int Batteries.ref = {contents = 8}
val meson_chatty : bool Batteries.ref = {contents = false}
exception Cut
type fol_term = Fvar of int | Fnapp of int * fol_term list
type fol_atom = int * fol_term list
type fol_form =
Atom of fol_atom
| Conj of fol_form * fol_form
| Disj of fol_form * fol_form
| Forallq of int * fol_form
File "", line 56, characters 47-50:
Error: Unbound type constructor thm
File "canon.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/meson.ml
- : unit = ()
- : unit = ()
File "", line 25, characters 20-29:
Error: Unbound value dest_type
File "meson.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/quot.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 14-28:
Error: Unbound value new_definition
File "quot.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/pair.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 0-8:
Error: Unbound value new_type
File "pair.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/nums.ml
- : unit = ()
- : unit = ()
File "", line 20, characters 17-26:
Error: Unbound value conjuncts
File "nums.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
recursion.ml
- : unit = ()
- : unit = ()
File "", line 20, characters 0-14:
Error: Unbound value parse_as_infix
File "recursion.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/arith.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 0-14:
Error: Unbound value parse_as_infix
File "arith.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/wf.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 16-32:
Error: Unbound value GEN_REWRITE_RULE
File "wf.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
calc_num.ml
- : unit = ()
- : unit = ()
File "", line 10, characters 22-27:
Error: Unbound value prove
File "calc_num.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
normalizer.ml
- : unit = ()
- : unit = ()
type history =
Start of int
| Mmul of (num * int list) * history
| Add of history * history
File "", line 40, characters 26-32:
Error: Unbound value itlist
File "normalizer.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/grobner.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 19-24:
Error: Unbound value prove
File "grobner.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
ind_types.ml
- : unit = ()
- : unit = ()
File "", line 17, characters 20-25:
Error: Unbound value prove
File "ind_types.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/lists.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 0-14:
Error: Unbound value parse_as_infix
File "lists.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/realax.ml
- : unit = ()
- : unit = ()
File "", line 18, characters 4-34:
Error: Unbound constructor Comb
File "realax.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
calc_int.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 21-26:
Error: Unbound value prove
File "calc_int.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
realarith.ml
- : unit = ()
- : unit = ()
File "", line 17, characters 21-26:
Error: Unbound value prove
File "realarith.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/real.ml
- : unit = ()
- : unit = ()
File "", line 16, characters 14-28:
Error: Unbound value new_definition
File "real.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
calc_rat.ml
- : unit = ()
- : unit = ()
File "", line 20, characters 14-28:
Error: Unbound value new_definition
File "calc_rat.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/int.ml
- : unit = ()
- : unit = ()
File "", line 17, characters 0-14:
Error: Unbound value parse_as_infix
File "int.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/sets.ml
- : unit = ()
- : unit = ()
File "", line 10, characters 0-14:
Error: Unbound value prioritize_num
File "sets.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/iterate.ml
- : unit = ()
- : unit = ()
File "", line 13, characters 15-29:
Error: Unbound value new_definition
File "iterate.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/cart.ml
- : unit = ()
- : unit = ()
File "", line 13, characters 19-43:
Error: Unbound value new_recursive_definition
File "cart.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/define.ml
- : unit = ()
- : unit = ()
val help_path : string list Batteries.ref = {contents = [u"$/Help"]}
File "", line 47, characters 34-49:
Error: This expression has type int but an expression was expected of type
num = Num.num
File "define.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/help.ml
- : unit = ()
- : unit = ()
File "", line 3, characters 0-8:
Error: Unbound value theorems
File "help.ml" already loaded
Error in included file /Users/owenlewis/Documents/hol_stuff/trunk/
database.ml
- : unit = ()
Camlp5 parsing version 6.08
------------------------------------------------------------------------------
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
