Repository navigation
Exponential time growth when repeating pure () #13858
Description
Prerequisites
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
A do block that only consists of pure ()s take a time exponential in the amount pure ()s. This is due to mkBindUnlessPure running the continuation twice, even if it is non-duplicable.
Context
Observing a non-duplicable continuation get run twice.
Steps to Reproduce
set_option backward.do.legacy false
def test : IO Unit := do
pure () -- 1
pure () -- 2
pure () -- 3
pure () -- 4
pure () -- 5
pure () -- 6
pure () -- 7
pure () -- 8
pure () -- 9
pure () -- 10
pure () -- 11
pure () -- 12
pure () -- 13
pure () -- 14Expected behavior:
The time it takes to elaborate test is roughly twice as much as if there were 7 pure ()s (i.e. negligible).
Actual behavior:
test takes multiple seconds to elaborate, roughly twice as much as if there were 13 pure ()s.
Versions
Lean 4.31.0, commit 2cd9863
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
Activity
Kha commentedon Jun 9, 2026
Practical context?
Rob23oba commentedon Jun 9, 2026
Fair, nobody would repeat
pure ()directly. How I discovered this is that I had a case where I ran the do elaborator with a nonduplicable continuation and relied on it running just once. To be concrete:What I was working on was a "command level do elaborator", i.e. allowing
on a command level. As an implementation, I made a continuation that records the local context and emits code to store the values of new local declarations in an environment extension. When the continuation gets run multiple times, we have a problem: what local context should we have in the next
docommand? So I just disallowed running the continuation twice using anIO.Refand was confused when the most trivial example,do pure ()failed with "continuation was run twice".The fix should be pretty simple though, basically a one-liner. I'll post a PR soon.
dtumad commentedon Sep 21, 2026
@Kha Found this issue by chance via Claude but this did come up practically for me working with
sail-riscv-leanwhich has this declaration that takes an insane amount of time to compile (10+ minutes at least). Also cc @ineol @tobiasgrosser I'm not sure the best contact on theopencomplside but this seems to be one of the big compile bottlenecks when importing the lean model of RISCVcasavaca commentedon Oct 13, 2026
@sgraf812 I think this is one for you, could you take a look?
sgraf812 commentedon Oct 14, 2026
Thanks, @Rob23oba! I took your PR #13985 almost verbatim in #15682, where I also added a commit that removes the stale comment.
fix: elaborate the do continuation only once when contracting `pure (…