Windows: copy-on-write .olean mapping (FILE_MAP_COPY) charges the full size of all imported module files to commit (regression since v4.31.0-rc1)

Open
  • Is something wrong?
#15,644 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
45/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Tech stack
cpp
Domain
operating-systems, performance

Research direction

Start with src/library/module.cpp around lean_compacted_region_read and compare its Windows mapping with the read-only mapping used before v4.31.0-rc1; read the region_reader::read() path in src/runtime/compact.cpp to understand when the mapped data needs fixups. Reproduce on Windows with the provided ImportLean.lean case and compare private bytes with working set; done means imports no longer incur commit charge for untouched file data.

Written by the indexing model from the issue text.

Description

Prerequisites
Description

On Windows, since v4.31.0-rc1 every lean process is charged commit (private bytes) for the full on-disk size of all imported .olean* files, even though almost none of these pages are ever touched.

lean_compacted_region_read maps the module files as a copy-on-write view:

https://github.com/leanprover/lean4/blob/v4.34.0-rc2/src/library/module.cpp#L507-L520

HANDLE h_map = CreateFileMapping(h_file, NULL, PAGE_WRITECOPY, 0, 0, NULL);
...
buffer = static_cast<char *>(MapViewOfFileEx(h_map, FILE_MAP_COPY, 0, 0, 0, base_addr));

Per the MapViewOfFile documentation: "When copy-on-write access is specified, the system and process commit charge taken is for the entire view because the calling process can potentially write to every page in the view." A read-only file-backed view is not charged.

This comes from #13185 (first released in v4.31.0-rc1); before that the mapping was read-only (PAGE_READONLY + FILE_MAP_READ). In the common case nothing is written to the view (the region lands at its saved base address and region_reader::read() only reads the root pointer, compact.cpp#L643-L656), so the working set stays small while the commit charge is large. Since module-system modules also load .olean.server / .olean.private (and .ir), the charge is roughly the size of all of those files.

Context

On a 12-thread / 32 GB machine, lake build of a project depending on Mathlib starts 12 lean.exe processes; each one is charged ~7.6 GB of private bytes right after importing (identical for all processes, independent of the file content), while all 12 together had a working set of only ~2 GB at that point. Mathlib + deps on disk: .olean 1.8 GB, .olean.private 3.5 GB, .olean.server 0.1 GB, .ir 0.3 GB. Total system commit exceeded 100 GB. With a system-managed pagefile (commit limit 63.8 GB) the commit limit was exhausted within ~2 minutes of starting the build: system services failed to start with "not enough memory resources", Windows tried to grow the pagefile, and the machine became unresponsive (Resource-Exhaustion-Detector, Event 2004, listed each lean.exe at ~9.6 GB). Raising the pagefile to 200 GB avoids this, and the pagefile is never actually written (Pages Output/sec = 0, pagefile usage 0 %), confirming that the charge is purely accounting for untouched pages.

Steps to Reproduce
  1. On Windows x64, create ImportLean.lean: 
    import Lean

#eval IO.sleep 8000
  2. Run lean ImportLean.lean with different toolchains and record the peak PrivateMemorySize64 (commit / "Commit size" in Task Manager) and WorkingSet64 of the process, e.g. in PowerShell: 
    $p = Start-Process lean.exe -ArgumentList 'ImportLean.lean' -PassThru -WindowStyle Hidden
$max = 0; $ws = 0
while (-not $p.HasExited) { $p.Refresh(); if ($p.PrivateMemorySize64 -gt $max) { $max = $p.PrivateMemorySize64; $ws = $p.WorkingSet64 }; Start-Sleep -Milliseconds 300 }
"peak private {0:N2} GB, working set {1:N2} GB" -f ($max/1GB), ($ws/1GB)

Measured results (same machine, same file):

Toolchain Peak private bytes Working set at that moment
v4.30.0 0.18 GB 0.75 GB
v4.31.0-rc1 2.02 GB 0.73 GB
v4.34.0-rc2 2.06 GB 0.81 GB
4.36.0-nightly-2026-10-12 2.09 GB 0.81 GB

Expected behavior: Importing modules does not charge commit for file data that is only read, as in v4.30.0 (private bytes well below the working set).

Actual behavior: Since v4.31.0-rc1, private bytes are ~11× higher for import Lean (and ~5.6 GB per process for Mathlib), i.e. the full size of the copy-on-write views, although the working set is unchanged.

Versions
  • Lean (version 4.34.0-rc2, x86_64-w64-windows-gnu, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, Release); also reproduced on v4.31.0-rc1 and 4.36.0-nightly-2026-10-12 (commit db7f10e90a71899cfd531a040360b1365f5fd92f); not reproduced on v4.30.0.
  • Windows 11 Enterprise 10.0.26200, x64, 32 GB RAM.
Additional Information

Possible directions (not verified):

  • Map with FILE_MAP_READ first and switch to a copy-on-write mapping (or the malloc + read fallback) only when a fixup is actually needed (region or one of its dependencies not at its base address, pointer relocations, etc.).
  • Avoid loading .olean.private / .olean.server when they are not needed, since they dominate the size.

Related, but not addressing the Windows commit charge: #14563, #14991, #14032.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Dominant language
Lean
Stars
9.8k
Forks
1.1k
Avg merge
14h 41m
Merged PRs (30d)
338

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More Operating Systems issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.