Setup

Quick setup

Clone the following repository: https://github.com/workflowfm/hol-light

1git clone https://github.com/workflowfm/hol-light.git

Then make sure all the submodules are initialised and updated:

1git submodule update --init --recursive

Manual setup

Assuming an existing installation of HOL Light, you can setup the reasoner manually by installing the following libraries:

  1. The Isabelle Light library. This also comes bundled with HOL Light by default.
  2. Additional HOL Light tools. This consists of useful snippets of code, libraries, and theorems. This should be installed in a tools/ directory within HOL Light.
  3. The HOL Light embed library which enables reasoning with encoded logics. This should be installed in a embed/ directory within HOL Light.
It is important to use the correct directory names, as the reasoner will seek to load specific files from each library.

Finally, install the reasoner itself by cloning the repository to a workflowfm/ directory within HOL Light:

1git clone https://github.com/workflowfm/workflowfm-reasoner.git worklfowfm