Skip to content

feat: mvcgen', an experimental SymM-based implementation mvcgen#13644

Merged
sgraf812 merged 10 commits into
masterfrom
sg/upstream-mvcgen'
May 7, 2026
Merged

feat: mvcgen', an experimental SymM-based implementation mvcgen#13644
sgraf812 merged 10 commits into
masterfrom
sg/upstream-mvcgen'

Conversation

@sgraf812
Copy link
Copy Markdown
Contributor

@sgraf812 sgraf812 commented May 5, 2026 •
edited
Loading

This PR adds an experimental tactic mvcgen' that will soon replace mvcgen. It has been reimplemented from the ground up using the new SymM-based framework for efficient symbolic evaluation and can outperform mvcgen by a factor of >100x for some synthetic benchmarks. mvcgen' aspires to be feature-complete with mvcgen. Known exceptions currently are join point sharing, introduction of local specs and smaller bugs.

The implementation of mvgen' used to live in the benchmark suite for rapid prototyping; this commit merely moves it into the Lean toolchain. Doing so results in an build time instruction count increase in seemingly unrelated tests such as elab/delayed_assign//instructions; the reason is that the builtin elaborator attribute now pulls in substantially more import code on startup.

@sgraf812 sgraf812 added changelog-language Language features and metaprograms changelog-tactics User facing tactics and removed changelog-language Language features and metaprograms labels May 5, 2026
@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 5, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented May 5, 2026 •
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 42eb0385a5898e8510c7098b473d0b8d98aee285 --onto dae325700c89e23c453b1d6d5ed5432d87880062. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-05 14:54:58)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 42eb0385a5898e8510c7098b473d0b8d98aee285 --onto 8ebd294673e9e0397c5ccf2ab9a65b0f3e937918. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-06 10:45:34)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 42eb0385a5898e8510c7098b473d0b8d98aee285 --onto ea6e76707835317858b7dd36c95322679c50aaac. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-06 17:40:40)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5d5642107d0433519265f155ddbfbfb98007a80b --onto ea6e76707835317858b7dd36c95322679c50aaac. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-07 08:00:33)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented May 5, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 42eb0385a5898e8510c7098b473d0b8d98aee285 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-05-05 14:55:01)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5d5642107d0433519265f155ddbfbfb98007a80b --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-05-07 08:00:35)

@sgraf812
Copy link
Copy Markdown
Contributor Author

sgraf812 commented May 5, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented May 5, 2026 •
edited
Loading

Benchmark results for 8d2db9d against 42eb038 are in. There are significant results. @sgraf812

  • 🟥 build//instructions: +69.3G (+0.57%)

Large changes (5🟥)

  • 🟥 build/profile/interpretation//wall-clock: +995ms (+19.90%)
  • 🟥 size/all/.c//lines: +77.2k (+0.69%)
  • 🟥 size/all/.ir//bytes: +3MiB (+0.75%)
  • 🟥 size/compile/.out//bytes: +14MiB (+0.80%)
  • 🟥 size/libleanshared.so//bytes: +1MiB (+0.74%)

Medium changes (4🟥)

  • 🟥 build/stat/imported bytes//bytes: +2GiB (+1.12%)
  • 🟥 build/stat/imported modules//amount: +13.9k (+1.27%)
  • 🟥 size/all/.olean.private//bytes: +7MiB (+0.55%)
  • 🟥 size/install//bytes: +14MiB (+0.53%)

Small changes (17🟥)

  • 🟥 build//instructions: +69.3G (+0.57%)
  • 🟥 build/module/Init.Tactics//instructions: +58.3M (+0.46%)
  • 🟥 build/module/Lean.Elab.Tactic.Do//instructions: +33.8M (+4.81%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Elab.Tactic//instructions: +9.2M (+0.87%)
  • 🟥 build/module/Lean.Elab//instructions: +11.7M (+1.04%)
  • 🟥 build/module/Std.Tactic.Do.Syntax//instructions: +79.0M (+1.20%)
  • 🟥 build/profile/C code generation//wall-clock: +805ms (+6.81%)
  • 🟥 build/stat/imported consts//amount: +687.0k (+0.93%)
  • 🟥 compiled/watchdogRss//instructions: +90.2M (+0.33%)
  • 🟥 elab/big_deceq//instructions: +17.1M (+0.37%)
  • 🟥 elab/charactersIn//instructions: +98.9M (+0.27%)
  • 🟥 elab/delayed_assign//instructions: +35.0M (+0.95%)
  • 🟥 elab/delayed_sharing//instructions: +15.2M (+0.51%)
  • 🟥 elab/workspaceSymbols//instructions: +84.1M (+0.40%)
  • 🟥 size/all/.ilean//bytes: +262kiB (+0.32%)
  • 🟥 size/all/.lean//lines: +2.0k (+0.30%)
  • 🟥 size/all/.olean.server//bytes: +70kiB (+0.23%)

and 1 hidden

