From d21e1d5ca984acfd69d95c7ebd106587625a590d Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 13 Nov 2024 02:43:41 +0900 Subject: [PATCH 1/4] =?UTF-8?q?`linter.style.multiGoal`=20=E3=82=92?= =?UTF-8?q?=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B=20Fixes=20#1006?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Option/MultiGoal.lean | 31 +++++++++++++++++++ booksrc/SUMMARY.md | 1 + 2 files changed, 32 insertions(+) create mode 100644 LeanByExample/Reference/Option/MultiGoal.lean diff --git a/LeanByExample/Reference/Option/MultiGoal.lean b/LeanByExample/Reference/Option/MultiGoal.lean new file mode 100644 index 00000000..d01a7ab1 --- /dev/null +++ b/LeanByExample/Reference/Option/MultiGoal.lean @@ -0,0 +1,31 @@ +/- # linter.style.multiGoal + +`linter.style.multiGoal` は、よくない証明の書き方を指摘するリンターの一つです。 + +Lean では、複数のサブゴールがあるときにタクティクを実行すると最初のゴールに対して実行されるのですが、証明を構造化するという観点からは、ゴールの一つにフォーカスする（infoview に一つしかゴールが表示されないようにする）べきです。 +このリンタはそのような問題を指摘します。 +-/ +import Mathlib.Tactic.Linter.MultiGoal + +set_option linter.style.multiGoal true + +/-- +warning: There are 2 unclosed goals before 'exact hP' and at least one remaining goal afterwards. +Please focus on the current goal, for instance using `·` (typed as "\."). +note: this linter can be disabled with `set_option linter.style.multiGoal false` +-/ +#guard_msgs in + example {P Q : Prop} (hP : P) (hQ : Q) : P ∧ Q := by + -- ゴールが２つ生成される + constructor + + -- この時点でサブゴールが２つあるのに、 + -- フォーカスせずにタクティクを実行しているので警告が出る + exact hP + exact hQ + +-- 良い証明の例 +example {P Q : Prop} (hP : P) (hQ : Q) : P ∧ Q := by + constructor + · exact hP + · exact hQ diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 8339e4ef..b009f7e9 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -76,6 +76,7 @@ - [autoImplicit: 自動束縛暗黙引数](./Reference/Option/AutoImplicit.md) - [hygiene: マクロ衛生](./Reference/Option/Hygiene.md) - [linter.flexible: 脆弱な証明を指摘する](./Reference/Option/Flexible.md) + - [linter.style.multiGoal: フォーカス強制](./Reference/Option/MultiGoal.md) - [relaxedAutoImplicit: 更にautoImplicit](./Reference/Option/RelaxedAutoImplicit.md) - [型クラス](./Reference/TypeClass/README.md) From 7ebc6403f26bbd348cdb55399b77392a6764841c Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 13 Nov 2024 02:49:26 +0900 Subject: [PATCH 2/4] =?UTF-8?q?CI=20=E3=81=AE=20build=20args=20=E3=81=AE?= =?UTF-8?q?=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 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a8ce1a2d..ecc08c2c 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: "--fail-level=warning" + build-args: "--log-level=warning --fail-level=warning" # Lean の更新により Windows 環境でだけビルドが壊れる可能性もあるので、 # 念のために Windows 環境でもビルドを行う From b8a8c37fa511b1355c2d4c1db8919f998ad4758b Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 13 Nov 2024 02:58:54 +0900 Subject: [PATCH 3/4] =?UTF-8?q?CI=20=E3=82=92=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 | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ecc08c2c..2cf81303 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,7 +25,12 @@ jobs: - name: lean action uses: leanprover/lean-action@v1 with: - build-args: "--log-level=warning --fail-level=warning" + build-args: "--log-level=warning" + + - name: lean action (warning as fail) + uses: leanprover/lean-action@v1 + with: + build-args: "--fail-level=warning" # Lean の更新により Windows 環境でだけビルドが壊れる可能性もあるので、 # 念のために Windows 環境でもビルドを行う From 02eb170a32d4db9d9bcf97eefb151ba2c6651737 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 13 Nov 2024 03:08:55 +0900 Subject: [PATCH 4/4] =?UTF-8?q?import=20=E3=81=95=E3=82=8C=E3=82=8B?= =?UTF-8?q?=E3=83=95=E3=82=A1=E3=82=A4=E3=83=AB=E5=90=8D=E3=82=92=E4=BF=AE?= =?UTF-8?q?=E6=AD=A3=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Option/MultiGoal.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanByExample/Reference/Option/MultiGoal.lean b/LeanByExample/Reference/Option/MultiGoal.lean index d01a7ab1..e04d8ceb 100644 --- a/LeanByExample/Reference/Option/MultiGoal.lean +++ b/LeanByExample/Reference/Option/MultiGoal.lean @@ -5,7 +5,7 @@ Lean では、複数のサブゴールがあるときにタクティクを実行すると最初のゴールに対して実行されるのですが、証明を構造化するという観点からは、ゴールの一つにフォーカスする（infoview に一つしかゴールが表示されないようにする）べきです。 このリンタはそのような問題を指摘します。 -/ -import Mathlib.Tactic.Linter.MultiGoal +import Mathlib.Tactic.Linter.Multigoal set_option linter.style.multiGoal true