diff --git a/src/Leanpkg/Build.lean b/src/Leanpkg/Build.lean index 82eacf7502..8b396d7d6c 100644 --- a/src/Leanpkg/Build.lean +++ b/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! diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 765a02b07c..8ea856772d 100644 --- a/src/shell/CMakeLists.txt +++ b/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'") diff --git a/tests/leanpkg/cyclic/Cyclic.lean b/tests/leanpkg/cyclic/Cyclic.lean new file mode 100644 index 0000000000..5af4f224d9 --- /dev/null +++ b/tests/leanpkg/cyclic/Cyclic.lean @@ -0,0 +1 @@ +import Cyclic.A diff --git a/tests/leanpkg/cyclic/Cyclic/A.lean b/tests/leanpkg/cyclic/Cyclic/A.lean new file mode 100644 index 0000000000..31d5d96dcc --- /dev/null +++ b/tests/leanpkg/cyclic/Cyclic/A.lean @@ -0,0 +1 @@ +import Cyclic.A.B diff --git a/tests/leanpkg/cyclic/Cyclic/A/B.lean b/tests/leanpkg/cyclic/Cyclic/A/B.lean new file mode 100644 index 0000000000..41c84985d2 --- /dev/null +++ b/tests/leanpkg/cyclic/Cyclic/A/B.lean @@ -0,0 +1 @@ +import Cyclic diff --git a/tests/leanpkg/cyclic/leanpkg.toml b/tests/leanpkg/cyclic/leanpkg.toml new file mode 100644 index 0000000000..8f7f2d5db6 --- /dev/null +++ b/tests/leanpkg/cyclic/leanpkg.toml @@ -0,0 +1,4 @@ +[package] +name = "cyclic" +version = "0.1" +lean_version = "leanprover/lean4:master"