8000 fix: make hasLocalInst ignore instance params of erased type by zwarich · Pull Request #8979 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

fix: make hasLocalInst ignore instance params of erased type #8979

New issue
8000

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

Sign up for GitHub

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

Jump to bottom
Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

fix: make hasLocalInst ignore instance params of erased type #8979

wants to merge 1 commit into from
+2 −2

Conversation

zwarich
Copy link
Contributor
@zwarich zwarich commented Jun 24, 2025

This PR makes hasLocalInst ignore instance params of erased type, which is useful for purely proof-carrying parameters like [NeZero n].

@zwarich zwarich requested a review from leodemoura as a code owner June 24, 2025 15:54
@zwarich zwarich added the changelog-compiler Compiler, runtime, and FFI label Jun 24, 2025
@zwarich
Copy link
Contributor Author
zwarich commented Jun 24, 2025

!bench

@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 Jun 24, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Jun 24, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ddbba944d42a1479ec9e4f350b9a270b008c01f0 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-24 16:21:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f1021e4537d1c97eb5e828f459bb396577bf2467 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-25 00:58:21)

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 95141b8.
There were no significant changes against commit ddbba94.

@zwarich zwarich marked this pull request as draft June 24, 2025 21:21
@zwarich
Copy link
Contributor Author
zwarich commented Jun 24, 2025

(converting to draft to test the followup to this)

@zwarich
Copy link
Contributor Author
zwarich commented Jun 24, 2025

!bench

@zwarich zwarich force-pushed the template-like-erased branch from 4d33101 to d9c3c81 Compare June 24, 2025 21:35
@leanprover-bot
8000 Copy link
Collaborator

Here are the benchmark results for commit 4d33101.
There were significant changes against commit ddbba94:

  Benchmark   Metric                  Change
  ===================================================
- qsort       task-clock               13.7% (25.4 σ)
- qsort       wall-clock               13.7% (25.1 σ)
- stdlib      blocked (unaccounted)     1.4% (26.9 σ)

@zwarich
Copy link
Contributor Author
zwarich commented Jun 24, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d9c3c81.
There were no significant changes against commit ddbba94.

@zwarich zwarich force-pushed the template-like-erased branch from d9c3c81 to 3e66957 Compare June 25, 2025 00:35
@zwarich zwarich marked this pull request as ready for review June 25, 2025 00:38
@zwarich
Copy link
Contributor Author
zwarich commented Jun 25, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 3e66957.
There were significant changes against commit f1021e4:

  Benchmark        Metric                  Change
  =========================================================
+ riscv-ast.lean   task-clock               -4.1% (-30.2 σ)
+ stdlib           blocked (unaccounted)    -1.6% (-30.0 σ)
+ stdlib           task-clock               -1.0% (-42.7 σ)

@zwarich zwarich marked this pull request as draft June 25, 2025 06:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees
No one assigned
Labels
changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@zwarich @leanprover-community-bot @leanprover-bot
0