Skip to content

Commit a35fea8

Browse files
committed
fix: recognise quoted bare names in lakefile.lean require blocks
`leanRequirePrefixes` only generated the unquoted pattern `require foo` for bare dependency names, so lakefiles using the valid quoted form `require "foo" from git ...` were rejected with "does not contain a require block named 'foo'". Add the quoted variant `require "foo"` as a second candidate prefix. Add a test fixture and three test cases covering readLeanGitUrl, readLeanPinnedRev, and rewriteLeanContents for quoted bare names.
1 parent 206943a commit a35fea8

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Hopscotch/LakefileProcessor.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -225,8 +225,8 @@ private def leanRequirePrefixes (depName : String) : Array String :=
225225
, "require \"" ++ scope ++ "\"/\"" ++ name ++ "\""
226226
]
227227
| _ =>
228-
-- Bare name: `require depName`.
229-
#["require " ++ depName]
228+
-- Bare name: `require depName` or `require "depName"` (quoted form is also valid Lake DSL).
229+
#["require " ++ depName, "require \"" ++ depName ++ "\""]
230230

231231
/--
232232
Scan `lines` and collect every `require` block whose dependency name equals `depName`.

0 commit comments

Comments
 (0)