perf: cache intermediate type class results and non-results #4272

JovanGerb · 2024-05-24T23:16:11Z

Cache intermediate type class successes and failures. A cleaned up version of #4152, (on that branch I was experimenting with some other stuff)

Note: in some tests, the numbers in metavariables have lowered. This is because less new metavariables are created during type class search, so the name generator is used less.

leanprover-community-mathlib4-bot · 2024-05-24T23:40:54Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-4272 build failed against this PR. (2024-05-24 23:40:52) View Log
💥 Mathlib branch lean-pr-testing-4272 build failed against this PR. (2024-05-25 00:07:44) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-25 01:34:49) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-25 02:53:27) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-25 04:32:42) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-25 13:52:18) View Log
🟡 Mathlib branch lean-pr-testing-4272 build against this PR was cancelled. (2024-05-25 15:14:02) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-25 16:06:44) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-25 18:21:23) View Log
🟡 Mathlib branch lean-pr-testing-4272 build this PR didn't complete normally. (2024-05-25 19:31:33) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-25 21:25:32) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-25 23:31:33) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-26 11:59:39) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-26 15:00:25) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-27 17:10:33) View Log
🟡 Mathlib branch lean-pr-testing-4272 build this PR didn't complete normally. (2024-05-28 22:39:16) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-29 00:02:08) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-29 02:57:08) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-29 11:48:43) View Log
❌ Mathlib branch lean-pr-testing-4272 built against this PR, but testing failed. (2024-05-31 23:23:16) View Log

This reverts commit 0d438bc.

feat: cache intermediate type class results and non-results

6757a3a

JovanGerb marked this pull request as draft May 24, 2024 23:16

.

66728e9

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

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

Update lean-toolchain for testing leanprover/lean4#4272

07e9358

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

Update lean-toolchain for testing leanprover/lean4#4272

2b46c19

leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan full-ci labels May 24, 2024

fix: don't cache negative results for unfinished searches

ccee383

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

Trigger CI for leanprover/lean4#4272

afcb8a8

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

Trigger CI for leanprover/lean4#4272

b4ca549

fix: check for loops

fe5f8fa

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

Trigger CI for leanprover/lean4#4272

d394f7e

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

Trigger CI for leanprover/lean4#4272

ee8fec7

JovanGerb added 2 commits May 25, 2024 02:22

more sophisticated loop detection

9ceeb0d

fix sign

3fa159e

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

Trigger CI for leanprover/lean4#4272

0b79050

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

Trigger CI for leanprover/lean4#4272

c6b57e9

JovanGerb added 2 commits May 25, 2024 03:13

fix tests

e3d454e

clean up

97ea4a6

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

Trigger CI for leanprover/lean4#4272

73ac42f

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

Trigger CI for leanprover/lean4#4272

46e1820

cache whenever the key isn't α-reduced

0d438bc

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

Trigger CI for leanprover/lean4#4272

dbf660b

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

Trigger CI for leanprover/lean4#4272

9c70cea

JovanGerb added 2 commits May 25, 2024 15:09

Revert "cache whenever the key isn't α-reduced"

c26ee24

This reverts commit 0d438bc.

use hasExprMVar

4bc1122

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

Trigger CI for leanprover/lean4#4272

3c3e92c

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

Trigger CI for leanprover/lean4#4272

1c39c47

JovanGerb added 2 commits May 26, 2024 00:43

comment

4719368

optimize loop detection

4455022

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

Trigger CI for leanprover/lean4#4272

ee1724a

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

Trigger CI for leanprover/lean4#4272

fcef64e

JovanGerb added 2 commits May 26, 2024 14:02

.

f25272d

check cached results for metavariable instantiations

02c25bb

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

Trigger CI for leanprover/lean4#4272

a158afb

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

Trigger CI for leanprover/lean4#4272

41e7240

revert to simpler loop detection

5f65a7e

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

Trigger CI for leanprover/lean4#4272

b76419e

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

Trigger CI for leanprover/lean4#4272

18eef3b

don't used classes with outParam in intermediate caching

2c5a49a

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

Trigger CI for leanprover/lean4#4272

b7648b8

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

Trigger CI for leanprover/lean4#4272

dd7393f

fix sign

c06f2e5

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

Trigger CI for leanprover/lean4#4272

56a88f9

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

Trigger CI for leanprover/lean4#4272

4c58a5c

JovanGerb added 4 commits May 29, 2024 02:08

don't telescope twice

3d79e7e

fix

671fca3

fix

4a2ea3e

fix

d84a544

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

Trigger CI for leanprover/lean4#4272

f1a5f00

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

Trigger CI for leanprover/lean4#4272

342e97b

undo

1fed626

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

Trigger CI for leanprover/lean4#4272

7ec8002

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

Trigger CI for leanprover/lean4#4272

c937fa9

don't forallTelescope explicitly

6632ffb

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

Trigger CI for leanprover/lean4#4272

9e21967

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

Trigger CI for leanprover/lean4#4272

e2f09e6

JovanGerb mentioned this pull request Jun 8, 2024

perf: deduplicate ← instantiateMVars (← inferType mvar) in TC search #4379

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

perf: cache intermediate type class results and non-results #4272

perf: cache intermediate type class results and non-results #4272

JovanGerb commented May 24, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented May 24, 2024 •

edited

Loading

perf: cache intermediate type class results and non-results #4272

Are you sure you want to change the base?

perf: cache intermediate type class results and non-results #4272

Conversation

JovanGerb commented May 24, 2024 • edited Loading

leanprover-community-mathlib4-bot commented May 24, 2024 • edited Loading

JovanGerb commented May 24, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented May 24, 2024 •

edited

Loading