Please note this plugin is unmaintained.
A HOL ITP (https://hol-theorem-prover.org/) development environment. Some parts taken from SML-syntax (https://github.com/Takaia/SML-syntax).
- HOL Theorem Prover (https://hol-theorem-prover.org/)
- Sublime Text plugin Terminus (https://github.com/randy3k/Terminus)
- An installed C Compiler
- You must have HOL installed (https://hol-theorem-prover.org/)
- You must have Terminus installed (https://github.com/randy3k/Terminus)
- Clone this repository into your Packages folder and rename it to HOL
- Inside the newly renamed
HOL
repo you cloned, buildfilter.c
with your favourite C compiler to an executable calledfilter
in the same folder. For example:
gcc filter.c -o filter
- In the Sublime Text menu select
Preferences -> Package Settings -> HOL -> Settings-User
- In opened settings file enter:
{ "holpath":"/your/path/to/binary/here/hol" }
- In the plugin folder (should be called
HOL
) in the Sublime Text packages folder rungit pull
- Recompile
filter.c
using you favourite C compiler to an executable calledfilter
. For example:gcc filter.c -o filter
- HOL Syntax Highlighting
- Tab completion from
`
to smart quote pair‘’
- Also from
``
to“”
- Also from
- Unicode tab completion within HOL terms for common HOL ASCII sequences
- Logical Symbols
!
to∀
?
to∃
~
to¬
==>
to⇒
- ...and many more!
- The Greek alphabet
'a
toα
'b
toβ
'c
toγ
and'C
toΓ
'd
toδ
and'D
toΔ
'e
toε
'f
to'ζ
'g
toη
'h
toθ
'i
toι
'j
toκ
- (No
'k
or'K
binding) 'l
toμ
'm
toν
'n
toξ
and'N
toΞ
- (No
'o
or'O
binding) 'p
toπ
and'P
toΠ
'q
toρ
'r
toς
's
toσ
and'S
toΣ
't
toτ
'u
toυ
'v
toφ
and'V
toΦ
'w
toχ
'x
toψ
and'X
toΨ
'y
toω
and'Y
toΩ
- (No
'z
or'Z
binding)
- Logical Symbols
- Full colour REPL (Uses HOL's
vt100_terminal
backend) - 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
- You cannot directly type in the REPL but instead work from a HOL file
HOL
submenu under Tools in Sublime for all the operations and their keybindings- Note you must work from a file, you cannot directly type in the REPL
- For more details and more control please see the key bindings and preference files available under the preferences menu
- To change the colour scheme of the REPL use the "Terminus Utilities: Select Theme" command in Sublime Text
- 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!
Everything is licensed under GPLv2, please see LICENSE.txt