blob: cabf4fc021a650e39bfd557c23525b1bd2981776 (
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
|
# 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. You can tell Isabelle where to
find them using the `-d` flag, as in
```
isabelle jedit -l Sail -d lib/lem -d lib/sail 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).
|
