This is the implementation accompanying the ITP 2019 paper "Virtualization of HOL4 in Isabelle" by Fabian Immler, Jonas Rädle, and Makarius Wenzel.

This file describes how to set up Poly/ML, HOL4, and Isabelle for hol4isabelle on Linux. It shall set up a hierarchy of directories like this. HOL must be a subdirectory of hol4isabelle, the location of isabelle and polyml is not too relevant.

hol4isabelle
|
|__ HOL
|
|__ isabelle
|
|__ polyml

In order to build HOL, download and install Poly/ML (5.8)

Clone HOL (the version below is tested to work) and build the kernel (this generates a couple of SML files that are required to run hol4isabelle, e.g., src/postkernel/TheoryDatTokens.sml)

git clone https://github.com/HOL-Theorem-Prover/HOL.git
cd HOL
git checkout b7716bd92

poly < tools/smart-configure.sml
bin/build --seq=tools/sequences/kernel
cd ..

git clone https://github.com/CakeML/cakeml.git
cd cakeml
git checkout 76ed0b0508

Download Isabelle2021 from https://isabelle.in.tum.de/website-Isabelle2021/. From here on we refer to the main Isabelle executable Isabelle2021/bin/isabelle as simply isabelle

Alternatively (in order to work with the repository):

hg clone http://isabelle.in.tum.de/repos/isabelle/rev/Isabelle2021
isabelle components -I
isabelle components -a
isabelle build -b HOL

isabelle jedit -d . -l Core_Isabelle Example/Example_Transfer.thy

isabelle jedit -d . -l HOL Core_Isabelle.thy

isabelle jedit -d . -l Pure Core_Original.thy

• Theory OpenTheoryImport requires the Isabelle-OpenTheory importer as a subdirectory in hol4isabelle:

git clone https://github.com/xrchz/isabelle-opentheory.git
cd isabelle-opentheory
git checkout f04496c
cd ..

• build OpenTheory .art files with HOL4's loggingKernel:

cd HOL
bin/build cleanAll
bin/build --otknl

This requires

• The Windows Subsystem for Linux, with Ubuntu 18.04
• An installation of the Isabelle2021 application

Most of the installation is just like under Linux, with the following exceptions:

• especially for polyml, make sure that everything is installed in a directory under the WSL home directory
• all commands involving that involve "./isabelle/bin/isabelle" must be executed in the Cygwin-Terminal (in the Isabelle2021) folder
• before building HOL, do

  echo 'val HOLDIR = "c:/path/to/hol4isabelle/HOL"' > tools-poly/poly-includes.sml
  

  because otherwise (due to WSL) HOLDIR = "/mnt/c/path/to/hol4isabelle/HOL" and this will confuse hol4isabelle.