Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

perf: globally cache intermediate type class results #4150

Closed
wants to merge 3 commits into from

Conversation

JovanGerb
Copy link
Contributor

@JovanGerb JovanGerb commented May 13, 2024

I seem to have messed up the git stuff, so I made a new identical PR: #4152

See Zulip discussion here

This is a PR to determine whether this idea indeed results in faster type class search.

@nomeata
Copy link
Collaborator

nomeata commented May 13, 2024

If this PR is created just to get the CI test, but you don't want people to look at and comment on the idea and implementation yet, using a “draft PR” makes it even more clear.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 13, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f74980ccee82ca2abdae65dcbc5571d4640ed076 --onto 7db8e6482e1dc46fd1070b3bf549112f02a4c05e. (2024-05-13 15:17:27)

@JovanGerb JovanGerb marked this pull request as draft May 13, 2024 15:24
@JovanGerb JovanGerb closed this May 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants