diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index c953232a..438de104 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -35,6 +35,12 @@ jobs: with: use-github-cache: false + - name: check that LeanBandits.lean is up to date + run: ~/.elan/bin/lake exe mk_all --check + + - name: Lint project + run: env LEAN_ABORT_ON_PANIC=1 ~/.elan/bin/lake exe runLinter LeanBandits + - name: Compile blueprint and documentation uses: leanprover-community/docgen-action@095763bcfa35bef9c6a3eb8ae778c5e6c7727df2 # 2025-07-03 with: diff --git a/lakefile.toml b/lakefile.toml index 10f5b839..e00690bf 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -2,37 +2,12 @@ name = "LeanBandits" defaultTargets = ["LeanBandits"] [leanOptions] -weak.linter.docPrime = false -weak.linter.hashCommand = true -weak.linter.oldObtain = true -weak.linter.style.refine = true -weak.linter.style.cdot = true -weak.linter.style.dollarSyntax = true -weak.linter.style.header = true -weak.linter.style.lambdaSyntax = true -weak.linter.style.longLine = true -weak.linter.style.longFile = 1500 -weak.linter.style.missingEnd = true -weak.linter.style.multiGoal = true -weak.linter.style.setOption = true pp.unicode.fun = true autoImplicit = false relaxedAutoImplicit = false - -[moreServerOptions] -linter.docPrime = false -linter.hashCommand = true -linter.oldObtain = true -linter.style.refine = true -linter.style.cdot = true -linter.style.dollarSyntax = true -linter.style.header = true -linter.style.lambdaSyntax = true -linter.style.longLine = true -linter.style.longFile = 1500 -linter.style.missingEnd = true -linter.style.multiGoal = true -linter.style.setOption = true +weak.linter.flexible = true # no rigid tactic (e.g. `exact`) after a flexible tactic (e.g. `simp`) +# Enable all mathlib linters: automatically matches what mathlib uses. +weak.linter.mathlibStandardSet = true [[require]] name = "mathlib" diff --git a/scripts/nolints.json b/scripts/nolints.json new file mode 100644 index 00000000..9d61646d --- /dev/null +++ b/scripts/nolints.json @@ -0,0 +1,6 @@ +[["docBlame", "Bandits.rewardByCount"], + ["docBlame", "Bandits.ucbArm"], + ["docBlame", "Bandits.ucbWidth"], + ["docBlame", "Bandits.ℱ"], + ["docBlame", "Bandits.Bandit.measure"], + ["docBlame", "Bandits.Bandit.streamMeasure"]]