Hi Elif,
On 24/06/2020 18:19, elif deniz wrote:
Hi Petros,
Thank you for your response. Yes, it is warning and seems like
running. But, when I want to load "Multivariate/realanalysis.ml
<http://realanalysis.ml>" or "Multivariate/cauchy.ml
<http://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 haven't seen this happen before and I don't think there is enough
context to figure it out.
The Multivariate theory is very large and it does take quite a bit of
time* to load fully, but I can't think of what could be killing it.
I then followed the steps given in
bitbucket.org/akrauss/hol-light-workbench
<http://bitbucket.org/akrauss/hol-light-workbench>. But, it gives
folllowing error:
I am not familiar with this script, but it seems quite old (last update
in 2012, loading HOL Light from the old repo, etc). Again, I would
strongly recommend using opam if you are installing OCaml from scratch.
Freek's suggestion with Docker looks simpler to set up though.
(I did not know about the Docker checkpointing feature, so thank you for
that pointer Freek!)
Regards,
Petros
* Took 26 minutes on an i5-4570 just now.
Freek Wiedijk <fr...@cs.ru.nl <mailto: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 <http://hol.ml>";;
loads "update_database.ml <http://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 <http://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 <mailto: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
--
Dr. Petros Papapanagiotou
Chancellor's Fellow in Digital Technologies
School of Informatics, The University of Edinburgh
Academic Coordinator
IoT Research & Innovation Service
Homepage: http://homepages.inf.ed.ac.uk/ppapapan/
AI Modelling Lab: https://aiml.inf.ed.ac.uk/
AI and its Applications Institute: http://web.inf.ed.ac.uk/aiai
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
