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.
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.
To build a pdf file just run the following command:
$ make pdfThe file will be created in the output folder.
It is also possible to create a nicely colored HTML version of the theory that will look like this. Execute the following command:
$ make htmlGenerated HTML files will be created in a separate directory, the path to which will be printed on the screen.