Skip to content

Commit

Permalink
chore: migrate to lakefile.toml (#396)
Browse files Browse the repository at this point in the history
With Lean 4.8 we now can use toml for the lakefile (which is the
preferred variant now), so this PR migrates our build to toml.

---------

Co-authored-by: Tobias Grosser <[email protected]>
  • Loading branch information
goens and tobiasgrosser authored Jul 8, 2024
1 parent cb95e52 commit b064c26
Show file tree
Hide file tree
Showing 3 changed files with 42 additions and 42 deletions.
2 changes: 1 addition & 1 deletion docgen.sh
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
set -o xtrace
set -e
lake -R exe cache get # load mathlib from cache
lake -R -Kdoc=on build SSA:docs
lake -R build SSA:docs
41 changes: 0 additions & 41 deletions lakefile.lean

This file was deleted.

41 changes: 41 additions & 0 deletions lakefile.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
name = "SSA"
defaultTargets = ["SSA"]

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "nightly-testing-2024-07-05"

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

[[require]]
name = "doc-gen4"
git = "https://github.com/leanprover/doc-gen4"
rev = "main"

[[lean_lib]]
name = "SSA"

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

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

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

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

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

0 comments on commit b064c26

Please sign in to comment.