fix: leanpkg: actually detect import cycles

src/Leanpkg/Build.lean

@@ -40,8 +40,8 @@ partial def buildModule (mod : Name) : BuildM Result := do
   let ctx ← read
   if ctx.parents.contains mod then
     -- cyclic import
-    let cycle := ctx.parents.dropWhile (· != mod) ++ [mod]
-    let cycle := cycle.reverse.map (s!"  {·}")
+    let cycle := mod :: (ctx.parents.partition (· != mod)).1 ++ [mod]
+    let cycle := cycle.map (s!"  {·}")
     throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
 
   if let some r := (← get).modTasks.find? mod then
@@ -54,7 +54,9 @@ partial def buildModule (mod : Name) : BuildM Result := do
   -- recursively build dependencies and calculate transitive `maxMTime`
   let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
   let localImports := imports.filter (·.module.getRoot == ctx.pkg)
-  let deps ← localImports.mapM (buildModule ·.module)
+  let deps ← localImports.mapM fun i =>
+    withReader (fun ctx => { ctx with parents := mod :: ctx.parents }) <|
+      buildModule i.module
   let depMTimes ← deps.mapM (·.maxMTime)
   let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
 

src/shell/CMakeLists.txt

@@ -148,3 +148,10 @@ add_test(NAME leanpkgtest
            (cd ../a; leanpkg build lib)
            leanpkg build bin LINK_OPTS=../a/build/lib/libA.a
            ./build/bin/B")
+
+add_test(NAME leanpkgtest_cyclic
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/cyclic"
+         COMMAND bash -c "
+           set -eu
+           export PATH=${LEAN_BIN}:$PATH
+           leanpkg build 2>&1 | grep 'import cycle'")

tests/leanpkg/cyclic/Cyclic.lean

@@ -0,0 +1 @@
+import Cyclic.A

tests/leanpkg/cyclic/Cyclic/A.lean

@@ -0,0 +1 @@
+import Cyclic.A.B

tests/leanpkg/cyclic/Cyclic/A/B.lean

@@ -0,0 +1 @@
+import Cyclic

tests/leanpkg/cyclic/leanpkg.toml

@@ -0,0 +1,4 @@
+[package]
+name = "cyclic"
+version = "0.1"
+lean_version = "leanprover/lean4:master"