The following advice was compiled by Zili Wang. Please follow the instructions below for installing Isabelle/HOL on your machines, and link the Archive of Formal Proofs (AFP)!
You can download Isabelle
here and the AFP
here (choose the current stable version). There are some instructions on how to link the AFP for each OS
here.
You will know that you have done this correctly if you can load the
Test.thy file without errors, meaning there should be no red loading highlights in the file after a few minutes!
Some platform specific instructions:
Linux Instructions (thanks to Chris Johannsen)
For anyone using linux, here are the steps I took to install Linux and link up the AFP.
-
Download Isabelle from this page:
https://isabelle.in.tum.de/
-
Extract the contents via tar -xvf Isabelle2023_linux.tar.gz to obtain the
Isabelle2023/ directory
-
You should be able to run Isabelle by executing ./Isabelle2023/Isabelle2023
-
Download the archive of formal proofs from this page:
https://www.isa-afp.org/download/
-
Extract the contents via tar -xvf afp-current.tar.gz to obtain the
afp-2023-09-26/ directory (or something similar)
-
/path/to/Isabelle2023/bin/isabelle components -u /path/to/afp-2023-09-26/thys
Windows Instructions
Here are the steps I followed to install Isabelle and linking to AFP.
-
Note: it doesn't matter where you install this, but you do need to know where this folder is for step 4
-
-
Note: in step 3 of the guide linked, the target directory should just be C:\
-
Go to the Isabelle installation folder and double click Cygwin-Terminal.bat
-
A terminal should pop up. Run this in the terminal:
isabelle components -u /cygdrive/c/afp/thys