`--incr-save` on top of an `--incr-header-save` snapshot yields a snapshot that fails to load (`invalid 'import' command`) once the file has >= 3 commands
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 30/100
- Issue type
- Bug
- Clarity
- Clearly specified
- Activity status
- Active
- Domain
- compilers
Research direction
Start by reproducing the chain with the steps in the issue: save a header-only snapshot with --incr-header-save, then --incr-save on top of it, then --incr-load the result on a file with three or more commands. The bug lives in the incremental snapshot save and load path behind the --incr-save, --incr-load and --incr-header-save flags. Done means the chained snapshot loads with exit 0 and no messages, matching lean b.lean, and the direct and full-snapshot controls still pass.
Written by the indexing model from the issue text.
Description
Prerequisites
- Checked that the issue is not already filed (searched issues and PRs for
incr-save,incr-load,header snapshot). - Reduced to a minimal, self-contained test case (plain
import Lean, no Mathlib). - Tested against the latest nightly (
4.36.0-nightly-2026-10-13) and4.33.0-rc1. Same result on both.
Description
Loading a header-only snapshot (--incr-header-save) and then saving a new snapshot (--incr-save) from it can produce a snapshot that loads incorrectly. The save exits 0 and prints nothing. A later --incr-load of the new snapshot reports invalid 'import' command, it must be used in the beginning of the file on the file's first line, and the file is rejected even though it elaborates fine without the snapshot. A direct --incr-save of the same file, and chaining from a full snapshot, both load correctly.
Steps to Reproduce
echo 'import Lean' > h.lean
lean --incr-header-save=H.snap h.lean
gen() { echo 'import Lean'; for i in $(seq 1 $1); do echo "theorem K$i (a b : Nat) (h : a < b) : a + $i < b + $i := by omega"; done; }
gen 3 > a.lean; gen 4 > b.lean
lean --incr-load=H.snap --incr-save=C.snap a.lean # exit 0, no output
lean --incr-load=C.snap b.lean
# b.lean:1:0: error: invalid 'import' command, it must be used in the beginning of the file (exit 1)
# controls
lean --incr-save=D.snap a.lean; lean --incr-load=D.snap b.lean # direct save: exit 0, correct
lean b.lean # no snapshot: exit 0
Expected behavior: lean --incr-load=C.snap b.lean behaves like lean b.lean (exit 0, no messages).
Actual behavior: exit 1 with the invalid 'import' command error at 1:0.
Versions
Lean (version 4.36.0-nightly-2026-10-13, x86_64-unknown-linux-gnu, commit b7725c34da98e6e2f6323d7f382448ddf31477fb, Release) and Lean (version 4.33.0-rc1, x86_64-unknown-linux-gnu, commit 62eed1db4d67327ec8120be05f1a1b0847d74561, Release). Linux x86_64.
Additional Information
Threshold measured by varying the number k of commands in the file saved in the chain step (--incr-load=H --incr-save=C, then --incr-load=C on the file plus one command). The same table was obtained with import Lean and with import Mathlib (only the threshold differs):
| k commands | direct save, then load | chain from header snapshot, then load | chain from full snapshot, then load |
|---|---|---|---|
| 1, 2 | ok | ok | ok |
>= 3 (import Lean), >= 5 (import Mathlib) |
ok | exit 1, invalid 'import' command | ok |
Chaining from a full snapshot (--incr-load=D --incr-save=E) loaded correctly in every case I tried (depth up to 3). I did not look into the cause.
Impact
Tools that cache header snapshots and then incrementally save on top of them get a corrupted cache entry with no error at save time. Workaround on my side: never --incr-save while loading a header-only snapshot, and load-test every new snapshot before publishing it.
- Dominant language
- Lean
- Stars
- 9.6k
- Forks
- 1.1k
- Avg merge
- 1d 17m
- Merged PRs (30d)
- 296
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
bug
Difficulty 1/5 Under an hour Newbie friendliness 85/100
leanprover/lean4#15925 ·
Maintainers usually reply within 1 day
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken @treiher claimed this 6 days ago. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
area:codegen backend:cuda backend:hip bug direction:input
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
CrossGL/crosstl#3061 · 1 comment ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 85/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
-
build
Difficulty 2/5 1-3 hours Newbie friendliness 65/100
AOMediaCodec/SVT-AV1#2500 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
rescript-lang/rescript#9037 ·
Maintainers usually reply within 1 day