hol-light-materials

Online materials for HOL Light:

• Tutorial
• Reference Manual (pdf, html)
• Very Quick Reference (pdf, txt)

Building & Running HOL Light

Assuming that OPAM is installed in your machine. you can easily build HOL Light using the following instructions which are also described in README:

make switch
eval $(opam env)
make
# Now you have 'hol.sh' .

Checkpointing

DMTCP is recommended (README of HOL Light has more instructions). Once dmtcp_restart_script.sh is created, you can create multiple instances of HOL Light by starting the script with distinct ports -p <port number>.

Editors

• VSCode: vscode-hol-light is available at VSCode Marketplace.
• Emacs: hol-light-emacs

Fundamentals and Internal Representation of Terms

• Fundamentals
• AST

How-to

• Use or update assumptions in HOL Light
• Use rewrite tactics well
• Debug a tactic
• Prove 'trivial' goals

HOL Light vs. Coq

Examples and Exercises

• exercises: exercises for HOL Light
• s2n-bignum-examples: examples for proving assembly programs in s2n-bignum

Misc