Home |
Software |
Publications |
Various |
Contact Us
# Tactician

### What is Tactician?

Tactician is a tool for helping you maintain and/or understand HOL Light
proof scripts. Its main function is to refactor the ML of a tactic proof,
typically to package up a "g/e" style proof into a "prove" style proof, or vice
versa, to flatten out a "prove" style proof into a series of "g/e" style
interactive steps. This can help experienced users maintain their proof
scripts, and novices learn from existing proof scripts.

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.
It is capable of refactoring tactic proofs written in the following styles:

- HOL Light's interactive "g and e" style (even incomplete proofs);
- HOL Light's batch "prove" style;
- The Flyspeck project's batch "prove-by-refinement" style.

Tactician also supports various other related activities, such as
visualising the tree of subgoals of a tactic proof, spotting slow tactic
applications and duplicate theorems, and viewing the dependencies between
theorems. These facilities are particularly useful when managing large proof
rojects.

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/main.ml";;`

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.