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

chore: improve imports lean-only build condition

Browse source
This commit is contained in:
tydeu 2022-06-09 21:08:06 -04:00
parent 6f38ebebe9
commit 8428ef7cd7
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Lake/Build/Package.lean
View file

@ -90,8 +90,8 @@ def Workspace.processImportList
/--
Build the workspace-local modules of list of imports.
Build only module `.olean` and `.ilean` files if the default package facet is
just `leanLib` or `oleans` (and the package has no binary executable targets).
Build only module `.olean` and `.ilean` files if
the default package build does not include any binary targets
Otherwise, also build `.c` files.
-/
def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM PUnit := do
@ -102,7 +102,7 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
else
-- build local imports from list
let infos := (← getWorkspace).processImportList imports
if (self.defaultFacet == .leanLib || self.defaultFacet == .oleans) && self.exes.isEmpty then
if self.exes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then
let build := recBuildModuleOleanTargetWithLocalImports depTarget
let targets ← buildModuleArray infos build
targets.forM (·.buildOpaque)