name = "EvmAsm"
version = "0.0.1"
defaultTargets = ["EvmAsm"]
leanOptions = []

[[require]]
name = "mathlib"
scope = "leanprover-community"

# FORK of Sail-generated RISC-V spec (https://github.com/dhsorens/sail-riscv-lean); pulls in lean-sail.
[[require]]
name = "Lean_RV64D"
git = "https://github.com/dhsorens/sail-riscv-lean"
rev = "main"

[[lean_lib]]
name = "EvmAsm"
# clang's default -fbracket-depth=256 trips on the deeply-nested
# C ternary chain that Lean emits for the `lookupProgram` /
# `lookupProgramTail` `match` cascade.  Each new probe arm adds
# one bracket layer; we already brush the limit at ~240 arms.
moreLeancArgs = ["-fbracket-depth=4096"]

[[lean_exe]]
name = "codegen"
root = "Main"
supportInterpreter = true

[[lean_exe]]
name = "progress-report"
root = "MainProgress"
supportInterpreter = true

[[lean_exe]]
name = "div128-v5-check"
root = "MainDiv128V5Check"
supportInterpreter = true

[[lean_exe]]
name = "arith-diff-check"
root = "MainArithDiffCheck"
supportInterpreter = true