lakefile.toml

name = "SSA"
precompileModules = true # Ensure that reflective code that uses native_decide runs compiled code, not in the ir_interpreter.
defaultTargets = ["SSA"]

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "nightly-testing-2025-01-28"

[[require]]
name = "Cli"
git = "https://github.com/mhuisi/lean4-cli.git"
rev = "nightly"

[[require]]
name = "leanwuzla"
git = "https://github.com/hargoniX/Leanwuzla.git"
rev = "main"

[[lean_lib]]
name = "SSA"

[[lean_lib]]
name = "AliveExamples"
roots = ["SSA.Projects.InstCombine.AliveAutoGenerated"]

[[lean_lib]]
name = "AliveStatements"
roots = ["SSA.Projects.InstCombine.AliveStatements"]

[[lean_lib]]
name = "AliveScaling"
roots = ["SSA.Projects.InstCombine.ScalingTest"]

[[lean_exe]]
name = "mlirnatural"
root = "SSA.MLIRNatural"

[[lean_exe]]
name = "bv-circuit-profile"
root = "SSA.Experimental.Bits.Fast.Profile"

[[lean_exe]]
name = "opt"
root = "SSA.Projects.InstCombine.LLVM.Opt"
supportInterpreter = true

[[lean_exe]]
name = "ssaLLVMEnumerator"
root = "SSA.Projects.InstCombine.LLVM.Enumerator"