forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPackage.lean
232 lines (203 loc) · 9.15 KB
/
Package.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
/-
Copyright (c) 2022 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Util.Git
import Lake.Util.Sugar
import Lake.Build.Common
import Lake.Build.Targets
import Lake.Reservoir
/-! # Package Facet Builds
Build function definitions for a package's builtin facets.
-/
open System
namespace Lake
/-- Compute a topological ordering of the package's transitive dependencies. -/
def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do
(·.toArray) <$> self.deps.foldlM (init := OrdPackageSet.empty) fun deps dep => do
return (← fetch <| dep.facet `deps).foldl (·.insert ·) deps |>.insert dep
/-- The `PackageFacetConfig` for the builtin `depsFacet`. -/
def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
mkFacetConfig Package.recComputeDeps
/--
Tries to download and unpack the package's cached build archive
(e.g., from Reservoir or GitHub).
-/
private def Package.fetchOptBuildCacheCore (self : Package) : FetchM (BuildJob Bool) := do
if self.preferReleaseBuild then
self.optGitHubRelease.fetch
else
self.optReservoirBarrel.fetch
/-- The `PackageFacetConfig` for the builtin `optBuildCacheFacet`. -/
def Package.optBuildCacheFacetConfig : PackageFacetConfig optBuildCacheFacet :=
mkFacetJobConfig (·.fetchOptBuildCacheCore)
/-- Tries to download the package's build cache (if configured). -/
def Package.maybeFetchBuildCache (self : Package) : FetchM (BuildJob Bool) := do
let shouldFetch :=
(← getTryCache) &&
(self.preferReleaseBuild || -- GitHub release
(!self.scope.isEmpty && !(← getElanToolchain).isEmpty)) -- Reservoir
if shouldFetch then
self.optBuildCache.fetch
else
return pure true
@[inline]
private def Package.optFacetDetails (self : Package) (facet : Name) : JobM String := do
if (← getIsVerbose) then
return s!" (see '{self.name}:{facet}' for details)"
else
return " (run with '-v' for details)"
/--
Tries to download and unpack the package's cached build archive
(e.g., from Reservoir or GitHub). Prints a warning on failure.
-/
def Package.maybeFetchBuildCacheWithWarning (self : Package) := do
let job ← self.maybeFetchBuildCache
job.bindSync fun success t => do
unless success do
let details ← self.optFacetDetails <| if self.preferReleaseBuild then
optGitHubReleaseFacet else optReservoirBarrelFacet
logWarning s!"building from source; failed to fetch cloud build{details}"
return ((), t)
@[deprecated maybeFetchBuildCacheWithWarning (since := "2024-09-27")]
def Package.fetchOptRelease := @maybeFetchBuildCacheWithWarning
/--
Build the `extraDepTargets` for the package and its transitive dependencies.
Also fetch pre-built releases for the package's' dependencies.
-/
def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
withRegisterJob s!"{self.name}:extraDep" do
let mut job := BuildJob.nil
-- Build dependencies' extra dep targets
for dep in self.deps do
job := job.mix <| ← dep.extraDep.fetch
-- Fetch build cache if this package is a dependency
if self.name ≠ (← getWorkspace).root.name then
job := job.add <| ← self.maybeFetchBuildCacheWithWarning
-- Build this package's extra dep targets
for target in self.extraDepTargets do
job := job.mix <| ← self.fetchTargetJob target
return job
/-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
mkFacetJobConfig Package.recBuildExtraDepTargets
/-- Compute the package's Reservoir barrel URL. -/
def Package.getBarrelUrl (self : Package) : JobM String := do
if self.scope.isEmpty then
error "package has no Reservoir scope"
let repo := GitRepo.mk self.dir
let some rev ← repo.getHeadRevision?
| error "failed to resolve HEAD revision"
let pkgName := self.name.toString (escape := false)
let env ← getLakeEnv
let mut url := Reservoir.pkgApiUrl env self.scope pkgName
if env.toolchain.isEmpty then
error "Lean toolchain not known; Reservoir only hosts builds for known toolchains"
url := s!"{url}/barrel?rev={rev}&toolchain={uriEncode env.toolchain}"
return url
/-- Compute the package's GitHub release URL. -/
def Package.getReleaseUrl (self : Package) : JobM String := do
let repo := GitRepo.mk self.dir
let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
| error "release repository URL not known; \
the package may need to set 'releaseRepo'"
let some tag ← repo.findTag?
| let rev ← if let some rev ← repo.getHeadRevision? then pure s!" '{rev}'" else pure ""
error s!"no release tag found for revision{rev}"
return s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
/-- Tries to download and unpack a build archive for the package from a URL. -/
def Package.fetchBuildArchive
(self : Package) (url : String) (archiveFile : FilePath)
(headers : Array String := #[])
: JobM PUnit := do
let depTrace := Hash.ofString url
let traceFile := archiveFile.addExtension "trace"
let upToDate ← buildUnlessUpToDate? (action := .fetch) archiveFile depTrace traceFile do
download url archiveFile headers
unless upToDate && (← self.buildDir.pathExists) do
updateAction .fetch
untar archiveFile self.buildDir
@[inline]
private def Package.mkOptBuildArchiveFacetConfig
{facet : Name} (archiveFile : Package → FilePath)
(getUrl : Package → JobM String) (headers : Array String := #[])
[FamilyDef PackageData facet (BuildJob Bool)]
: PackageFacetConfig facet := mkFacetJobConfig fun pkg =>
withRegisterJob s!"{pkg.name}:{facet}" (optional := true) <| Job.async do
try
let url ← getUrl pkg
pkg.fetchBuildArchive url (archiveFile pkg) headers
return (true, .nil)
catch _ =>
updateAction .fetch
return (false, .nil)
@[inline]
private def Package.mkBuildArchiveFacetConfig
{facet : Name} (optFacet : Name) (what : String)
[FamilyDef PackageData facet (BuildJob Unit)]
[FamilyDef PackageData optFacet (BuildJob Bool)]
: PackageFacetConfig facet :=
mkFacetJobConfig fun pkg =>
withRegisterJob s!"{pkg.name}:{facet}" do
(← fetch <| pkg.facet optFacet).bindSync fun success t => do
unless success do
error s!"failed to fetch {what}{← pkg.optFacetDetails optFacet}"
return ((), t)
/-- The `PackageFacetConfig` for the builtin `buildCacheFacet`. -/
def Package.buildCacheFacetConfig : PackageFacetConfig buildCacheFacet :=
mkBuildArchiveFacetConfig optBuildCacheFacet "build cache"
/-- The `PackageFacetConfig` for the builtin `optReservoirBarrelFacet`. -/
def Package.optBarrelFacetConfig : PackageFacetConfig optReservoirBarrelFacet :=
mkOptBuildArchiveFacetConfig barrelFile getBarrelUrl Reservoir.lakeHeaders
/-- The `PackageFacetConfig` for the builtin `reservoirBarrelFacet`. -/
def Package.barrelFacetConfig : PackageFacetConfig reservoirBarrelFacet :=
mkBuildArchiveFacetConfig optReservoirBarrelFacet "Reservoir barrel"
/-- The `PackageFacetConfig` for the builtin `optGitHubReleaseFacet`. -/
def Package.optGitHubReleaseFacetConfig : PackageFacetConfig optGitHubReleaseFacet :=
mkOptBuildArchiveFacetConfig buildArchiveFile getReleaseUrl
@[deprecated (since := "2024-09-27")]
abbrev Package.optReleaseFacetConfig := optGitHubReleaseFacetConfig
/-- The `PackageFacetConfig` for the builtin `gitHubReleaseFacet`. -/
def Package.gitHubReleaseFacetConfig : PackageFacetConfig gitHubReleaseFacet :=
mkBuildArchiveFacetConfig optGitHubReleaseFacet "GitHub release"
@[deprecated (since := "2024-09-27")]
abbrev Package.releaseFacetConfig := gitHubReleaseFacetConfig
/--
Perform a build job after first checking for an (optional) cached build
for the package (e.g., from Reservoir or GitHub).
-/
def Package.afterBuildCacheAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
if self.name ≠ (← getRootPackage).name then
(← self.maybeFetchBuildCache).bindAsync fun _ _ => build
else
build
@[deprecated afterBuildCacheAsync (since := "2024-09-27")]
def Package.afterReleaseAsync := @afterBuildCacheAsync
/--
Perform a build after first checking for an (optional) cached build
for the package (e.g., from Reservoir or GitHub).
-/
def Package.afterBuildCacheSync (self : Package) (build : JobM α) : FetchM (Job α) := do
if self.name ≠ (← getRootPackage).name then
(← self.maybeFetchBuildCache).bindSync fun _ _ => build
else
Job.async build
@[deprecated afterBuildCacheSync (since := "2024-09-27")]
def Package.afterReleaseSync := @afterBuildCacheSync
open Package in
/--
A package facet name to build function map that contains builders for
the initial set of Lake package facets (e.g., `extraDep`).
-/
def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
DNameMap.empty
|>.insert depsFacet depsFacetConfig
|>.insert extraDepFacet extraDepFacetConfig
|>.insert optBuildCacheFacet optBuildCacheFacetConfig
|>.insert buildCacheFacet buildCacheFacetConfig
|>.insert optReservoirBarrelFacet optBarrelFacetConfig
|>.insert reservoirBarrelFacet barrelFacetConfig
|>.insert optGitHubReleaseFacet optGitHubReleaseFacetConfig
|>.insert gitHubReleaseFacet gitHubReleaseFacetConfig