Skip to content

perf: optimize instantiateForall - #16321

Closed
Rob23oba wants to merge 1 commit into
leanprover:masterfrom
Rob23oba:instantiate-forall-faster
Closed

Rob23oba wants to merge 1 commit into
leanprover:masterfrom
Rob23oba:instantiate-forall-faster

Conversation

@Rob23oba

@Rob23oba Rob23oba commented Nov 6, 2026

Copy link
Copy Markdown
Contributor

This PR optimizes instantiateForall to only perform one instantiateRevRange if it doesn't need to reduce the expression.

@Rob23oba

Rob23oba commented Nov 6, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@Rob23oba

Rob23oba commented Nov 6, 2026

Copy link
Copy Markdown
Contributor Author

!radar

@leanprover-radar

leanprover-radar commented Nov 6, 2026 •

Copy link
Copy Markdown

Benchmark results for 08e37c0 against f5be489 are in. (These commits have already been benchmarked in a previous command.) There are significant results. @Rob23oba

  • 🟥 build//instructions: +3.2G (+0.03%)

Large changes (1🟥)

  • 🟥 vcgen/AdcChain/250/kernel//wall-clock: +7ms (+32.92%)

Medium changes (1🟥)

  • 🟥 build/module/Lean.Meta.Basic//instructions: +3.3G (+17.45%) (reduced significance based on absolute threshold)

Small changes (2✅, 1🟥)

  • ✅ compiled/rbmap_checkpoint2//maxrss: -272kiB (-0.09%)
  • and 2 hidden

1 similar comment
@leanprover-radar

leanprover-radar commented Nov 6, 2026 •

Copy link
Copy Markdown

Benchmark results for 08e37c0 against f5be489 are in. (These commits have already been benchmarked in a previous command.) There are significant results. @Rob23oba

  • 🟥 build//instructions: +3.2G (+0.03%)

Large changes (1🟥)

  • 🟥 vcgen/AdcChain/250/kernel//wall-clock: +7ms (+32.92%)

Medium changes (1🟥)

  • 🟥 build/module/Lean.Meta.Basic//instructions: +3.3G (+17.45%) (reduced significance based on absolute threshold)

Small changes (2✅, 1🟥)

  • ✅ compiled/rbmap_checkpoint2//maxrss: -272kiB (-0.09%)
  • and 2 hidden

@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 Nov 6, 2026
@Rob23oba Rob23oba closed this Nov 6, 2026
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.

2 participants