Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 1 commit into from
Oct 23, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions META
Original file line number Diff line number Diff line change
@@ -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"
29 changes: 22 additions & 7 deletions README
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion hol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)

let hol_version = "2.20++";;
let hol_version = "3.0.0+";;

#directory "+compiler-libs";;

Expand Down
16 changes: 11 additions & 5 deletions hol_4.14.sh
Original file line number Diff line number Diff line change
@@ -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.
Expand All @@ -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
Expand Down
16 changes: 11 additions & 5 deletions hol_4.sh
Original file line number Diff line number Diff line change
@@ -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.
Expand All @@ -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
Expand Down
75 changes: 75 additions & 0 deletions opam
Original file line number Diff line number Diff line change
@@ -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}%"]
]
Loading