# Snapshot of Isabelle definitions of RISC-V

This directory contains snapshots of the Isabelle theories generated by Sail
for the RISC-V model (RV32 and RV64).

A heap image containing the architecture definitions (as well as the Lem and
Sail libraries in the [lem](lem/) subdirectory) can be built using

```
isabelle build -b -D .
```

This takes roughly 10 minutes on an Intel Core i7-7700 with 64GB RAM.

An interactive session based on this heap image can be started using the
following command (replacing `$DIR` with the path of this directory):

```
isabelle jedit -d $DIR -l Sail-RV64
```

The model was built with
* `sail` release 0.10, commit `da307c67`
* `sail-riscv` commit `7e6ffe2`
and checked against Isabelle 2018.
