commit: 272f0f5db390b3c720fc47ffed94f578018e8337

[log]
author: Kim Morrison <kim@tqft.net>

Tue Dec 02 18:19:45 2025 +1100
committer: Kim Morrison <kim@tqft.net>

Tue Dec 02 18:35:46 2025 +1100
tree: a1df36e4c75d89e4526b560ac5b9e4518b02e4e1
parent: 1d3fda41306f7d3191fff93567313673984fed30 [diff]

feat: add chunked variants of `parIterWithCancel`

Add `parIterWithCancelChunked` functions for CoreM, MetaM, TermElabM, and TacticM that support chunking jobs into groups to reduce task creation overhead.

The original `parIterWithCancel` functions remain unchanged for backward compatibility. The new chunked variants accept `maxTasks` and `minChunkSize` parameters to control parallelism.

This enables PRs that use `parIterWithCancel` (like parallel library search and rewrites) to benefit from chunking by switching to the new `parIterWithCancelChunked` function with `maxTasks := 128`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

src/Lean/Elab/Parallel.lean[diff]

1 file changed

tree: a1df36e4c75d89e4526b560ac5b9e4518b02e4e1

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.