max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: add buildDir setting and make bin/lib/ir subdirs of it

Browse source
This commit is contained in:
tydeu 2021-07-28 12:23:37 -04:00
parent cce0b3cce5
commit d8ac18a807
2 changed files with 13 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
Lake/Package.lean
View file

@ -14,10 +14,10 @@ open Lean Std System
namespace Lake
def defaultBuildDir : FilePath := "build"
def defaultBinDir := defaultBuildDir / "bin"
def defaultLibDir := defaultBuildDir / "lib"
def defaultOleanDir := defaultBuildDir / "lib"
def defaultIrDir := defaultBuildDir / "ir"
def defaultBinDir : FilePath := "bin"
def defaultLibDir : FilePath := "lib"
def defaultOleanDir : FilePath := "lib"
def defaultIrDir : FilePath := "ir"
def defaultDepsDir : FilePath := "lean_packages"
inductive Source where
@ -42,6 +42,7 @@ structure PackageConfig where
linkArgs : Array String := #[]
rootDir : FilePath := "."
srcDir : FilePath := rootDir
buildDir : FilePath := defaultBuildDir
oleanDir : FilePath := defaultOleanDir
irDir : FilePath := defaultIrDir
binDir : FilePath := defaultBinDir
@ -111,8 +112,11 @@ def modToSrc (mod : Name) (self : Package) : FilePath :=
def srcRoot (self : Package) : FilePath :=
self.modToSrc self.moduleRoot
def buildDir (self : Package) : FilePath :=
self.dir / self.config.buildDir
def oleanDir (self : Package) : FilePath :=
self.dir / self.config.oleanDir
self.buildDir / self.config.oleanDir
def modToOlean (mod : Name) (self : Package) : FilePath :=
Lean.modToFilePath self.oleanDir mod "olean"
@ -124,7 +128,7 @@ def modToHashFile (mod : Name) (self : Package) : FilePath :=
Lean.modToFilePath self.oleanDir mod "hash"
def irDir (self : Package) : FilePath :=
self.dir / self.config.irDir
self.buildDir / self.config.irDir
def cDir (self : Package) : FilePath :=
self.irDir
@ -139,7 +143,7 @@ def modToO (mod : Name) (self : Package) : FilePath :=
Lean.modToFilePath self.oDir mod "o"
def binDir (self : Package) : FilePath :=
self.dir / self.config.binDir
self.buildDir / self.config.binDir
def binName (self : Package) : FilePath :=
self.config.binName
@ -151,7 +155,7 @@ def binFile (self : Package) : FilePath :=
self.binDir / self.binFileName
def libDir (self : Package) : FilePath :=
self.dir / self.config.libDir
self.buildDir / self.config.libDir
def staticLibName (self : Package) : FilePath :=
self.config.libName

2
examples/bootstrap/package.lean
View file

@ -6,7 +6,7 @@ def package : PackageConfig := {
name := "lake"
version := "2.0-pre-bootstrap"
rootDir := FilePath.mk ".." / ".."
oleanDir := defaultBuildDir
oleanDir := "."
leancArgs := #["-O3", "-DNDEBUG"]
linkArgs :=
if Platform.isWindows then