HOL for Sublime Text

A HOL ITP (https://hol-theorem-prover.org/) development environment built on top of slimmed down, heavily modified versions of SublimeREPL (https://github.com/wuub/SublimeREPL), SublimeANSI (https://github.com/aziz/SublimeANSI), and SML-syntax (https://github.com/Takaia/SML-syntax) put together.

Features

HOL Files

• HOL Syntax Highlighting
• Tab completion from ` to smart quote pair ‘’
  • Also from `` to “”
• Unicode tab completion within HOL terms for common HOL ASCII sequences
  • Logical Symbols
    • ! to ∀
    • ? to ∃
    • ~ to ¬
    • ==> to ⇒
    • ...and many more!
  • The lower case greek alphabet
    • 'a to α
    • 'b to β
    • ... and so on...

HOL REPL

• Unicode tab completion features in REPL entry also
• Full colour REPL (Uses HOL's vt100_terminal backend)
• Complete REPL history and scrollback
• Send selection, lines, and entire files straight to REPL in Sublime
• Automatically format selection/lines into:
  • Goals
  • Subgoals
    • Basic subgoals
    • Sufficient Condition
  • Tactics
  • Quiet mode
• Changes Flags from menus or key bindings
  • Show Types
  • Show Assums
  • Print Goal at Top
  • Print Free Variables

Installation

• You must have HOL installed and accessible through the command hol
• Install the HOL package from PackageControl (https://packagecontrol.io/)
• OR clone this repository into your Packages folder and rename it to HOL

Usage

• HOL submenu under Tools in Sublime for all the operations and their keybindings
• A right click context menu exists to kill/restart the REPL and send signals including SIGINT
• For more details and more control please see the key bindings and preference files available under the preferences menu
• Note: The terminal is speedy enough for interactive use but large imports should be done in quiet mode as they can take some time to colourise!

License

Parts of this project are under GPLv2 and parts under MIT, please see LICENSE.txt