hol_light_moduleversion
A flag for compiling HOL Light core to a bytecode and native module
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.
| Author | HOL Light |
|---|---|
| License | https://github.com/jrh13/hol-light/blob/master/LICENSE |
| Published | |
| Homepage | https://hol-light.github.io |
| Issue Tracker | https://github.com/jrh13/hol-light/issues |
| Maintainers | John Harrison <jrh013@gmail.com> and Juneyoung Lee <aqjune@gmail.com> |
| Dependencies |
|
| Source [http] | https://github.com/aqjune/hol-light-module/archive/refs/tags/1.0.tar.gz md5=232eeb03c8fa6f4f7d076943ad652582 sha512=ec0ae802a6977366b26e0438670579cf3a3d329d3600ae5e2493a01867259d74bc3a09d7f27efd31ef96b6385fdce089aa06fb04611db2077f37aa9d66ce0cfe |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/hol_light_module/hol_light_module.1.0/opam |
Optionally used by
