Skip to content

Commit

Permalink
chore: cleanup lakefile (#296)
Browse files Browse the repository at this point in the history
This is in preparation for considering moving to the lakefile TOML
format.
  • Loading branch information
bollu authored May 10, 2024
1 parent b834bb1 commit 3813f67
Showing 1 changed file with 0 additions and 27 deletions.
27 changes: 0 additions & 27 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -35,35 +35,8 @@ lean_lib AliveScaling {
roots := #[`SSA.Projects.InstCombine.ScalingTest]
}

--
-- lean_lib «AliveAll» {
-- roots := #[`Projects.AliveAll]
-- }
--
-- lean_lib «Tensor1D» {
-- roots := #[`Projects.Tensor1D.Tensor1D]
-- }
--
-- lean_lib «InstCombine» {
-- srcDir := "Projects/InstCombine"
-- roots := #[`InstCombinePeepholeRewrites]
-- roots := #[`InstCombinePeepholeRewrites]
-- }
--
-- -- Experiments
-- -- ===========
--
-- lean_lib «Bits» {
-- roots := #[`Experiment.Bits.Decide]
-- }

-- NOTE: this must be 'm'mathlib, as indicated from:
-- https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"

require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly"

require partax from git "https://github.com/tydeu/lean4-partax" @ "master"

meta if get_config? doc = some "on" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

0 comments on commit 3813f67

Please sign in to comment.