fix(Shake): update for changes to header grammar (#25054)

fixes #24743 ... again



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: digama0

Shake/Main.lean

@@ -3,11 +3,6 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lake.Util.Error
-import Lean.Environment
-import Lean.Parser.Module
-import Lean.Util.FoldConsts
-import Lean.Util.Paths
 import Lake.CLI.Main
 
 /-! # `lake exe shake` command
@@ -221,24 +216,38 @@ def Edits.add (ed : Edits) (src : Name) (tgt : Nat) : Edits :=
 
 /-- Parse a source file to extract the location of the import lines, for edits and error messages.
 
-Returns `(path, inputCtx, headerStx, endPos)` where `headerStx` is the `Lean.Parser.Module.header`
+Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
 and `endPos` is the position of the end of the header.
 -/
-def parseHeader (srcSearchPath : SearchPath) (mod : Name) :
-    IO (System.FilePath × Parser.InputContext × TSyntax ``Parser.Module.header × String.Pos) := do
-  -- Parse the input file
-  let some path ← srcSearchPath.findModuleWithExt "lean" mod
-    | throw <| .userError "error: failed to find source file for {mod}"
-  let text ← IO.FS.readFile path
-  let inputCtx := Parser.mkInputContext text path.toString
+def parseHeaderFromString (text path : String) :
+    IO (System.FilePath × Parser.InputContext ×
+      TSyntaxArray ``Parser.Module.import × String.Pos) := do
+  let inputCtx := Parser.mkInputContext text path
   let (header, parserState, msgs) ← Parser.parseHeader inputCtx
   if !msgs.toList.isEmpty then -- skip this file if there are parse errors
     msgs.forM fun msg => msg.toString >>= IO.println
     throw <| .userError "parse errors in file"
   -- the insertion point for `add` is the first newline after the imports
   let insertion := header.raw.getTailPos?.getD parserState.pos
   let insertion := text.findAux (· == '\n') text.endPos insertion + ⟨1⟩
-  pure (path, inputCtx, header, insertion)
+  pure (path, inputCtx, .mk header.raw[2].getArgs, insertion)
+
+/-- Parse a source file to extract the location of the import lines, for edits and error messages.
+
+Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
+and `endPos` is the position of the end of the header.
+-/
+def parseHeader (srcSearchPath : SearchPath) (mod : Name) :
+    IO (System.FilePath × Parser.InputContext ×
+      TSyntaxArray ``Parser.Module.import × String.Pos) := do
+  -- Parse the input file
+  let some path ← srcSearchPath.findModuleWithExt "lean" mod
+    | throw <| .userError "error: failed to find source file for {mod}"
+  let text ← IO.FS.readFile path
+  parseHeaderFromString text path.toString
+
+/-- Gets the name `Foo` in `import Foo`. -/
+def importId (stx : TSyntax ``Parser.Module.import) : Name := stx.raw[3].getId
 
 /-- Analyze and report issues from module `i`. Arguments:
 
@@ -291,10 +300,10 @@ def visitModule (s : State) (srcSearchPath : SearchPath) (ignoreImps : Bitset)
     edits.remove s.modNames[i]! s.modNames[n]!
   if githubStyle then
     try
-      let (path, inputCtx, header, endHeader) ← parseHeader srcSearchPath s.modNames[i]!
-      for stx in header.raw[2].getArgs do
-        if toRemove.any fun i => s.modNames[i]! == stx[2].getId then
-          let pos := inputCtx.fileMap.toPosition stx.getPos?.get!
+      let (path, inputCtx, imports, endHeader) ← parseHeader srcSearchPath s.modNames[i]!
+      for stx in imports do
+        if toRemove.any fun i => s.modNames[i]! == importId stx then
+          let pos := inputCtx.fileMap.toPosition stx.raw.getPos?.get!
           println! "{path}:{pos.line}:{pos.column+1}: warning: unused import \
             (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)"
       if !toAdd.isEmpty then
@@ -595,7 +604,7 @@ def main (args : List String) : IO UInt32 := do
       out.qsort Name.lt
 
     -- Parse the input file
-    let (path, inputCtx, header, insertion) ←
+    let (path, inputCtx, imports, insertion) ←
       try parseHeader srcSearchPath mod
       catch e => println! e.toString; return count
     let text := inputCtx.input
@@ -604,12 +613,12 @@ def main (args : List String) : IO UInt32 := do
     let mut pos : String.Pos := 0
     let mut out : String := ""
     let mut seen : NameSet := {}
-    for stx in header.raw[2].getArgs do
-      let mod := stx[2].getId
+    for stx in imports do
+      let mod := importId stx
       if remove.contains mod || seen.contains mod then
-        out := out ++ text.extract pos stx.getPos?.get!
+        out := out ++ text.extract pos stx.raw.getPos?.get!
         -- We use the end position of the syntax, but include whitespace up to the first newline
-        pos := text.findAux (· == '\n') text.endPos stx.getTailPos?.get! + ⟨1⟩
+        pos := text.findAux (· == '\n') text.endPos stx.raw.getTailPos?.get! + ⟨1⟩
       seen := seen.insert mod
     out := out ++ text.extract pos insertion
     for mod in add do
@@ -628,3 +637,10 @@ def main (args : List String) : IO UInt32 := do
   else
     println! "No edits required."
   return 0
+
+-- self-test so that future grammar changes cause a build failure
+/-- info: #[`Lake.CLI.Main] -/
+#guard_msgs (whitespace := lax) in
+#eval show MetaM _ from do
+  let (_, _, imports, _) ← parseHeaderFromString (← getFileMap).source (← getFileName)
+  return imports.map importId