From 6ef635fff0b2427aa63675fd0a5f524a7eb0b033 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?= <remydegenne@gmail.com>
Date: Tue, 2 Sep 2025 13:11:44 +0200
Subject: [PATCH 1/3] Update linter options in lakefile.toml

Use Mathlib linters.
---
 lakefile.toml | 31 +++----------------------------
 1 file changed, 3 insertions(+), 28 deletions(-)

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"

From 6e7a8a947ee38fdf902e3a746a583c3a84dbd798 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Tue, 2 Sep 2025 13:13:21 +0200
Subject: [PATCH 2/3] add linting step in CI

---
 .github/workflows/blueprint.yml | 6 ++++++
 1 file changed, 6 insertions(+)

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:

From 0c2e5c794f4d496dfaa226441ebc35aed6be24d6 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Tue, 2 Sep 2025 13:16:17 +0200
Subject: [PATCH 3/3] add nolints for missing docstrings

---
 scripts/nolints.json | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 scripts/nolints.json

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"]]