[opentheory-users] Exception: Sys_error "opentheory/hol-light.int: No such file or directory".

Naeem Abbasi notnaeemabbasi at gmail.com
Sun Oct 10 14:48:05 UTC 2010


Hello,

I installed opentheory earlier today on my PC with Ubuntu 10.04. I am
having difficulty in converting a hol-light theory to an opentheory
proof article.

I am following the instructions in one of the examples described in
FAQs,  "How can I generate a proof article file from a HOL Light
theory file?", Step 3,

--------------------------
File "help.ml" already loaded
- : unit = ()
- : unit = ()
- : unit = ()
	Camlp5 Parsing version 5.15

# #use "bool.ml";;
- : unit = ()
Exception: Sys_error "opentheory/hol-light.int: No such file or directory".
#
---------------------------

I am not quite sure what I may have done wrong. Can any one help?

Thanks

Naeem



More information about the opentheory-users mailing list