Skip to content

SublimeHOL - A HOL Development Environment built on top of SublimeREPL

License

Unknown and 2 other licenses found

Licenses found

Unknown
LICENSE.TXT
GPL-2.0
GPL-LICENSE.TXT
MIT
MIT-LICENSE.TXT
Notifications You must be signed in to change notification settings

HOL-Theorem-Prover/SublimeHOL

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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.

HOL Plugin Screenshot

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

About

SublimeHOL - A HOL Development Environment built on top of SublimeREPL

Resources

License

Unknown and 2 other licenses found

Licenses found

Unknown
LICENSE.TXT
GPL-2.0
GPL-LICENSE.TXT
MIT
MIT-LICENSE.TXT

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Python 100.0%