Add opam and META files, add '-dir' to hol.sh, other updates

This patch
- adds opam and META files.
- add '-dir' to hol.sh: 'hol.sh -dir' prints its HOLLIGHT_DIR variable. This is convenient when one wants to know where hol light is installed :)
- increases version at hol.ml to "3.0.0+" ('+' is to describe that there are updates after the official release)
- updates README to explain how to use OPAM to install HOL Light

The contents of 'opam' file is equivalent to the already published version to the OPAM repository
https://github.com/ocaml/opam-repository/blob/master/packages/hol_light/hol_light.3.0.0/opam
modulo:
- A reference to the released tar.gz
- `extra-source "META"` because the META file will now be included in hol-light with this patch
- Version number and some extra stuffs (they seem to extract those from the directory path)

META was necessary to help ocamlfind locate package 'hol_light'.
When HOL Light is installed during OPAM installation, I uploaded this file at gist.github.com and
download it; but I think it is a wiser idea to explicitly put it in this repo. :)

META

@@ -0,0 +1,5 @@
+version = "3.0.0+"
+description = "The HOL Light interactive theorem prover"
+requires = "camlp5 zarith"
+archive(byte) = "hol_lib.cma"
+archive(native) = "hol_lib.cmxa"

README

@@ -27,7 +27,21 @@ Refer to the reference manual for more details of individual functions:
 The Objective CAML (OCaml) implementation is a prerequisite for running
 HOL Light. HOL Light should work with any recent version of OCaml; I've
 tried it on at least 3.04, 3.06, 3.07+2, 3.08.1, 3.09.3, 3.10.0, 3.11.2,
