adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

haskell: update documentation for building the Haskell kernel

This commit is contained in:
Matthew Brecknell 2017-02-03 11:24:40 +11:00
parent aee13996a6
commit d08ee04e2f
2 changed files with 13 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
README.md
View File

@ -128,9 +128,10 @@ For running the standalone version of the C Parser you will additionally need
* [MLton][7] ML compiler (package `mlton-compiler` on Ubuntu)
For building the Haskell kernel model, GHC 7.8.x is currently required.
Note that this repository does not contain the QEmu interface for actually
running the model.
For building the Haskell kernel model, the Haskell build tool [stack][] is
required. The Haskell kernel `Makefile` will use `stack` to obtain appropriate
versions of `ghc` and `cabal-install`. Note that this repository does not
contain the QEmu interface for actually running the model.
For running the C proofs, you need a working C preprocessor setup for the seL4
repository.
@ -167,6 +168,7 @@ need a gcc-compatible C pre-processor and python. Try the following steps:
[7]: http://mlton.org "MLton ML compiler"
[8]: http://sel4.systems/Info/GettingStarted/DebianToolChain.pml "seL4 tool chain setup"
[9]: https://pypi.python.org/pypi/setuptools "python package installer"
[stack]: https://haskellstack.org/
Isabelle Setup

13
spec/haskell/README.md
View File

@ -17,17 +17,20 @@ stand-alone; it must be integrated into a simulator that can run user-level
binaries and generate events that the kernel model can process.
To build it:
- install `GHC 7.8.x`
- install `Cabal 1.20.x`. This is usually included with GHC 7.8.
- install the Haskell build tool [stack][].
- run `make`
The `Makefile` will use `stack` to fetch appropriate versions of `ghc` and
`cabal-install`.
After that, you can compile Haskell programs using the simulator by adding
`-package SEL4-ARM` to the `ghc` command line. Note that the qemu target
requires some callback functions to be accessible via the FFI, so it is not
possible to load a model compiled for those targets in GHCi.
`-package SEL4` to the `ghc` command line. Note that the qemu target requires
some callback functions to be accessible via the FFI, so it is not possible to
load a model compiled for those targets in GHCi.
Currently, the simulator interface is out of date, so this model is currently
only useful as documentation and as intermediate artefact in the seL4
correctness proof. The model itself is kept up to date with the C code, only
the simulator interface is outdated.
[stack]: https://haskellstack.org/