From 2fa708178330d16401623b8f17aa19d84ff83d45 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 8 Oct 2024 04:45:10 +0900
Subject: [PATCH] =?UTF-8?q?`flexible`=20=E3=83=AA=E3=83=B3=E3=82=BF?=
 =?UTF-8?q?=E3=81=AE=E8=AD=A6=E5=91=8A=E3=81=8C=E6=B6=88=E3=81=88=E3=81=AA?=
 =?UTF-8?q?=E3=81=84=E5=95=8F=E9=A1=8C=E3=81=AE=E4=BF=AE=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/ci.yml                     | 2 +-
 LeanByExample/Reference/Option/Flexible.lean | 7 +++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index cbbefee5..a8ce1a2d 100644
--- 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
index 69a5980e..55647f78 100644
--- 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