Proof Technologies Ltd
Home | Software | Publications | Various | Contact Us


What is Tactician?

Tactician is a tool for helping you maintain and/or understand HOL Light tactic proof scripts. It is intended both for experienced users managing large proof projects, and for novices hoping to learn from existing proof scripts.

Tactician's main function is to refactor tactic proofs, particularly for refactoring between different styles of tactic proof. This enables batch-style proofs to be stepped through interactively, and interactive-style proofs to be automatically batched up. Tactician also supports visualising the tree of subgoals of a tactic proof, spotting slow tactic applications and duplicate theorems, and viewing the dependencies between theorems.

Once loaded into a HOL Light session, it runs in the background, dynamically capturing tactic proofs as they are executed, and outputting upon user request. The following styles of tactic proof are supported:

See here for some simple examples of its refactoring capability. We have also written a paper giving an overview of Tactician and its implementation.

Download and Installation

A source tarball for the latest version can be downloaded here:

hollight_tactician-3.1.tgz (released 2015-01-10).

Unpack the downloaded tarball as a subdirectory of your existing HOL Light installation directory, by executing the following command from a terminal window, to result in a directory called Tactician:

tar -xzf hollight_tactician-3.1.tgz -C your-hollight-dir

Users are encouraged to rebuild OCaml specially for Tactician usage. Doing this avoids the need to execute promote_all_values before each proof you want to refactor (see below). See the Tactician release README for full details on how to rebuild.

Tactician can be loaded into an existing HOL Light session in about 5 to 30 seconds (depending on your system hardware and how many theorems have already been proved in the session) by executing the following ML directive in the HOL Light session (where the first # indicates the OCaml prompt):

# #use "Tactician/";;

Tactician is then ready to record and refactor proofs in terms of the ML bindings referred to in the original proof script. For a full description of Tactician's capabilities, see USER_GUIDE bundled with the Tactician release.