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

[Joe Hurd]

Hi Naeem,

Sorry for the delayed response - I've just returned from a vacation in the UK.

I'm afraid the instructions in the FAQ for extracting theorems from
HOL Light were out of date, since I'm actively working on extracting
HOL Light theories to test the new theory repo:

http://opentheory.gilith.com/packages/

I've updated the instructions in the FAQ

http://www.gilith.com/software/opentheory/faq.html

as part of a new release of the tool, opentheory 1.0 (release
20101020), which is available from

http://www.gilith.com/software/opentheory/

Please have another try and let me know if there are further problems.

Cheers,

Joe

On Sun, Oct 10, 2010 at 7:48 AM, Naeem Abbasi <notnaeemabbasi at gmail.com> wrote:
> 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
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>