# Isabelle Snapshots of Sail Specifications

This directory contains snapshots of the Isabelle theories generated by Sail
for the [CHERI-MIPS](cheri/), [RISC-V](riscv/), and [ARM v8.3](aarch64/)
specifications, together with snapshots of the Sail and Lem libraries.  These
snapshots are provided for convenience, and are not guaranteed to be
up-to-date.

In order to open a theory of one of the specifications in Isabelle, use the `-l
Sail` command-line flag to load the session containing the Sail library.
Snapshots of the Sail and Lem libraries are in the [lib/sail](lib/sail/) and
[lib/lem](lib/lem/) directories, respectively.  The ROOTS file in this directory
contains pointers to them; you can tell Isabelle to use it with the `-d` flag,
as in

```
isabelle jedit -l Sail -d . riscv/Riscv.thy
```

This will open the RISC-V specification.

The file [Manual.thy](Manual.thy) (and its PDF rendering in
[Manual.pdf](Manual.pdf)) contains an introduction on how to use the Sail
specifications in Isabelle.

The Lem library files in `lib/lem` have been generated from the
[Lem](https://github.com/rems-project/lem) sources.  The Lem license can be
found in [lib/lem/LICENSE](lib/lem/LICENSE).