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" on ocaml interface, I'm facing the following errors:
File "/home/elif/hol-light/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" , 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" , 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
