perf: do not lint unused variables defined in tactics by default #5338

Kha · 2024-09-13T11:49:50Z

Should ensure we visit at most as many expr nodes as in the final expr instead of many possibly overlapping mvar assignments. This is likely the only way we can ensure acceptable performance in all cases.

src/Lean/Server/InfoUtils.lean

leanprover-community-mathlib4-bot · 2024-09-13T12:10:31Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5f789e63fa6db9fdd0c46f00e15a0d1da6a212a1 --onto 2080fc022187595020d519c1e08aa72340c4b5ff. (2024-09-13 12:10:31)
💥 Mathlib branch lean-pr-testing-5338 build failed against this PR. (2024-09-18 12:02:12) View Log
💥 Mathlib branch lean-pr-testing-5338 build failed against this PR. (2024-09-23 09:53:45) View Log
💥 Mathlib branch lean-pr-testing-5338 build failed against this PR. (2024-09-23 11:37:09) View Log
💥 Mathlib branch lean-pr-testing-5338 build failed against this PR. (2024-09-23 16:06:07) View Log
✅ Mathlib branch lean-pr-testing-5338 has successfully built against this PR. (2024-09-24 02:05:57) View Log
💥 Mathlib branch lean-pr-testing-5338 build failed against this PR. (2024-09-24 15:59:10) View Log
🟡 Mathlib branch lean-pr-testing-5338 build against this PR was cancelled. (2024-09-26 06:44:38) View Log
🟡 Mathlib branch lean-pr-testing-5338 build against this PR was cancelled. (2024-09-26 06:54:06) View Log
❌ Mathlib branch lean-pr-testing-5338 built against this PR, but linting failed. (2024-09-26 07:35:38) View Log
🟡 Mathlib branch lean-pr-testing-5338 build against this PR was cancelled. (2024-09-27 05:58:14) View Log
❌ Mathlib branch lean-pr-testing-5338 built against this PR, but linting failed. (2024-09-27 06:48:06) View Log
❌ Mathlib branch lean-pr-testing-5338 built against this PR, but was unexpectedly noisy. (2024-09-27 10:43:01) View Log
❌ Mathlib branch lean-pr-testing-5338 built against this PR, but was unexpectedly noisy. (2024-10-02 23:59:47) View Log
❌ Mathlib branch lean-pr-testing-5338 built against this PR, but testing failed. (2024-10-03 07:09:05) View Log
❌ Mathlib branch lean-pr-testing-5338 built against this PR, but testing failed. (2024-10-03 09:56:22) View Log
❌ Mathlib branch lean-pr-testing-5338 built against this PR, but testing failed. (2024-10-03 10:14:09) View Log
✅ Mathlib branch lean-pr-testing-5338 has successfully built against this PR. (2024-10-03 10:26:42) View Log

kim-em · 2024-09-26T04:16:38Z

What is the plan here? It generates a massive number of warnings (~4200) in Mathlib.

Reconsider the design?
Resolve them all in Mathlib. There are enough that it is probably worth automating.

Update: All fixed in Mathlib, with adaptation notes for the edge cases. Touches over 900 files.

…pensive than traversal over finished proof term

leanprover-community-bot · 2024-10-17T00:23:01Z

Mathlib CI status (docs):

❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-10-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-10-17 00:23:00)
🟡 Mathlib branch lean-pr-testing-5338 build against this PR was cancelled. (2024-10-17 15:59:08) View Log

Kha requested a review from mhuisi as a code owner September 13, 2024 11:49

Kha force-pushed the unused-in-tactics branch from d01f21d to 448f998 Compare September 13, 2024 11:50

mhuisi approved these changes Sep 13, 2024

View reviewed changes

src/Lean/Server/InfoUtils.lean Outdated Show resolved Hide resolved

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 13, 2024

Kha force-pushed the unused-in-tactics branch from 448f998 to ea68a45 Compare September 13, 2024 15:58

Kha changed the base branch from master to nightly-with-mathlib September 13, 2024 16:00

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 18, 2024

Update lean-toolchain for testing leanprover/lean4#5338

99e1a40

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 18, 2024

Update lean-toolchain for testing leanprover/lean4#5338

70ecfe1

leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Sep 18, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 23, 2024

Trigger CI for leanprover/lean4#5338

dc5da60

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 23, 2024

Trigger CI for leanprover/lean4#5338

41ee1e5

Kha force-pushed the unused-in-tactics branch from 81aa906 to 1e42149 Compare September 23, 2024 11:20

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 23, 2024

Trigger CI for leanprover/lean4#5338

49c5535

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 23, 2024

Trigger CI for leanprover/lean4#5338

f0d6ba3

Kha force-pushed the unused-in-tactics branch from 1e42149 to 316be7e Compare September 23, 2024 15:47

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 23, 2024

Trigger CI for leanprover/lean4#5338

719d343

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 23, 2024

Trigger CI for leanprover/lean4#5338

964c34f

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 24, 2024

bump batteries for leanprover/lean4#5338

9c7bf4f

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 24, 2024

bump batteries for leanprover/lean4#5338

1064ebb

leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Sep 24, 2024

Kha force-pushed the unused-in-tactics branch from 316be7e to fb9e582 Compare September 24, 2024 14:43

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 24, 2024

Trigger CI for leanprover/lean4#5338

66287b1

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 24, 2024

Trigger CI for leanprover/lean4#5338

846598f

leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Sep 24, 2024

Kha added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Sep 26, 2024

kim-em requested a review from hargoniX as a code owner September 27, 2024 03:17

leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 3, 2024

Kha pushed a commit to leanprover-community/mathlib4 that referenced this pull request Oct 8, 2024

bump batteries for testing against leanprover/lean4#5338

ea2f380

kim-em changed the base branch from nightly-with-mathlib to master October 16, 2024 04:11

Kha marked this pull request as ready for review October 16, 2024 11:15

Kha and others added 11 commits October 17, 2024 09:28

perf: do not lint unused variables defined in tactics by default

d11b6be

minimize visited exprs

99e8f38

chore: fix up unused variables

9a1fce7

restrict to parameters in presence of tactics, avoid any work more ex…

79dbb64

…pensive than traversal over finished proof term

fix tests

6cb9d3b

cover let rec bodies containing proofs

14427f3

fix

b79d0c9

always analyze body term

51bc434

fix

2fcd9a2

fix

b2784b0

trigger mathlib CI

22f7c34

kim-em force-pushed the unused-in-tactics branch from 52fb143 to 22f7c34 Compare October 16, 2024 22:28

Revert unnecessary changes

af875b4

kim-em approved these changes Oct 16, 2024

View reviewed changes

linter changes

8243ef0

update moddoc

2d27691

Kha enabled auto-merge October 17, 2024 09:29

Kha added this pull request to the merge queue Oct 17, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 17, 2024

Trigger CI for leanprover/lean4#5338

9846d01

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 17, 2024

Trigger CI for leanprover/lean4#5338

03eeecd

Merged via the queue into leanprover:master with commit f2ac0d0 Oct 17, 2024
15 checks passed

Kha deleted the unused-in-tactics branch October 18, 2024 09:22

kim-em mentioned this pull request Oct 21, 2024

Instantiate metavars takes enormously long in VSCode, but is snappy in the terminal #5614

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

perf: do not lint unused variables defined in tactics by default #5338

perf: do not lint unused variables defined in tactics by default #5338

Kha commented Sep 13, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented Sep 13, 2024 •

edited by leanprover-community-bot

Loading

kim-em commented Sep 26, 2024 •

edited

Loading

leanprover-community-bot commented Oct 17, 2024 •

edited

Loading

perf: do not lint unused variables defined in tactics by default #5338

perf: do not lint unused variables defined in tactics by default #5338

Conversation

Kha commented Sep 13, 2024 • edited Loading

leanprover-community-mathlib4-bot commented Sep 13, 2024 • edited by leanprover-community-bot Loading

kim-em commented Sep 26, 2024 • edited Loading

leanprover-community-bot commented Oct 17, 2024 • edited Loading

Kha commented Sep 13, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented Sep 13, 2024 •

edited by leanprover-community-bot

Loading

kim-em commented Sep 26, 2024 •

edited

Loading

leanprover-community-bot commented Oct 17, 2024 •

edited

Loading