From 54f43e016a41910e1a29abd3940e154d32920cb5 Mon Sep 17 00:00:00 2001
From: Juneyoung Lee <aqjune@gmail.com>
Date: Fri, 20 Jun 2025 08:30:39 -0500
Subject: [PATCH] Add hol_light 3.1.0

---
 packages/hol_light/hol_light.3.1.0/opam | 89 +++++++++++++++++++++++++
 1 file changed, 89 insertions(+)
 create mode 100644 packages/hol_light/hol_light.3.1.0/opam

diff --git a/packages/hol_light/hol_light.3.1.0/opam b/packages/hol_light/hol_light.3.1.0/opam
new file mode 100644
index 000000000000..b4eec9c2c177
--- /dev/null
+++ b/packages/hol_light/hol_light.3.1.0/opam
@@ -0,0 +1,89 @@
+opam-version: "2.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 <jrh013@gmail.com>" "Juneyoung Lee <aqjune@gmail.com>"]
+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"} &
+   "ocaml-base-compiler" &
+   "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}%"]
+]
+extra-source "META" {
+  src: "https://gist.githubusercontent.com/aqjune/4b5b54a88b208672d3bc3d764675cb89/raw/107b3d14af6852f39fbf3a885d2c421e5b98617b/META"
+  checksum: [
+    "sha256=0e3725fbfe2ddc503781895cd0401cb0c2d8f11b715c6d3421e2233076c2cf11"
+    "md5=553360015351e37ffbee4760aa96af93"
+  ]
+}
+url {
+  src:
+    "https://github.com/jrh13/hol-light/archive/refs/tags/Release-3.1.0.tar.gz"
+  checksum: [
+    "md5=00ff3680c6651158795388280a28b906"
+    "sha512=0cdf9753c2cbcdbbad34f6df42490ca03324819ad78b1f5cb3d7fe24ec364c07bd7a656ce7bde3adf281f1074052e217fa77853097da4125865c64ad74335f53"
+  ]
+}