Package hol-light-module.1.0

packages/hol-light-module/hol-light-module.1.0/opam

@@ -0,0 +1,29 @@
+opam-version: "2.0"
+authors: "HOL Light"
+homepage: "https://hol-light.github.io"
+bug-reports: "https://github.com/jrh13/hol-light/issues"
+maintainer: ["John Harrison <[email protected]>" "Juneyoung Lee <[email protected]>"]
+depends: [
+  "ocaml" {>= "4.14.0"}
+]
+synopsis: "A flag for compiling HOL Light core to a bytecode and native module"
+license: "https://github.com/jrh13/hol-light/blob/master/LICENSE"
+dev-repo: "git+https://github.com/jrh13/hol-light.git"
+description: """
+Installing this package makes the hol-light package to build the
+bytecode and native module of HOL Light core as well.
+
+NOTE: This extends the trusted base of HOL Light to include its inliner script,
+inline_loads.ml. inline_loads.ml is an OCaml program in HOL Light that receives
+an HOL Light proof and replaces the loads/loadt/needs function invocations with
+their actual contents. Please install this package only if having this
+additional trusted base is considered okay.
+"""
+url {
+  src:
+    "https://github.com/aqjune/hol-light-module/archive/refs/tags/1.0.tar.gz"
+  checksum: [
+    "md5=2e1c7f71547d9a42a956c06a39b1a26e"
+    "sha512=2c6c1c6aefc22a2704d87d4230d7d3a599f1aac372cc9c5786c60a1c59fc75515426a37a74cc271ee859d00729769b130971c57cb8a476e288b739902296fe43"
+  ]
+}