---
name: "hol-light"
section: "1"
platform: "linux"
package: "hol-light"
version: "1:3.0.0-2+b7"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/hol-light"
---

# hol-light(1)

HOL Light interactive theorem prover

## NAME

hol-light - HOL Light interactive theorem prover

## SYNOPSIS

**hol-light** \[options...\]

## DESCRIPTION

The command **hol-light** is a simple wrapper for calling  **ocaml** and loading the HOL Light basic definitions (by loading */usr/share/hol-light/hol.ml* instead of  **.ocamlinit** as initialization file). Loading these definitions takes about 2 minutes on modern hardware, please be patient. All options and other arguments are passed as options to **ocaml.**

If you have a  **readline-editor** such as **rlwrap, ledit or rlfe** installed, the  **hol-light ocaml** toplevel is wrapped in **readline-editor.** Install just one of these readline editors or configure your preferred one via the alternative system.

## SEE ALSO

[**ocaml**(1)](/ocaml/1.md), **readline-editor**(1), [**rlwrap**(1)](/rlwrap/1.md), [**ledit**(1)](/ledit/1.md), [**rlfe**(1)](/rlfe/1.md)\
 HOL Light documentation at  *http://www.cl.cam.ac.uk/~jrh13/hol-light/*

## AUTHOR

The  **hol-light** script and this manual page were written by Hendrik Tews \<hendrik@askra.de\>, specifically for the Debian project (and may be used by others).