170 lines
7 KiB
Text
170 lines
7 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 Lean.Data.Name
|
||
import Lean.Elab.Import
|
||
import Lake.Target
|
||
import Lake.BuildModule
|
||
import Lake.Resolve
|
||
import Lake.Package
|
||
|
||
open System
|
||
open Lean hiding SearchPath
|
||
|
||
namespace Lake
|
||
|
||
-- # Build Target
|
||
|
||
abbrev ActivePackageTarget := ActiveBuildTarget (Package × NameMap ActiveOleanAndCTarget)
|
||
|
||
namespace ActivePackageTarget
|
||
|
||
def package (self : ActivePackageTarget) :=
|
||
self.info.1
|
||
|
||
def moduleTargetMap (self : ActivePackageTarget) : NameMap ActiveOleanAndCTarget :=
|
||
self.info.2
|
||
|
||
def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveOleanAndCTarget) :=
|
||
self.moduleTargetMap.fold (fun arr k v => arr.push (k, v)) #[]
|
||
|
||
end ActivePackageTarget
|
||
|
||
-- # Build Modules
|
||
|
||
def Package.buildModuleOleanAndCTargetDAG
|
||
(mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
|
||
(self : Package) : BuildM (Array ActiveOleanAndCTarget × OleanAndCTargetMap) := do
|
||
let buildMod : OleanAndCTargetBuild :=
|
||
self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget
|
||
let (resE, map) ← mods.mapM (buildRBTop buildMod id) |>.run
|
||
(← failOnBuildCycle resE, map)
|
||
|
||
def Package.buildModuleOleanTargetDAG
|
||
(mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
|
||
(self : Package) : BuildM (Array ActiveFileTarget × OleanTargetMap) := do
|
||
let buildMod : OleanTargetBuild :=
|
||
self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget
|
||
let (resE, map) ← RBTopT.run <| mods.mapM (buildRBTop buildMod id)
|
||
(← failOnBuildCycle resE, map)
|
||
|
||
def Package.buildOleanAndCTargetDAG
|
||
(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
|
||
(self : Package) : BuildM (Array ActiveOleanAndCTarget × OleanAndCTargetMap) := do
|
||
self.buildModuleOleanAndCTargetDAG (← self.getModuleArray) moreOleanDirs depTarget
|
||
|
||
def Package.buildOleanTargetDAG
|
||
(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
|
||
(self : Package) : BuildM (Array ActiveFileTarget × OleanTargetMap) := do
|
||
self.buildModuleOleanTargetDAG (← self.getModuleArray) moreOleanDirs depTarget
|
||
|
||
def Package.buildModuleOleanAndCTargets
|
||
(mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
|
||
(self : Package) : BuildM (Array ActiveOleanAndCTarget) := do
|
||
let buildMod : OleanAndCTargetBuild :=
|
||
self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget
|
||
failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <| buildRBTop buildMod id
|
||
|
||
def Package.buildModuleOleanTargets
|
||
(mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
|
||
(self : Package) : BuildM (Array ActiveFileTarget) := do
|
||
let buildMod : OleanTargetBuild :=
|
||
self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget
|
||
failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <| buildRBTop buildMod id
|
||
|
||
def Package.buildOleanAndCTargets
|
||
(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
|
||
(self : Package) : BuildM (Array ActiveOleanAndCTarget) := do
|
||
self.buildModuleOleanAndCTargets (← self.getModuleArray) moreOleanDirs depTarget
|
||
|
||
def Package.buildOleanTargets
|
||
(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
|
||
(self : Package) : BuildM (Array ActiveFileTarget) := do
|
||
self.buildModuleOleanTargets (← self.getModuleArray) moreOleanDirs depTarget
|
||
|
||
-- # Configure/Build Packages
|
||
|
||
def Package.buildDepTargetWith
|
||
(depTargets : List ActivePackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do
|
||
let extraDepTarget ← self.extraDepTarget.run
|
||
let depTarget ← ActiveTarget.collectOpaqueList depTargets
|
||
extraDepTarget.mixOpaqueAsync depTarget
|
||
|
||
def Package.buildModuleOleanAndCTargetsWithDepTargets
|
||
(mods : Array Name) (depTargets : List ActivePackageTarget) (self : Package)
|
||
: BuildM ActivePackageTarget := do
|
||
let depTarget ← self.buildDepTargetWith depTargets
|
||
let moreOleanDirs := depTargets.map (·.package.oleanDir)
|
||
let (targets, targetMap) ← self.buildModuleOleanAndCTargetDAG mods moreOleanDirs depTarget
|
||
let target ← ActiveTarget.collectOpaqueArray targets
|
||
return target.withInfo ⟨self, targetMap⟩
|
||
|
||
def Package.buildOleanAndCTargetsWithDepTargets
|
||
(depTargets : List ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget := do
|
||
self.buildModuleOleanAndCTargetsWithDepTargets (← self.getModuleArray) depTargets
|
||
|
||
/--
|
||
The main package build function.
|
||
|
||
It resolves the package's dependencies and recursively builds them.
|
||
For each package, it compiles its modules into `.olean` and `.c` files.
|
||
-/
|
||
def recBuildPkgWithDeps [Monad m] [MonadLiftT BuildM m]
|
||
: RecBuild Package ActivePackageTarget m := fun pkg buildPkg => do
|
||
-- TODO: merge dependency resolution into build
|
||
let deps ← liftM (m := BuildM) <| solveDeps pkg
|
||
pkg.buildOleanAndCTargetsWithDepTargets (← deps.mapM buildPkg)
|
||
|
||
def buildPackageTargetList (pkgs : List Package) : BuildM (List ActivePackageTarget) := do
|
||
failOnBuildCycle <| ← RBTopT.run' <| pkgs.mapM fun pkg =>
|
||
buildRBTop (cmp := Name.quickCmp) recBuildPkgWithDeps (·.name.toName) pkg
|
||
|
||
def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do
|
||
failOnBuildCycle <| ← RBTopT.run' <|
|
||
buildRBTop (cmp := Name.quickCmp) recBuildPkgWithDeps (·.name.toName) self
|
||
|
||
def Package.buildDepTargets (self : Package) : BuildM (List ActivePackageTarget) := do
|
||
buildPackageTargetList (← solveDeps self)
|
||
|
||
def Package.buildDeps (self : Package) : BuildM (List Package) := do
|
||
let deps ← solveDeps self
|
||
let targets ← buildPackageTargetList deps
|
||
targets.forM (discard ·.materialize)
|
||
return deps
|
||
|
||
def configure (pkg : Package) : IO Unit :=
|
||
pkg.buildDeps.run
|
||
|
||
def Package.build (self : Package) : BuildM PUnit := do
|
||
let depTargets ← self.buildDepTargets
|
||
let depTarget ← self.buildDepTargetWith depTargets
|
||
let moreOleanDirs := depTargets.map (·.package.oleanDir)
|
||
let targets ← self.buildOleanTargets moreOleanDirs depTarget
|
||
discard <| ActiveTarget.materializeArray targets
|
||
|
||
def build (pkg : Package) : IO PUnit :=
|
||
pkg.build.run
|
||
|
||
-- # Print Paths
|
||
|
||
def Package.buildModuleOleanTargetsWithDeps
|
||
(deps : List Package) (mods : Array Name) (self : Package)
|
||
: BuildM (Array ActiveFileTarget) := do
|
||
let moreOleanDirs := deps.map (·.oleanDir)
|
||
let depTarget ← self.buildDepTargetWith <| ← buildPackageTargetList deps
|
||
self.buildModuleOleanTargets mods moreOleanDirs depTarget
|
||
|
||
def Package.buildModuleOleansWithDeps
|
||
(deps : List Package) (mods : Array Name) (self : Package) :=
|
||
self.buildModuleOleanTargetsWithDeps deps mods >>= (·.forM (discard ·.materialize))
|
||
|
||
def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do
|
||
let deps ← solveDeps pkg
|
||
unless imports.isEmpty do
|
||
let imports := imports.map (·.toName)
|
||
let localImports := imports.filter pkg.isLocalModule |>.toArray
|
||
pkg.buildModuleOleansWithDeps deps localImports |>.run
|
||
IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
|
||
IO.println <| SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir)
|