Hi Elif,
I am not sure what went wrong with your first attempt. The chunk you
pasted contains no errors, only warnings.
The other errors you are getting are errors with installing OCaml. It is
trying to install it globally, but you are not giving it permission to
do that.
You can either (a) run all commands with a "sudo" prefix or (b) install
locally using ./configure --prefix=/home/elif/ocaml (for instance).
A much better third option is to install OCaml (and camlp5 and anything
else you need) using opam: https://opam.ocaml.org/
This can help you manage a local installation, including packages, or
even multiple installations so you can pick the one that works with HOL
Light.
Hope this helps.
Regards,
Petros
On 22/06/2020 11:21, elif deniz wrote:
Dear all,
I'm trying to install HOL-Light on Ubuntu 14.04 and following the
instruction on Github website. When I do #use "hol.ml
<http://hol.ml/>" on ocaml interface, I'm facing the following errors:
File "/home/elif/hol-light/impconv.ml <http://impconv.ml/>" , line
315, characters 8-174:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(Var_(_ , _)|Const_ (_ , _, _))
File "/home/elif/hol-light/impconv.ml <http://impconv.ml/>" , line
456, characters 22-45:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
[ ]
File "/home/elif/hol-light/impconv.ml <http://impconv.ml/>" , line
1780, characters 16-27:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(_, [ ] )
----------------------------------------------------------------------------------------------------------------------------------
Then, I tried to install Ocaml-4.01.0 and camlp5-6.11 from sources.
Here my actions:
cd ocaml-4.01.0
./configure
make world
make install
if test -d /usr/local/bin; then : ; else mkdir -p /usr/local/bin; fi
if test -d /usr/local/lib/ocaml; then : ; else mkdir -p
/usr/local/lib/ocaml; fi
if test -d /usr/local/lib/ocaml/stublibs; then : ; else mkdir -p
/usr/local/lib/ocaml/stublibs; fi
if test -d /usr/local/lib/ocaml/compiler-libs; then : ; else mkdir -p
/usr/local/lib/ocaml/compiler-libs; fi
if test -d /usr/local/man/man1; then : ; \
else mkdir -p /usr/local/man/man1; fi
cp VERSION /usr/local/lib/ocaml/
cp: cannot create regular file ‘/usr/local/lib/ocaml/VERSION’:
Permission denied
make: *** [install] Error 1
sudo make install
make[1]: Entering directory `/home/elif/Downloads/ocaml-4.01.0/byterun'
cp ocamlrun /usr/local/bin/ocamlrun
cp: cannot create regular file ‘/usr/local/bin/ocamlrun’: Text file busy
make[1]: *** [install] Error 1
make[1]: Leaving directory `/home/elif/Downloads/ocaml-4.01.0/byterun'
make: *** [install] Error 2
--------------------------------------------------------------------------------------------------------------------------------
After this, I tried to install camlp5-6.11
./configure --strict
make world.opt
make install
it gives following error:
rm: cannot remove ‘/usr/local/lib/ocaml/camlp5/pa_mkast.o’: Permission
denied
rm: cannot remove ‘/usr/local/lib/ocaml/camlp5/pr_extfun.cmo’:
Permission denied
rm: cannot remove ‘/usr/local/lib/ocaml/camlp5/plexer.cmx’: Permission
denied
rm: cannot remove ‘/usr/local/lib/ocaml/camlp5/pr_o.cmx’: Permission
denied
make: *** [install] Error 1
---------------------------------------------------------------------------------------------------------------------------------
They are not properly installed and HOL system gives errors. How can I
fix it? Would anyone be able to help me on how to install HOL-Light?
Regards,
_______________________________________________
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
