§ Setting up SAIL for porting to Lean

• Since I have no idea how to use opam, but I do not the older Coq setup via makefiles, that's what I'll be using.

§ Directory Structure

.
├── bbv -> sail-src/bbv/
└── sail-src
    ├── bbv@master:c53d5b95c7
    ├── coq-sail@main:843059
    └── sail@sail2:ba9f7f1

• In general, it's a welcome, pleasant surprise that everything works on tip-of-tree.
• We first build bbv, which is a library for bitvector theory. We then build coq-sail. Finally, we build sail.
• Yes, we need two copies of bbv. coq-sail uses the bbv from:

root/sail-src/coq-sail$ ../../bbv`
 -> root/bbv

• sail itself, in its test suite, uses the bbv from:

root/sail/test/coq$ ../../../bbv
 -> root/sail-src/bbv/

§ Grabbing the right ocaml

root$ opam switch create 5.1.0
root$ eval $(opam config env) 

§ Building bbv

root$ cd bbv && make -j$(nproc) && make install

§ Building bbv

root$ cd sail-src/coq-sail/src && make -j$(nproc) && make install

§ Building sail

root$ cd sail && cat INSTALL.md
root$ cd sail && make -j $(nproc) && make install

§ What's needed to port to Lean

There's quite a bit of obsolete stuff in the Coq backend at the moment that you could safely skip. sail coq backend by default generates a shallow embedding. It's probably worth looking at katamaran, though. I don't think a deep embedding is too hard, it's partly just a case of deciding what the output language should look like.