The main branch of this (unofficial) fork includes various improvements not yet merged upstream. For example, this version is compatible with Coq 8.14 (rather than the original repository which uses Coq 8.9). Please feel free to examine the git history to see the other changes since the repositories diverged at commit 603866.
This codebase may only be used for educational, research or evaluation purposes, and not for commercial use. This is because the DeepSEA compiler includes files taken and modified from CompCert, so it is developed pursuant to the CompCert licence. Please see the CompCert licence for the full details. You may also wish to look at the INRIA CompCert research project website or the CompCert GitHub repository.
The Shentu Chain webpage has more information about the DeepSEA project, and there are blog posts An Introduction to DeepSEA and How DeepSEA Works (see also the version on the Internet Archive).
Please let us know what you think! Feedback can be sent to deepsea@certik.org or for feedback specific to this fork, feel free to raise an issue.
This directory contains the OCaml parts of the DeepSEA compiler. For the time being, we do not include the sources for the parts that are written in Coq, but we ship the Ocaml files which were compiled from them.
In order to build it, use opam or Nix to install the prerequisites, and then run make:
opam install .
make edsger
mv _build/default/Edsger/edsger.bc dsc
OR
nix-shell
make edsger
mv _build/default/Edsger/edsger.bc dsc
To install the dependencies using Nix, run nix-shell from the root of the repository to install most dependencies without opam (install npm packages separately). Nix is a package manager available on Linux, macOS, and (via WSL) Windows. You can get Nix here.