Hi Petros,
Thank you for your response. Yes, it is warning and seems like running.
But, when I want to load "Multivariate/realanalysis.ml" or "Multivariate/
cauchy.ml" theories; after loading almost 45 minutes, system killed and I
couldn't load these theories. So, I thought maybe it is not proper
installation and tried to install again.
I then followed the steps given in bitbucket.org/akrauss/hol-light-workbench.
But, it gives folllowing error:
# #use "hol.ml";;
val hol_version : string = "2.20++"
val hol_dir : string ref =
{contents = "/home/elif/hol-light-workbench/hol-light/trunk"}
val temp_path : string ref = {contents = "/tmp"}
Cannot find file camlp5o.cma.
- : unit = ()
Cannot find file /home/elif/hol-light-workbench/hol-light/trunk/pa_j.cmo.
- : unit = ()
val use_file : string -> unit = <fun>
val hol_expand_directory : string -> string = <fun>
.
.
val needs : string -> unit = <fun>
- : unit = ()
- : unit = ()
val quotexpander : string -> string = <fun>
File "/home/elif/hol-light-workbench/hol-light/trunk/system.ml", line 34,
characters 0-13:
Error: Unbound module Quotation
Error in included file /home/elif/hol-light-workbench/hol-light/trunk/
system.ml
- : unit = ()
File "/home/elif/hol-light-workbench/hol-light/trunk/lib.ml", line 22,
characters 8-9:
Error: Syntax error
I installed ocaml (4.01) and camlp5 (6.11) with sudo as you advised.
Hol-Light seemed to be worked, again. For example, I can load "Library/
analysis.ml" or "Library/prime.ml" etc. But, when I want to load bigger
theory like Multivariate theory, system gives same error:
.
.
#killed
What did I miss? Any suggestions would be appreciated...
Regards,
Freek Wiedijk <fr...@cs.ru.nl>, 23 Haz 2020 Sal, 09:22 tarihinde şunu yazdı:
> Dear all,
>
> Some time ago (in the times of Debian Stretch :-)) I made
> a Dockerfile for HOL Light, see the attachment.
>
> The commands I used for building the image and running
> it are:
>
> docker build -t hol-light .
> docker run -i -v /home/freek:/home/freek --name hol-light hol-light
>
> You need to run the build command in the directory (".") that
> has the Dockerfile in it. Of course, the directory you
> want to mount in the container in your case probably will
> not be /home/freek :-)
>
> Then at the ocaml prompt ("# ") when running the image,
> I input some ocaml commands:
>
> #use "hol.ml";;
> loads "update_database.ml";;
> #load "unix.cma";;
> let cd path = Unix.chdir path;;
> let pwd () = Unix.getcwd ();;
> let ls () = Unix.system "/bin/ls -C";;
> cd "/home/freek";;
> ls ();;
>
> I have Docker checkpointing enabled
> in my /etc/docker/daemon.json, see
> https://docs.docker.com/engine/reference/commandline/checkpoint/,
> so in a different window I then gave the command:
>
> docker checkpoint create hol-light hol
>
> This creates the checkpoint. Finally, I then run HOL Light
> every time using:
>
> docker start -i --checkpoint hol hol-light
>
> It still takes some time to start, but you don't have
> to go through the initialisation of the system with #use
> "hol.ml";; every time...
>
> Unfortunately, you cannot have two instances of this running
> at the same time. If someone can tell me how to do that
> (I'm not really a Docker user), I would appreciate that.
>
> Even if you don't want to use docker, the Dockerfile shows
> commands to install the system in a way that works :-) I
> _think_ I even tested that the SOS stuff works in this setup.
>
> Hope this is useful to someone.
>
> Freek
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