Sebastian Graf and others added 4 commits May 5, 2026 17:38
chore: add BackwardRule.applyChecked debug wrapper for mvcgen'
d795893 
Adds a `+debug` config option to `mvcgen'` and a `BackwardRule.applyChecked`
wrapper around `BackwardRule.apply`. On apply failure with `+debug` set, the
wrapper retries on the `unfoldReducible`-normalized goal type; if the retry
succeeds, an earlier step missed a normalization and we throw a hard error
naming the rule (auto-derived from `rule.expr.getAppFn` when available) and
showing the original vs. normalized types.

All `BackwardRule.apply` call sites in `Entails`, `Solve`, and `Util`
(`repeatAndRfl`) now go through `applyChecked` via dot notation. Default
behaviour (without `+debug`) is unchanged.
@sgraf812
fix: unfold reducible abbreviations in inline-elaborated invariant va…
26b0f59 
…lues

User-provided invariant values (`mvcgen' invariants · …`) are elaborated against
goal types containing reducible abbreviations like `PostShape.args ps`, so the
resulting term carries `(PostShape.args PostShape.pure)` baked into its body
instead of `[]`. Those stuck abbreviations propagate via metavariable
substitution and later block rule applications such as `SPred.pure_elim'` in
`solveSPredEntails`.

After `tryInlineInvariant` confirms the user tactic assigned the invariant
metavariable, reduce its assignment with `unfoldReducible`.

Fixes the failure on `tests/elab/10564.lean` (and incidentally `9581.lean`
and `grind_12246.lean`) when the proofs are migrated to `mvcgen'`. The
`+debug` wrapper added in the previous commit was used to pinpoint the
missing reduction.
@sgraf812
fix: mvcgen' with grind should fail when grind fails
dc95b75
Merge remote-tracking branch 'origin/master' into sg/upstream-mvcgen'
e626935
@sgraf812 sgraf812 force-pushed the sg/upstream-mvcgen' branch from 8176e6b to e626935 Compare May 7, 2026 07:13
@sgraf812
Copy link
Copy Markdown
Contributor Author

sgraf812 commented May 7, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented May 7, 2026 •
edited
Loading

Benchmark results for e626935 against 5d56421 are in. There are significant results. @sgraf812

  • 🟥 build//instructions: +66.3G (+0.58%)

Large changes (4🟥)

  • 🟥 size/all/.c//lines: +80.2k (+0.71%)
  • 🟥 size/all/.ir//bytes: +3MiB (+0.78%)
  • 🟥 size/compile/.out//bytes: +16MiB (+0.80%)
  • 🟥 size/libleanshared.so//bytes: +1MiB (+0.78%)

Medium changes (4🟥)

  • 🟥 build/stat/imported bytes//bytes: +2GiB (+1.12%)
  • 🟥 build/stat/imported modules//amount: +13.9k (+1.27%)
  • 🟥 size/all/.olean.private//bytes: +7MiB (+0.58%)
  • 🟥 size/install//bytes: +14MiB (+0.49%)

Small changes (18🟥)

  • 🟥 build//instructions: +66.3G (+0.58%)
  • 🟥 build/module/Init.Tactics//instructions: +45.3M (+0.38%)
  • 🟥 build/module/Lean.Elab.Tactic.Do//instructions: +32.7M (+4.85%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Elab.Tactic//instructions: +8.3M (+0.81%)
  • 🟥 build/module/Lean.Elab//instructions: +10.6M (+0.97%)
  • 🟥 build/module/Std.Tactic.Do.Syntax//instructions: +67.9M (+1.11%)
  • 🟥 build/stat/imported consts//amount: +687.2k (+0.93%)
  • 🟥 compiled/watchdogRss//instructions: +91.8M (+0.36%)
  • 🟥 elab/big_deceq//instructions: +15.9M (+0.36%)
  • 🟥 elab/big_match//instructions: +18.6M (+0.17%)
  • 🟥 elab/charactersIn//instructions: +103.1M (+0.28%)
  • 🟥 elab/delayed_assign//instructions: +17.8M (+0.49%)
  • 🟥 elab/delayed_sharing//instructions: +16.7M (+0.57%)
  • 🟥 elab/workspaceSymbols//instructions: +95.3M (+0.47%)
  • 🟥 misc/import Lean//instructions: +7.9M (+0.53%)
  • 🟥 size/all/.ilean//bytes: +271kiB (+0.33%)
  • 🟥 size/all/.lean//lines: +2.1k (+0.31%)
  • 🟥 size/all/.olean.server//bytes: +72kiB (+0.24%)

and 1 hidden

@sgraf812 sgraf812 marked this pull request as ready for review May 7, 2026 12:52
@sgraf812 sgraf812 requested a review from kim-em as a code owner May 7, 2026 12:52
@sgraf812 sgraf812 enabled auto-merge May 7, 2026 12:52
@sgraf812 sgraf812 added this pull request to the merge queue May 7, 2026
Merged via the queue into master with commit 422920f May 7, 2026
24 checks passed
@sgraf812 sgraf812 deleted the sg/upstream-mvcgen' branch May 7, 2026 13:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

changelog-tactics User facing tactics 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

@sgraf812 @leanprover-bot @leanprover-radar