§ Setting up SAIL for porting to Lean



§ Directory Structure


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


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


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.