perf: cache intermediate type class results and non-results by JovanGerb · Pull Request #4272 · leanprover/lean4

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.

ghost · 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 24, 2024

Update lean-toolchain for testing leanprover/lean4#4272

07e9358

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

Update lean-toolchain for testing leanprover/lean4#4272

2b46c19

ghost 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 25, 2024

Trigger CI for leanprover/lean4#4272

afcb8a8

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 25, 2024

Trigger CI for leanprover/lean4#4272

d394f7e

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 25, 2024

Trigger CI for leanprover/lean4#4272

0b79050

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 25, 2024

Trigger CI for leanprover/lean4#4272

73ac42f

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 25, 2024

Trigger CI for leanprover/lean4#4272

dbf660b

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 25, 2024

Trigger CI for leanprover/lean4#4272

3c3e92c

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

Trigger CI for leanprover/lean4#4272

1c39c47

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 26, 2024

Trigger CI for leanprover/lean4#4272

a158afb

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 27, 2024

Trigger CI for leanprover/lean4#4272

b76419e

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 28, 2024

Trigger CI for leanprover/lean4#4272

b7648b8

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

Trigger CI for leanprover/lean4#4272

dd7393f

fix sign

c06f2e5

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 28, 2024

Trigger CI for leanprover/lean4#4272

56a88f9

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 29, 2024

Trigger CI for leanprover/lean4#4272

f1a5f00

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

Trigger CI for leanprover/lean4#4272

342e97b

undo

1fed626

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 29, 2024

Trigger CI for leanprover/lean4#4272

7ec8002

ghost pushed 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

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 31, 2024

Trigger CI for leanprover/lean4#4272

9e21967

ghost pushed 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

leodemoura force-pushed the master branch from 32d60c5 to 696f70b Compare July 20, 2024 02:58

nomeata removed the full-ci label Jul 23, 2024

JovanGerb closed this Jul 9, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

perf: cache intermediate type class results and non-results#4272
JovanGerb wants to merge 31 commits into
leanprover:masterfrom
JovanGerb:instanceCaching

JovanGerb commented May 24, 2024 •

edited

Loading

Uh oh!

ghost commented May 24, 2024 •

edited by ghost

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

JovanGerb commented May 24, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ghost commented May 24, 2024 • edited by ghost Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

JovanGerb commented May 24, 2024 •

edited

Loading

ghost commented May 24, 2024 •

edited by ghost

Loading