From 61ea41581b8b400d563fc015c26e4662027c732a Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Tue, 22 Oct 2024 11:43:15 -0500 Subject: [PATCH] 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 | 5 ++++ README | 29 ++++++++++++++++----- hol.ml | 2 +- hol_4.14.sh | 16 ++++++++---- hol_4.sh | 16 ++++++++---- opam | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 125 insertions(+), 18 deletions(-) create mode 100644 META create mode 100644 opam diff --git a/META b/META new file mode 100644 index 00000000..d86b6657 --- /dev/null +++ b/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" diff --git a/README b/README index d18342b1..d77441ce 100644 --- a/README +++ b/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 diff --git a/hol.ml b/hol.ml index 15e68063..19749f7b 100644 --- a/hol.ml +++ b/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";; diff --git a/hol_4.14.sh b/hol_4.14.sh index c807ed5c..0fa0f64c 100755 --- a/hol_4.14.sh +++ b/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 diff --git a/hol_4.sh b/hol_4.sh index 3c8feb4a..be55568a 100755 --- a/hol_4.sh +++ b/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 diff --git a/opam b/opam new file mode 100644 index 00000000..3c827e94 --- /dev/null +++ b/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 " "Juneyoung Lee "] +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}%"] +]