-4.00, 4.05 and 4.14 and 5.2.0.
+4.00, 4.05, 4.14, 5.1.0 and 5.2.0.
+
+The easiest way to install HOL Light is through OPAM, an OCaml package
+manager. After installing OPAM (https://opam.ocaml.org/doc/Install.html),
+run the following command:
+
+    opam install hol_light
+    # To compile the core module of HOL Light and use, add hol_light_module
+    # opam install hol_light hol_light_module
+
+This will build 'hol.sh' and copy it at the 'bin' path of your OPAM setting,
+making it executable at any location.
+
+To manually build HOL Light, OCaml and a few packages that HOL Light depends on
+are necessary.
 
  1. OCaml: there are packages for many Linux distributions. For
     example, on a debian derivative like Ubuntu, you may just need
@@ -41,13 +55,14 @@ tried it on at least 3.04, 3.06, 3.07+2, 3.08.1, 3.09.3, 3.10.0, 3.11.2,
 
         http://caml.inria.fr/ocaml/index.en.html
 
-  2. Dependencies: HOL Light uses camlp5 and zarith (num for OCaml
-    version < 4.14). If you have OPAM installed on your machine,
-    running the following command inside this directory will create a local
-    OPAM switch which uses the latest OCaml version that fully supports
-    features of as well as all dependencies installed:
+ 2. Dependencies: Using OPAM (OCaml package manager) is the easiest way to
+    install dependent packages (https://opam.ocaml.org/doc/Install.html).
+    If you have OPAM installed on your machine, running the following command
+    inside this directory will create a local OPAM switch which uses the
+    latest OCaml version that fully supports features of as well as all
+    dependencies installed:
 
-        make switch
+        make switch # or 'make switch-5' for OCaml 5
         eval $(opam env)
 
     To manually install dependencies, the DEPENDENCIES chapter of this document

hol.ml

@@ -9,7 +9,7 @@
 (*              (c) Copyright, John Harrison 1998-2007                       *)
 (* ========================================================================= *)
 
-let hol_version = "2.20++";;
+let hol_version = "3.0.0+";;
 
 #directory "+compiler-libs";;
 

hol_4.14.sh

@@ -1,8 +1,16 @@
 #!/bin/bash
 
-if [ "$#" -eq 1 ] && [ "$1" == "-pp" ]; then
-  echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo"
-  exit 0
+# Makefile will replace __DIR__ with the path
+export HOLLIGHT_DIR=__DIR__
+
+if [ "$#" -eq 1 ]; then
+  if [ "$1" == "-pp" ]; then
+    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo"
+    exit 0
+  elif [ "$1" == "-dir" ]; then
+    echo "${HOLLIGHT_DIR}"
+    exit 0
+  fi
 fi
 
 # The default ocaml REPL does not accept arrow keys.
@@ -12,8 +20,6 @@ if [ "${LINE_EDITOR}" == "" ]; then
   LINE_EDITOR="ledit"
 fi
 
-# Makefile will replace __DIR__ with the path
-export HOLLIGHT_DIR=__DIR__
 export HOLLIGHT_USE_MODULE=__USE_MODULE__
 
 # If a local OPAM is installed, use it

hol_4.sh

@@ -1,8 +1,16 @@
 #!/bin/bash
 
-if [ "$#" -eq 1 ] && [ "$1" == "-pp" ]; then
-  echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo"
-  exit 0
+# Makefile will replace __DIR__ with the path
+export HOLLIGHT_DIR=__DIR__
+
+if [ "$#" -eq 1 ]; then
+  if [ "$1" == "-pp" ]; then
+    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo"
+    exit 0
+  elif [ "$1" == "-dir" ]; then
+    echo "${HOLLIGHT_DIR}"
+    exit 0
+  fi
 fi
 
 # The default ocaml REPL does not accept arrow keys.
@@ -12,8 +20,6 @@ if [ "${LINE_EDITOR}" == "" ]; then
   LINE_EDITOR="ledit"
 fi
 
-# Makefile will replace __DIR__ with the path
-export HOLLIGHT_DIR=__DIR__
 export HOLLIGHT_USE_MODULE=__USE_MODULE__
 
 # If a local OPAM is installed, use it

opam

@@ -0,0 +1,75 @@
+opam-version: "2.0"
+name: "hol_light"
+version: "3.0.0"
+synopsis: "The HOL-Light interactive theorem prover"
+description: """
+HOL Light is a computer program written by John Harrison to help users prove
+interesting mathematical theorems completely formally in higher order logic.
+It sets a very exacting standard of correctness, but provides a number of
+automated tools and pre-proved mathematical theorems (e.g. about arithmetic,
+basic set theory and real analysis) to save the user work. It is also fully
+programmable, so users can extend it with new theorems and inference rules
+without compromising its soundness. There are a number of versions of HOL,
+going back to Mike Gordon’s work in the early 80s. Compared with other HOL
+systems, HOL Light uses a much simpler logical core and has little legacy code,
+giving the system a simple and uncluttered feel. Despite its simplicity, it
+offers theorem proving power comparable to, and in some areas greater than,
+other versions of HOL, and has been used for some significant
+industrial-scale verification applications.
+
+This package will install `hol.sh` which will run OCaml REPL with HOL Light
+loaded.
+To use a compiled module of HOL Light, please install with the
+hol_light_module OPAM package.
+"""
+authors: "HOL Light"
+license: "https://github.com/jrh13/hol-light/blob/master/LICENSE"
+homepage: "https://hol-light.github.io/"
+bug-reports: "https://github.com/jrh13/hol-light/issues"
+dev-repo: "git+https://github.com/jrh13/hol-light.git"
+maintainer: ["John Harrison <[email protected]>" "Juneyoung Lee <[email protected]>"]
+depopts: [ "hol_light_module" ]
+depends: [
+  ("ocaml" {> "4.02.0" & < "4.04.0"} &
+   "camlp5" {>= "6.15" & <= "7.1"})
+  |
+  ("ocaml" {>= "4.04.0" & < "4.06.0"} &
+   "camlp5" {>= "7.01" & <= "7.1"})
+  |
+  ("ocaml" {>= "4.06.1" & < "4.08.0"} &
+   "num" &
+   "camlp5" {>= "7.06" & < "7.15"} &
+   "ledit")
+  |
+  ("ocaml" {>= "4.08.0" & < "4.10.0"} &
+   "num" &
+   "camlp5" {>= "7.11" & < "8.01"} &
+   "ledit")
+  |
+  ("ocaml" {>= "4.10.0" & < "4.14.0"} &
+   "num" &
+   "camlp5" {>= "7.14"} &
+   "ledit")
+  |
+  ("ocaml" {>= "4.14.0"} &
+   "camlp5" {>= "8.0"} &
+   "zarith" {>= "1.5"} &
+   "ledit")
+]
+available: os = "linux" | os = "macos" | os = "cygwin"
+build: [
+  [make] {!hol_light_module:installed}
+  [make "HOLLIGHT_USE_MODULE=1"] {hol_light_module:installed}
+  ["sh" "-c" "sed \"s^%{hol_light:build}%^%{hol_light:lib}%^g\" hol.sh >hol_new.sh"]
+  ["mv" "hol_new.sh" "hol.sh"]
+  ["chmod" "+x" "hol.sh"]
+]
+install: [
+  ["mkdir" "-p" "%{hol_light:lib}%"]
+  ["cp" "-r" "." "%{hol_light:lib}%"]
+  ["cp" "hol.sh" "%{bin}%/hol.sh"]
+]
+remove: [
+  ["rm" "%{bin}%/hol.sh"]
+  ["rm" "-rf" "%{hol_light:lib}%"]
+]