-
Notifications
You must be signed in to change notification settings - Fork 10
/
INSTALL
20 lines (16 loc) · 815 Bytes
/
INSTALL
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
At time of writing the current development version of HOL4
is required to use this software. So, clone from
https://github.com/HOL-Theorem-Prover/HOL
and install using that software's installation instructions.
HOL4 must be installed with polyml, which is good as it's
much faster using that method.
If you wish to build the dissertation, a moderately recent
version of LaTeX is required. A number of extensions are
required, notably recent versions of latexmk and the proof
enviroment. To my knowledge, these are installed automatically
with MacTeX but not with ubuntu
(although texlive-full includes both).
Once the dependencies are built, the software can be built with
Holmake, the relevant targets being all, l1c, and dissertation.
Dissertation produces the file diss.pdf, l1c produces the executable
l1c.