Introduction

This is an Isabelle/HOL theory that describes and proves the correctness of the Cap9 kernel specification. There is a pdf version of this theory, but you are free to install Isabelle and open it directly.

Warning: this is work in progress, so everything is subject to change.

Build

To manually build a pdf or html versions of the theory you need to install the following prerequisites:

• Isabelle2019
• pdflatex
• make

Make sure that isabelle command is available from the terminal: you may need to manually add the path to the Isabelle bin directory to the PATH environment variable.

PDF

To build a pdf file just run the following command:

$ make pdf

The file will be created in the output folder.

HTML

It is also possible to create a nicely colored HTML version of the theory that will look like this. Execute the following command:

$ make html

Generated HTML files will be created in a separate directory, the path to which will be printed on the screen.