45 lines
1.6 KiB
Text
45 lines
1.6 KiB
Text
/-
|
|
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
|
|
-/
|
|
import Leanpkg2.BuildCore
|
|
import Leanpkg2.Resolve
|
|
|
|
open System
|
|
|
|
namespace Leanpkg2
|
|
|
|
def getRootPart (pkg : FilePath := ".") : IO Lean.Name := do
|
|
let entries ← pkg.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"
|
|
|
|
structure Configuration :=
|
|
leanPath : String
|
|
leanSrcPath : String
|
|
moreDeps : List FilePath
|
|
|
|
def configure (manifest : Manifest) : IO Configuration := do
|
|
IO.eprintln $
|
|
"configuring " ++ manifest.name ++ " " ++ manifest.version
|
|
let paths ← solveDeps manifest
|
|
let mut moreDeps := []
|
|
for (pkgpath, srcpath) in paths do
|
|
unless pkgpath == "." do
|
|
-- build recursively
|
|
-- TODO: share build of common dependencies
|
|
execCmd {
|
|
cmd := (← IO.appPath).toString
|
|
cwd := pkgpath
|
|
args := #["build"]
|
|
}
|
|
let pkgRoot := srcpath / Build.buildPath / (← getRootPart srcpath).toString
|
|
moreDeps := pkgRoot.withExtension "olean" :: moreDeps
|
|
return {
|
|
leanPath := SearchPath.toString <| paths.map (·.2 / Build.buildPath)
|
|
leanSrcPath := SearchPath.toString <| paths.map (·.2)
|
|
moreDeps
|
|
}
|