# 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).  This snapshots is provided for
convenience, and is not guaranteed to be up-to-date.

It requires [Isabelle 2020](https://isabelle.in.tum.de/website-Isabelle2020/index.html)
to build.

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-riscv](https://github.com/rems-project/sail-riscv) commit `b1db5b9`
  * [sail](https://github.com/rems-project/sail) commit `63343363`
  * [lem](https://github.com/rems-project/lem) commit `ga839114`
and checked against Isabelle 2020.
