Fix bug in lakefile rewriting, improve test

The lakefile rewriting logic was assuming the relevant [[require]] block was followed by another [[require]] in the TOML (or EOF). This is wrong: any other block (like [[lean_lib]]) should mark the end of it.

Also reorganize and improve the tests around it.

Author: marcelolynch

Hopscotch/LakefileProcessor.lean

@@ -13,6 +13,10 @@ private def preferredNewline (contents : String) : String :=
 private def isRequireHeader (line : String) : Bool :=
   line.trimAscii.copy == "[[require]]"
 
+/-- Detect any TOML section header (`[table]` or `[[array-of-tables]]`) after trimming indentation. -/
+private def isTomlSectionHeader (line : String) : Bool :=
+  line.trimAscii.startsWith "["
+
 /-- Read `name = "..."` or `rev = "..."` values from a trimmed TOML assignment line.
     Splits on `"` to extract the value; does not handle escaped quotes inside values. -/
 private def quotedAssignmentValue? (key : String) (line : String) : Option String :=
@@ -62,14 +66,17 @@ private def findNamedRequireBlocks (lines : Array String) (dependencyName : Stri
       let mut blockEnd := lines.size
       let mut j := blockStart
       while j < lines.size do
-        if isRequireHeader lines[j]! then
+        if isTomlSectionHeader lines[j]! then
           blockEnd := j
           break
         j := j + 1
       -- Record this block if its `name` field matches.
       let hasName := (lines.extract blockStart blockEnd).any
         fun line => quotedAssignmentValue? "name" line == some dependencyName
       if hasName then
+        -- Decrement blockEnd while it's whitespace or newline
+        while blockEnd > blockStart && lines[blockEnd - 1]!.isEmpty do
+          blockEnd := blockEnd - 1
         blocks := blocks.push (blockStart, blockEnd)
       i := blockEnd
     else

HopscotchTest/Main.lean

@@ -6,6 +6,7 @@ import HopscotchTestLib.LakefileLeanReadTests
 import HopscotchTestLib.ParseTests
 import HopscotchTestLib.ToolchainIOTests
 import HopscotchTestLib.UtilTests
+import HopscotchTestLib.LakefileRewriting
 
 open HopscotchTestLib
 
@@ -37,6 +38,7 @@ def testSuitesToRun : IO (Array (String × TestSuite)) := do
     ("ParseTests",            ParseTests.suite),
     ("IOTests",               IOTests.suite),
     ("LakefileReadTests",     LakefileReadTests.suite),
+    ("LakefileRewriting",     LakefileRewriting.suite),
     ("LakefileLeanReadTests", LakefileLeanReadTests.suite),
     ("ToolchainIOTests",      ToolchainIOTests.suite),
     ("UtilTests",             UtilTests.suite)

HopscotchTestLib/BehaviorTests.lean

@@ -51,124 +51,6 @@ private def «commit list normalization» : IO Unit := do
     catch _ =>
       pure ()
 
-/-- Scenario: the lakefile rewrite updates the first matching dependency rev in place. -/
-private def «lakefile dependency rev rewriting» : IO Unit := do
-  -- Prepare: a lakefile with two dependency blocks and one target rev to rewrite.
-  let base := makeMultiline [
-    "name = \"demo\"",
-    "",
-    "[[require]]",
-    "name = \"mathlib\"",
-    "git = \"https://github.com/leanprover-community/mathlib4.git\"",
-    "rev = \"upstream\" # keep this comment",
-    "",
-    "[[require]]",
-    "name = \"batteries\"",
-    "git = \"https://github.com/leanprover-community/batteries.git\"",
-    "rev = \"old\"",
-    ""
-  ]
-
-  -- Act: rewrite the target dependency rev in the prepared lakefile.
-  let rewritten ← IO.ofExcept <| LakefileProcessor.rewriteContents base "batteries" "abc123"
-  -- Assert: the rewritten lakefile changes only the requested dependency rev.
-  assertTrue (rewritten.contains "rev = \"abc123\"")
-    "rewrite should update the requested dependency rev"
-  assertTrue (rewritten.contains "rev = \"upstream\" # keep this comment")
-    "rewrite should leave unrelated dependency rev lines untouched"
-  assertEq 1 ((rewritten.splitOn "rev = \"abc123\"" |>.length) - 1)
-    "rewrite should touch only one rev line"
-  -- Prepare: a lakefile that omits the requested dependency block.
-  let missing := makeMultiline [
-    "name = \"demo\"",
-    "",
-    "[[require]]",
-    "name = \"mathlib\"",
-    "rev = \"main\"",
-    ""
-  ]
-
-  -- Act: attempt the rewrite
-  -- Asssert the missing dependency is rejected.
-  match LakefileProcessor.rewriteContents missing "batteries" "oops" with
-  | .ok _ => fail "missing dependency should be rejected"
-  | .error _ => pure ()
-
-  -- Prepare: a lakefile with duplicate dependency blocks for the requested name.
-  let duplicate := makeMultiline [
-    "name = \"demo\"",
-    "",
-    "[[require]]",
-    "name = \"batteries\"",
-    "rev = \"old1\"",
-    "",
-    "[[require]]",
-    "name = \"batteries\"",
-    "rev = \"old2\"",
-    ""
-  ]
-
-  -- Act: attempt the rewrite
-  -- Assert: duplicate dependency blocks are rejected.
-  match LakefileProcessor.rewriteContents duplicate "batteries" "oops" with
-  | .ok _ => fail "multiple matching dependency blocks should be rejected"
-  | .error _ => pure ()
-  -- Prepare: a matching dependency block without a rev line.
-  let missingRev := makeMultiline [
-    "name = \"demo\"",
-    "",
-    "[[require]]",
-    "name = \"batteries\"",
-    "git = \"https://github.com/leanprover-community/batteries.git\"",
-    ""
-  ]
-
-  -- Act: rewrite a dependency block that has no existing rev entry.
-  let insertedRev ← IO.ofExcept <| LakefileProcessor.rewriteContents missingRev "batteries" "inserted"
-  -- Assert: the rev is inserted into the block rather than causing an error.
-  assertTrue (insertedRev.contains "rev = \"inserted\"")
-    "rewrite should insert a rev entry when none exists"
-  -- Prepare: a matching dependency block without a rev that is followed by another block.
-  let missingRevMulti := makeMultiline [
-    "name = \"demo\"",
-    "",
-    "[[require]]",
-    "name = \"batteries\"",
-    "git = \"https://github.com/leanprover-community/batteries.git\"",
-    "",
-    "[[require]]",
-    "name = \"mathlib\"",
-    "rev = \"keepme\"",
-    ""
-  ]
-
-  -- Act: insert a rev only into the target block when followed by another block.
-  let insertedRevMulti ← IO.ofExcept <| LakefileProcessor.rewriteContents missingRevMulti "batteries" "inserted2"
-  -- Assert: only the target block receives the inserted rev; the other block is untouched.
-  assertTrue (insertedRevMulti.contains "rev = \"inserted2\"")
-    "rewrite should insert a rev entry before the next [[require]] block"
-  assertTrue (insertedRevMulti.contains "rev = \"keepme\"")
-    "rewrite should leave other dependency revs untouched when inserting"
-  -- Prepare: a CRLF-formatted lakefile with an inline rev comment.
-  let crlf := "\r\n"
-  let baseCrlf := String.intercalate crlf [
-    "name = \"demo\"",
-    "",
-    "[[require]]",
-    "name = \"batteries\"",
-    "git = \"https://github.com/leanprover-community/batteries.git\"",
-    "rev = \"old\" # trailing comment",
-    ""
-  ]
-
-  -- Act: rewrite the target dependency rev in the CRLF-formatted lakefile.
-  let rewrittenCrlf ← IO.ofExcept <| LakefileProcessor.rewriteContents baseCrlf "batteries" "newcrlf"
-  -- Assert: the CRLF rewrite preserves the inline suffix and line endings.
-  assertTrue (rewrittenCrlf.contains s!"rev = \"newcrlf\" # trailing comment")
-    "rewrite should preserve inline suffixes on the updated rev line"
-  assertTrue (rewrittenCrlf.contains crlf)
-    "rewrite should preserve CRLF line endings"
-
 /-- Scenario: console color helpers only add ANSI escapes when enabled. -/
 private def «console color helper behavior» : IO Unit := do
   -- Act: evaluate the color helper cases
@@ -437,7 +319,6 @@ private def «bisect 2-element list is immediately resolved» : IO Unit := do
 
 def suite : TestSuite := #[
   test_case «commit list normalization»,
-  test_case «lakefile dependency rev rewriting»,
   test_case «console color helper behavior»,
   test_case «summary display formatting»,
   test_case «summary git check formatting»,