diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean index 795fe93053..18de59d001 100644 --- a/src/Leanpkg.lean +++ b/src/Leanpkg.lean @@ -82,14 +82,21 @@ def execMake (makeArgs leanArgs : List String) (leanPath : String) : IO Unit := } execCmd spawnArgs +def getRootPart : IO Lean.Name := do + let entries ← FilePath.readDir "." + match entries.filter (FilePath.extension ·.fileName == "lean") with + | #[rootFile] => FilePath.withExtension rootFile.fileName "" |>.toString + | #[] => throw <| IO.userError s!"no '.lean' file found in {← IO.realPath "."}" + | _ => throw <| IO.userError s!"{← IO.realPath "."} must contain a unique '.lean' file as the package root" + def buildImports (imports : List String) (leanArgs : List String) : IO Unit := do unless ← leanpkgTomlFn.pathExists do return let manifest ← readManifest let cfg ← configure let imports := imports.map (·.toName) - -- TODO: shoddy check - let localImports := imports.filter fun i => i.getRoot.toString.toLower == manifest.name.toLower + let root ← getRootPart + let localImports := imports.filter (·.getRoot == root) if localImports != [] then let oleans := localImports.map fun i => Lean.modPathToFilePath ⟨"build"⟩ i |>.withExtension "olean" |>.toString execMake oleans leanArgs cfg.leanPath