lakefile.toml

name = "batteries"
testDriver = "BatteriesTest"
lintDriver = "runLinter"
defaultTargets = ["Batteries", "runLinter"]

[leanOptions]
linter.missingDocs = true
# We prefix this with `weak.` so that running `lake new my_project math`
# with an older default toolchain doesn't fail when running the Mathlib post update hook.
# This option should be removed entirely once Batteries stops using `backward.privateInPublic`.
weak.backward.privateInPublic.warn = false

[[lean_lib]]
name = "Batteries"

[[lean_lib]]
name = "BatteriesTest"
globs = ["BatteriesTest.+"]
leanOptions = {linter.missingDocs = false}

[[lean_exe]]
name = "runLinter"
srcDir = "scripts"
supportInterpreter = true

[[lean_exe]]
name = "test"
srcDir = "scripts"

# `lake exe shake` checks files for unnecessary imports.
[[lean_exe]]
name = "shake"
root = "Shake.Main"
supportInterpreter = true