feat: build packages without make

This commit is contained in:
tydeu 2021-07-08 19:46:10 -04:00
parent 9034b6b79b
commit 981db940e8
11 changed files with 298 additions and 209 deletions

View file

@ -7,162 +7,217 @@ import Lean.Data.Name
import Lean.Elab.Import
import Lake.Resolve
import Lake.Package
import Lake.Make
import Lake.Proc
import Lake.Compile
open Lean System
open System
open Lean hiding SearchPath
namespace Lake
structure BuildConfig where
module : Name
leanArgs : List String
leanPath : String
-- things that should also trigger rebuilds
-- ex. olean roots of dependencies
moreDeps : List FilePath
-- # Basic Build Infos
def mkBuildConfig
(pkg : Package) (deps : List Package) (leanArgs : List String)
: BuildConfig := {
leanArgs,
module := pkg.module
leanPath := SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
moreDeps := deps.map (·.oleanRoot)
}
structure BuildContext extends BuildConfig where
parents : List Name := []
moreDepsMTime : IO.FS.SystemTime
structure BuildResult where
maxMTime : IO.FS.SystemTime
task : Task (Except IO.Error Unit)
structure BuildInfo (α : Type) where
artifact : α
maxMTime : IO.FS.SystemTime
task : Task (Except IO.Error PUnit)
deriving Inhabited
structure BuildState where
modTasks : NameMap BuildResult := ∅
abbrev ModuleBuildInfo := BuildInfo (FilePath × FilePath)
abbrev BuildM := ReaderT BuildContext <| StateT BuildState IO
namespace ModuleBuildInfo
def oleanFile (self : ModuleBuildInfo) := self.artifact.1
def cFile (self : ModuleBuildInfo) := self.artifact.2
end ModuleBuildInfo
partial def buildModule (mod : Name) : BuildM BuildResult := do
let ctx ← read
-- detect cyclic imports
if ctx.parents.contains mod then
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}"
-- skip if already visited
if let some res := (← get).modTasks.find? mod then
return res
-- deduce lean file
let leanFile := modToFilePath "." mod "lean"
-- parse imports
let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
let localImports := imports.filter (·.module.getRoot == ctx.module)
-- recursively build local dependencies
let deps ← localImports.mapM fun i =>
withReader (fun ctx => { ctx with parents := mod :: ctx.parents }) <|
buildModule i.module
-- calculate transitive `maxMTime`
let leanMData ← leanFile.metadata
let depMTimes ← deps.mapM (·.maxMTime)
let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
-- check whether we have an up-to-date .olean
let oleanFile := modToFilePath buildPath mod "olean"
def buildOleanAndC (leanFile oleanFile cFile : FilePath)
(depInfos : List ModuleBuildInfo) (maxMTime : IO.FS.SystemTime)
(leanPath : String := "") (rootDir : FilePath := ".") (leanArgs : Array String := #[])
: IO ModuleBuildInfo := do
let artifact := (oleanFile, cFile)
-- check whether we have an up-to-date .olean and .c
try
if (← oleanFile.metadata).modified >= maxMTime then
let res := { maxMTime, task := Task.pure (Except.ok ()) }
modify fun st => { st with modTasks := st.modTasks.insert mod res }
return res
let cMTime := (← cFile.metadata).modified
let oleanMTime := (← oleanFile.metadata).modified
if cMTime >= maxMTime && oleanMTime >= maxMTime then
let task := Task.pure (Except.ok ())
return { artifact, maxMTime, task }
catch
| IO.Error.noFileOrDirectory .. => pure ()
| e => throw e
-- (try to) compile the olean and c file
let task ← IO.mapTasks (tasks := deps.map (·.task)) fun rs => do
if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then
-- propagate failure from dependencies
throw e
let task ← IO.mapTasks (tasks := depInfos.map (·.task)) fun rs => do
rs.forM IO.ofExcept -- propagate first failure from dependencies
try
let cFile := modToFilePath tempBuildPath mod "c"
IO.FS.createDirAll oleanFile.parent.get!
IO.FS.createDirAll cFile.parent.get!
execCmd {
cmd := "lean"
args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]
env := #[("LEAN_PATH", ctx.leanPath)]
}
compileOleanAndC leanFile oleanFile cFile leanPath rootDir leanArgs
catch e =>
-- print compile errors early
IO.eprintln e
throw e
return { artifact, maxMTime, task }
let res := { maxMTime, task := task }
modify fun st => { st with modTasks := st.modTasks.insert mod res }
return res
def buildO (oFile : FilePath)
(cInfo : BuildInfo FilePath) (leancArgs : Array String := #[])
: IO (BuildInfo FilePath) := do
-- skip if we have an up-to-date .o
try
let cMTime := cInfo.maxMTime
if (← oFile.metadata).modified >= cMTime then
return {artifact := oFile, maxMTime := cMTime, task := Task.pure (Except.ok ()) }
catch
| IO.Error.noFileOrDirectory .. => pure ()
| e => throw e
-- compile it otherwise
let task ← IO.mapTask (t := cInfo.task) fun x => do
IO.ofExcept x -- propagate failure from building .c
try
compileO oFile cInfo.artifact leancArgs
catch e =>
-- print compile errors early
IO.eprintln e
throw e
return {artifact := oFile, maxMTime := cInfo.maxMTime, task }
def buildModules (cfg : BuildConfig) (mods : List Name) : IO Unit := do
let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
let rs ← mods.mapM buildModule |>.run { toBuildConfig := cfg, moreDepsMTime } |>.run' {}
for r in rs do
if let Except.error _ ← IO.wait r.task then
-- actual error has already been printed above
throw <| IO.userError "Build failed."
-- # Build Modules
def buildImports (pkg : Package) (deps : List Package) (imports leanArgs : List String := []) : IO Unit := do
let imports := imports.map (·.toName)
let localImports := imports.filter (·.getRoot == pkg.module)
if localImports != [] then
if ← FilePath.pathExists "Makefile" then
let oleans := localImports.map fun i =>
Lean.modToFilePath buildPath i "olean" |>.toString
execMake pkg deps oleans leanArgs
else
buildModules (mkBuildConfig pkg deps leanArgs) localImports
structure BuildContext where
package : Package
leanPath : String
-- things that should also trigger rebuilds
-- ex. olean roots of dependencies
moreDeps : List FilePath
buildParents : List Name := []
moreDepsMTime : IO.FS.SystemTime
def buildPkg (pkg : Package) (deps : List Package) (makeArgs leanArgs : List String := []) : IO Unit := do
if makeArgs != [] || (← FilePath.pathExists "Makefile") then
execMake pkg deps makeArgs leanArgs
else
buildModules (mkBuildConfig pkg deps leanArgs) [pkg.module]
structure BuildState where
buildInfos : NameMap ModuleBuildInfo := ∅
def buildDeps (pkg : Package) (makeArgs leanArgs : List String := []) : IO (List Package) := do
abbrev BuildM := ReaderT BuildContext <| StateT BuildState IO
partial def buildModule (mod : Name) : BuildM ModuleBuildInfo := do
let ctx ← read
let pkg := ctx.package
-- detect cyclic imports
if ctx.buildParents.contains mod then
let cycle := mod :: (ctx.buildParents.partition (· != mod)).1 ++ [mod]
let cycle := cycle.map (s!" {·}")
throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
-- return previous result if already visited
if let some info := (← get).buildInfos.find? mod then
return info
-- deduce lean file
let leanFile := ctx.package.modToSource mod
-- parse imports
let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
let directLocalImports := imports.map (·.module) |>.filter (·.getRoot == pkg.module)
-- recursively build local dependencies
let depInfos ← directLocalImports.mapM fun i =>
withReader (fun ctx => { ctx with buildParents := mod :: ctx.buildParents }) <|
buildModule i
-- calculate transitive `maxMTime`
let leanMData ← leanFile.metadata
let depMTimes ← depInfos.mapM (·.maxMTime)
let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
-- do build
let cFile := pkg.modToC mod
let oleanFile := pkg.modToOlean mod
let info ← buildOleanAndC leanFile oleanFile cFile
depInfos maxMTime ctx.leanPath pkg.dir pkg.leanArgs
modify fun st => { st with buildInfos := st.buildInfos.insert mod info }
return info
def mkBuildContext (pkg : Package) (deps : List Package) : IO BuildContext := do
let moreDeps := deps.map (·.oleanRoot)
let moreDepsMTime := (← moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
let leanPath := SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
return { package := pkg, leanPath, moreDeps, moreDepsMTime }
def buildPackageModulesCore
(pkg : Package) (deps : List Package) : IO (ModuleBuildInfo × BuildState) := do
let crx ← mkBuildContext pkg deps
buildModule pkg.module |>.run crx |>.run {}
def buildPackageModuleDAG
(pkg : Package) (deps : List Package) : IO (NameMap ModuleBuildInfo) := do
(← buildPackageModulesCore pkg deps).2.buildInfos
-- # Configure/Build Packages
def buildPackageModules
(pkg : Package) (deps : List Package) : IO PUnit := do
let (info, _) ← buildPackageModulesCore pkg deps
if let Except.error _ ← IO.wait info.task then
-- actual error has already been printed above
throw <| IO.userError "Build failed."
def buildDeps (pkg : Package) : IO (List Package) := do
let deps ← solveDeps pkg
for dep in deps do
-- build recursively
-- TODO: share build of common dependencies
let depDeps ← solveDeps dep
buildPkg dep depDeps makeArgs leanArgs
buildPackageModules pkg deps
return deps
def configure (pkg : Package) : IO Unit :=
def configure (pkg : Package) : IO Unit := do
discard <| buildDeps pkg
def printPaths (pkg : Package) (imports leanArgs : List String := []) : IO Unit := do
def build (pkg : Package) : IO Unit := do
let deps ← buildDeps pkg
buildImports pkg deps imports leanArgs
buildPackageModules pkg deps
-- # Build Package Lib/Bin
def buildPackageOFiles (pkg : Package) (buildMap : NameMap ModuleBuildInfo)
: IO (List FilePath) := do
let oInfos ← buildMap.toList.mapM fun (mod, info) =>
let oFile := pkg.modToO mod
buildO oFile {info with artifact := info.cFile} pkg.leancArgs
oInfos.mapM fun info => do
IO.ofExcept (← IO.wait info.task)
info.artifact
def buildStaticLib (pkg : Package) : IO FilePath := do
let deps ← buildDeps pkg
let buildMap ← buildPackageModuleDAG pkg deps
let oFiles ← buildPackageOFiles pkg buildMap
compileLib pkg.staticLibFile oFiles.toArray
pkg.staticLibFile
def buildBin (pkg : Package) : IO FilePath := do
let deps ← solveDeps pkg
let depLibs ← deps.mapM buildStaticLib
let buildMap ← buildPackageModuleDAG pkg deps
let oFiles ← buildPackageOFiles pkg buildMap
compileBin pkg.binFile (oFiles ++ depLibs).toArray pkg.linkArgs
pkg.binFile
-- # Print Paths
def buildModulesInPackage (pkg : Package) (deps : List Package) (mods : List Name) : IO Unit := do
let ctx ← mkBuildContext pkg deps
let rs ← mods.mapM buildModule |>.run ctx |>.run' {}
for r in rs do
if let Except.error _ ← IO.wait r.task then
-- actual error has already been printed above
throw <| IO.userError "Build failed."
def buildImports
(pkg : Package) (deps : List Package) (imports : List String := [])
: IO Unit := do
let imports := imports.map (·.toName)
let localImports := imports.filter (·.getRoot == pkg.module)
buildModulesInPackage pkg deps localImports
def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do
let deps ← buildDeps pkg
buildImports pkg deps imports
IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
IO.println <| SearchPath.toString <| pkg.sourceDir :: deps.map (·.sourceDir)
private def relPathToUnixString (path : FilePath) : String :=
if Platform.isWindows then
path.toString.map fun c => if c == '\\' then '/' else c
else
path.toString
def build (pkg : Package) (makeArgs leanArgs : List String := []) : IO Unit := do
if makeArgs.contains "bin" then
let deps ← buildDeps pkg ["lib"]
let depLibs := " ".intercalate <| deps.map (relPathToUnixString ·.staticLibPath)
buildPkg pkg deps (s!"LINK_OPTS=\"{depLibs}\"" :: makeArgs) leanArgs
else
let deps ← buildDeps pkg
buildPkg pkg deps makeArgs leanArgs

View file

@ -68,16 +68,18 @@ def getRootPkg : IO Package := do
leanVersionString ++ ", but package requires " ++ cfg.leanVersion ++ "\n"
return ⟨".", cfg⟩
def cli : (cmd : String) → (lakeArgs leanArgs : List String) → IO Unit
| "init", [name], [] => init name
| "configure", [], [] => do configure (← getRootPkg)
| "print-paths", imports, leanArgs => do printPaths (← getRootPkg) imports leanArgs
| "build", makeArgs, leanArgs => do build (← getRootPkg) makeArgs leanArgs
| "help", ["init"], [] => IO.println helpInit
| "help", ["configure"], [] => IO.println helpConfigure
| "help", ["build"], [] => IO.println helpBuild
| "help", _, [] => IO.println usage
| _, _, _ => throw <| IO.userError usage
def cli : (cmd : String) → (lakeArgs pkgArgs : List String) → IO Unit
| "init", [name], [] => init name
| "configure", [], [] => do configure (← getRootPkg)
| "print-paths", imports, [] => do printPaths (← getRootPkg) imports
| "build", [], [] => do build (← getRootPkg)
| "build-bin", [], [] => do discard <| buildBin (← getRootPkg)
| "build-lib", [], [] => do discard <| buildStaticLib (← getRootPkg)
| "help", ["init"], [] => IO.println helpInit
| "help", ["configure"], [] => IO.println helpConfigure
| "help", ["build"], [] => IO.println helpBuild
| "help", _, [] => IO.println usage
| _, _, _ => throw <| IO.userError usage
private def splitCmdlineArgsCore : List String → List String × List String
| [] => ([], [])

51
Lake/Compile.lean Normal file
View file

@ -0,0 +1,51 @@
/-
Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Proc
namespace Lake
open System
def compileOleanAndC
(leanFile oleanFile cFile : FilePath)
(leanPath : String := "") (rootDir : FilePath := ".") (leanArgs : Array String := #[])
: IO Unit := do
if let some dir := cFile.parent then IO.FS.createDirAll dir
if let some dir := oleanFile.parent then IO.FS.createDirAll dir
execCmd {
cmd := "lean"
args := leanArgs ++ #[
"-R", rootDir.toString, "-o", oleanFile.toString, "-c",
cFile.toString, leanFile.toString
]
env := #[("LEAN_PATH", leanPath)]
}
def compileO
(oFile cFile : FilePath) (leancArgs : Array String := #[])
: IO Unit := do
if let some dir := oFile.parent then IO.FS.createDirAll dir
execCmd {
cmd := "leanc"
args := #["-c", "-o", oFile.toString, cFile.toString] ++ leancArgs
}
def compileBin
(binFile : FilePath) (oFiles : Array FilePath) (linkArgs : Array String := #[])
: IO Unit := do
if let some dir := binFile.parent then IO.FS.createDirAll dir
execCmd {
cmd := "leanc"
args := #["-o", binFile.toString] ++ oFiles.map toString ++ linkArgs
}
def compileLib
(libFile : FilePath) (oFiles : Array FilePath)
: IO Unit := do
if let some dir := libFile.parent then IO.FS.createDirAll dir
execCmd {
cmd := "ar"
args := #["rcs", libFile.toString] ++ oFiles.map toString
}

View file

@ -1,59 +0,0 @@
/-
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 Lake.Proc
import Lake.Package
open System
namespace Lake
def lockfile : FilePath := buildPath / ".lake-lock"
partial def withLockFile (x : IO α) : IO α := do
acquire
try
x
finally
IO.FS.removeFile lockfile
where
acquire (firstTime := true) := do
IO.FS.createDirAll lockfile.parent.get!
try
-- TODO: lock file should ideally contain PID
if !Platform.isWindows then
discard <| IO.FS.Handle.mkPrim lockfile "wx"
else
-- `x` mode doesn't seem to work on Windows even though it's listed at
-- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
-- ...? Let's use the slightly racy approach then.
if ← lockfile.pathExists then
throw <| IO.Error.alreadyExists 0 ""
discard <| IO.FS.Handle.mk lockfile IO.FS.Mode.write
catch
| IO.Error.alreadyExists _ _ => do
if firstTime then
IO.eprintln s!"Waiting for prior lake invocation to finish... (remove '{lockfile}' if stuck)"
IO.sleep (ms := 300)
acquire (firstTime := false)
| e => throw e
def execMake
(pkg : Package) (deps : List Package) (makeArgs leanArgs : List String := [])
: IO Unit := withLockFile do
let timeoutArgs :=
match pkg.timeout with
| some t => ["-T", toString t]
| none => []
let leanOptsStr := " ".intercalate <| timeoutArgs ++ leanArgs
let leanPathStr := SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
let makeArgsStr := " ".intercalate makeArgs
let moreDepsStr := " ".intercalate <| deps.map (·.oleanRoot.toString)
let mut spawnArgs := {
cmd := "sh"
cwd := pkg.dir
args := #["-c", s!"leanmake PKG={pkg.module} LEAN_OPTS=\"{leanOptsStr}\" LEAN_PATH=\"{leanPathStr}\" {makeArgsStr} MORE_DEPS+=\"{moreDepsStr}\" >&2"]
}
execCmd spawnArgs

View file

@ -4,6 +4,7 @@ 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.LeanVersion
open Lean System
@ -26,6 +27,9 @@ structure PackageConfig where
name : String
version : String
leanVersion : String := leanVersionString
leanArgs : Array String := #[]
leancArgs : Array String := #[]
linkArgs : Array String := #[]
timeout : Option Nat := none
module : Name := name.capitalize
dependencies : List Dependency := []
@ -50,6 +54,15 @@ def moduleName (self : Package) :=
def dependencies (self : Package) :=
self.config.dependencies
def leanArgs (self : Package) :=
self.config.leanArgs
def leancArgs (self : Package) :=
self.config.leancArgs
def linkArgs (self : Package) :=
self.config.linkArgs
def timeout (self : Package) :=
self.config.timeout
@ -59,29 +72,56 @@ def sourceDir (self : Package) :=
def sourceRoot (self : Package) :=
self.sourceDir / self.moduleName
def modToSource (mod : Name) (self : Package) :=
Lean.modToFilePath self.sourceDir mod "lean"
def buildDir (self : Package) :=
self.dir / Lake.buildPath
def oleanDir (self : Package) :=
self.buildDir
def oleanRoot (self : Package) :=
self.oleanDir / FilePath.withExtension self.moduleName "olean"
def modToOlean (mod : Name) (self : Package) :=
Lean.modToFilePath self.oleanDir mod "olean"
def tempBuildDir (self : Package) :=
self.dir / tempBuildPath
def cDir (self : Package) :=
self.tempBuildDir
def modToC (mod : Name) (self : Package) :=
Lean.modToFilePath self.cDir mod "c"
def oDir (self : Package) :=
self.tempBuildDir
def modToO (mod : Name) (self : Package) :=
Lean.modToFilePath self.oDir mod "o"
def binDir (self : Package) :=
self.buildDir / "bin"
def binName (self : Package) :=
self.moduleName
def binPath (self : Package) :=
self.binDir / FilePath.withExtension self.binName FilePath.exeExtension
def binFileName (self : Package) : FilePath :=
FilePath.withExtension self.binName FilePath.exeExtension
def binFile (self : Package) :=
self.binDir / self.binFileName
def libDir (self : Package) :=
self.buildDir / "lib"
def staticLibFile (self : Package) :=
def staticLibName (self : Package) :=
self.moduleName
def staticLibFileName (self : Package) :=
s!"lib{self.module}.a"
def staticLibPath (self : Package) :=
self.libDir / self.staticLibFile
def oleanDir (self : Package) :=
self.dir / Lake.buildPath
def oleanRoot (self : Package) :=
self.oleanDir / FilePath.withExtension self.moduleName "olean"
def staticLibFile (self : Package) :=
self.libDir / self.staticLibFileName

View file

@ -30,7 +30,6 @@ def materialize (pkgDir : FilePath) (dep : Dependency) : IO FilePath :=
match dep.src with
| Source.path dir => do
let depdir := pkgDir / dir
IO.eprintln s!"{dep.name}: using local path {depdir}"
depdir
| Source.git url rev branch => do
let depdir := pkgDir / depsPath / dep.name

View file

@ -58,10 +58,10 @@ def package : Lake.PackageConfig := {
}
```
We can use the command `lake build bin` to build the module (and its dependencies, if it has them) and a native executable. The latter of which will be written to `build/bin`.
We can use the command `lake build-bin` to build the package (and its dependencies, if it has them) into a native executable. The result will be placed in to `build/bin`.
```
$ lake build bin
$ lake build-bin
...
$ ./build/bin/Hello
Hello, world!

View file

@ -1 +1 @@
leanpkg build bin LINK_OPTS=-Wl,--export-all
leanpkg build bin LINK_OPTS=-Wl,--export-all "$@"

View file

@ -1 +1 @@
leanpkg build bin LINK_OPTS=-rdynamic
leanpkg build bin LINK_OPTS=-rdynamic "$@"

View file

@ -1 +1 @@
../../build/bin/Lake build bin
../../build/bin/Lake build-bin

View file

@ -1,2 +1,3 @@
cd foo
../../../build/bin/Lake build bin
echo "in directory 'foo'"
../../../build/bin/Lake build-bin