lakefile.toml

name = "cslib"
version = "0.1.0"
defaultTargets = ["Cslib"]
testDriver = "CslibTests"
lintDriver = "batteries/runLinter"

[leanOptions]
weak.linter.mathlibStandardSet = true
weak.linter.flexible = true
# The next three linters are provided by Mathlib, but don't work here.
# This should be fixed, see discussion at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weak.2Elinter.2EmathlibStandardSet.20and.20lint-style-action/with/544726745
weak.linter.pythonStyle = false
weak.linter.checkInitImports = false
weak.linter.allScriptsDocumented = false
# this is currently not extensible for unicode not used in Mathlib
weak.linter.unicodeLinter = false

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "2c99b7bf363ce6123c6f22241b920cbd310be945"

[[lean_lib]]
name = "Cslib"

[[lean_lib]]
name = "CslibTests"
leanOptions = {weak.linter.style.header = false}

[[lean_exe]]
name = "checkInitImports"
srcDir = "scripts"
root = "CheckInitImports"