blob: d2b4fe7133814944aabdbc75a2ee1b1b9605ad82 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
# 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).
|
