Merge pull request #961 from lean-ja/fix-warning

`flexible` リンタの警告が消えない問題の修正
lean-ja · Oct 7, 2024 · 15b6236 · 15b6236
2 parents 01e2189 + 2fa7081
commit 15b6236
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -25,7 +25,7 @@ jobs:
       - name: lean action
         uses: leanprover/lean-action@v1
         with:
-          build-args: "--log-level=error"
+          build-args: "--fail-level=warning"
 
   # Lean の更新により Windows 環境でだけビルドが壊れる可能性もあるので、
   # 念のために Windows 環境でもビルドを行う

diff --git a/LeanByExample/Reference/Option/Flexible.lean b/LeanByExample/Reference/Option/Flexible.lean
@@ -55,14 +55,17 @@ end --#
 -/
 section --#
 
--- flexible tactic リンタを有効にする
-set_option linter.flexible true
+-- 技術的な理由で、一時的に flexible tactic リンタを無効にしている --#
+set_option linter.flexible false --#
 
 /--
 warning: 'simp' is a flexible tactic modifying '⊢'…
 note: this linter can be disabled with `set_option linter.flexible false`
 -/
 #guard_msgs (warning) in
+  -- 技術的な理由で、`#guard_msgs` のスコープ内でリンタを有効にしている
+  set_option linter.flexible true in
+
   example {n m : Nat} (h : n = m) : True ∧ (n = m) := by
     simp
     exact h