max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: shake: avoid panic on header-only files without trailing newline (#12963)

Browse source 
This PR fixes a panic in `lake shake` when applied to a header-only file
without trailing newline
This commit is contained in:
Sebastian Ullrich 2026-03-18 16:44:39 +01:00 • committed by GitHub
parent 58ef418dda
commit b13325f95d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/lake/Lake/CLI/Shake.lean
View file

@ -368,7 +368,8 @@ def parseHeaderFromString (text path : String) :
throw <| .userError "parse errors in file" throw <| .userError "parse errors in file"
-- the insertion point for `add` is the first newline after the imports -- the insertion point for `add` is the first newline after the imports
let insertion := header.raw.getTailPos?.getD parserState.pos let insertion := header.raw.getTailPos?.getD parserState.pos
let insertion := inputCtx.fileMap.source.pos! insertion |>.find (· == '\n') |>.next! let insertion := inputCtx.fileMap.source.pos! insertion |>.find (· == '\n')
let insertion := insertion.next?.getD insertion
pure ⟨path, inputCtx, header, insertion⟩ pure ⟨path, inputCtx, header, insertion⟩
/-- Parse a source file to extract the location of the import lines, for edits and error messages. /-- Parse a source file to extract the location of the import lines, for edits and error messages.
@ -709,7 +710,8 @@ public def run (args : Args) (srcSearchPath : SearchPath := {}) : IO UInt32 := d
if remove.contains mod || seen.contains mod then if remove.contains mod || seen.contains mod then
out := out ++ text.extract pos (text.pos! stx.raw.getPos?.get!) out := out ++ text.extract pos (text.pos! stx.raw.getPos?.get!)
-- We use the end position of the syntax, but include whitespace up to the first newline -- We use the end position of the syntax, but include whitespace up to the first newline
pos := text.pos! stx.raw.getTailPos?.get! |>.find '\n' |>.next! pos := text.pos! stx.raw.getTailPos?.get! |>.find '\n'
pos := pos.next?.getD pos
seen := seen.insert mod seen := seen.insert mod
out := out ++ text.extract pos insertion out := out ++ text.extract pos insertion
for mod in add do for mod in add do