This repository has been archived by the owner on Oct 25, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 19
/
Package.lean
367 lines (292 loc) · 12.6 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
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
/-
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.Config.Opaque
import Lake.Config.LeanLibConfig
import Lake.Config.LeanExeConfig
import Lake.Config.ExternLibConfig
import Lake.Config.WorkspaceConfig
import Lake.Config.Dependency
import Lake.Config.Script
import Lake.Util.DRBMap
import Lake.Util.OrdHashSet
open System Lean
namespace Lake
/-- A string descriptor of the `System.Platform` OS (`windows`, `macOS`, or `linux`). -/
def osDescriptor : String :=
if Platform.isWindows then
"windows"
else if Platform.isOSX then
"macOS"
else
"linux"
/--
A `tar.gz` file name suffix encoding the the current Platform.
(i.e, `osDescriptor` joined with `System.Platform.numBits`).
-/
def archiveSuffix :=
s!"{osDescriptor}-{Platform.numBits}.tar.gz"
/-- If `name?`, `{name}-{archiveSuffix}`, otherwise just `archiveSuffix`. -/
def nameToArchive (name? : Option String) : String :=
match name? with
| none => archiveSuffix
| some name => s!"{name}-{archiveSuffix}"
/--
First tries to convert a string into a legal name.
If that fails, defaults to making it a simple name (e.g., `Lean.Name.mkSimple`).
Currently used for package and target names taken from the CLI.
-/
def stringToLegalOrSimpleName (s : String) : Name :=
if s.toName.isAnonymous then Lean.Name.mkSimple s else s.toName
--------------------------------------------------------------------------------
/-! # Defaults -/
--------------------------------------------------------------------------------
/-- The default setting for a `PackageConfig`'s `manifestFile` option. -/
def defaultManifestFile := "lake-manifest.json"
/-- The default setting for a `PackageConfig`'s `buildDir` option. -/
def defaultBuildDir : FilePath := "build"
/-- The default setting for a `PackageConfig`'s `leanLibDir` option. -/
def defaultLeanLibDir : FilePath := "lib"
/-- The default setting for a `PackageConfig`'s `nativeLibDir` option. -/
def defaultNativeLibDir : FilePath := "lib"
/-- The default setting for a `PackageConfig`'s `binDir` option. -/
def defaultBinDir : FilePath := "bin"
/-- The default setting for a `PackageConfig`'s `irDir` option. -/
def defaultIrDir : FilePath := "ir"
--------------------------------------------------------------------------------
/-! # PackageConfig -/
--------------------------------------------------------------------------------
/-- A `Package`'s declarative configuration. -/
structure PackageConfig extends WorkspaceConfig, LeanConfig where
/-- The `Name` of the package. -/
name : Name
/--
The path of a package's manifest file, which stores the exact versions
of its resolved dependencies.
Defaults to `defaultManifestFile` (i.e., `lake-manifest.json`).
-/
manifestFile := defaultManifestFile
/-- An `Array` of target names to build whenever the package is used. -/
extraDepTargets : Array Name := #[]
/--
Whether to compile each of the package's module into a native shared library
that is loaded whenever the module is imported. This speeds up evaluation of
metaprograms and enables the interpreter to run functions marked `@[extern]`.
Defaults to `false`.
-/
precompileModules : Bool := false
/--
Additional arguments to pass to the Lean language server
(i.e., `lean --server`) launched by `lake server`.
-/
moreServerArgs : Array String := #[]
/--
The directory containing the package's Lean source files.
Defaults to the package's directory.
(This will be passed to `lean` as the `-R` option.)
-/
srcDir : FilePath := "."
/--
The directory to which Lake should output the package's build results.
Defaults to `defaultBuildDir` (i.e., `build`).
-/
buildDir : FilePath := defaultBuildDir
/--
The build subdirectory to which Lake should output the package's
binary Lean libraries (e.g., `.olean`, `.ilean` files).
Defaults to `defaultLeanLibDir` (i.e., `lib`).
-/
leanLibDir : FilePath := defaultLeanLibDir
/--
The build subdirectory to which Lake should output the package's
native libraries (e.g., `.a`, `.so`, `.dll` files).
Defaults to `defaultNativeLibDir` (i.e., `lib`).
-/
nativeLibDir : FilePath := defaultNativeLibDir
/--
The build subdirectory to which Lake should output the package's binary executable.
Defaults to `defaultBinDir` (i.e., `bin`).
-/
binDir : FilePath := defaultBinDir
/--
The build subdirectory to which Lake should output
the package's intermediary results (e.g., `.c` and `.o` files).
Defaults to `defaultIrDir` (i.e., `ir`).
-/
irDir : FilePath := defaultIrDir
/--
The URL of the GitHub repository to upload and download releases of this package.
If `none` (the default), for downloads, Lake uses the URL the package was download
from (if it is a dependency) and for uploads, uses `gh`'s default.
-/
releaseRepo? : Option String := none
/--
The name of the build archive on GitHub. Defaults to `none`.
The archive's full file name will be `nameToArchive buildArchive?`.
-/
buildArchive? : Option String := none
/--
Whether to prefer downloading a prebuilt release (from GitHub) rather than
building this package from the source when this package is used as a dependency.
-/
preferReleaseBuild : Bool := false
deriving Inhabited
--------------------------------------------------------------------------------
/-! # Package -/
--------------------------------------------------------------------------------
abbrev DNameMap α := DRBMap Name α Name.quickCmp
@[inline] def DNameMap.empty : DNameMap α := DRBMap.empty
/-- A Lake package -- its location plus its configuration. -/
structure Package where
/-- The path to the package's directory. -/
dir : FilePath
/-- The package's user-defined configuration. -/
config : PackageConfig
/-- The elaboration environment of the package's configuration file. -/
configEnv : Environment
/-- The Lean `Options` the package configuration was elaborated with. -/
leanOpts : Options
/-- The URL to this package's Git remote. -/
remoteUrl? : Option String := none
/-- The Git tag of this package. -/
gitTag? : Option String := none
/-- (Opaque references to) the package's direct dependencies. -/
opaqueDeps : Array OpaquePackage := #[]
/-- Lean library configurations for the package. -/
leanLibConfigs : NameMap LeanLibConfig := {}
/-- Lean binary executable configurations for the package. -/
leanExeConfigs : NameMap LeanExeConfig := {}
/-- External library targets for the package. -/
externLibConfigs : DNameMap (ExternLibConfig config.name) := {}
/-- (Opaque references to) targets defined in the package. -/
opaqueTargetConfigs : DNameMap (OpaqueTargetConfig config.name) := {}
/--
The names of the package's targets to build by default
(i.e., on a bare `lake build` of the package).
-/
defaultTargets : Array Name := #[]
/-- Scripts for the package. -/
scripts : NameMap Script := {}
/--
The names of the package's scripts run by default
(i.e., on a bare `lake run` of the package).
-/
defaultScripts : Array Script := #[]
instance : Nonempty Package :=
have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance
by refine' ⟨{..}⟩ <;> exact default
hydrate_opaque_type OpaquePackage Package
instance : Hashable Package where hash pkg := hash pkg.config.name
instance : BEq Package where beq p1 p2 := p1.config.name == p2.config.name
abbrev PackageSet := HashSet Package
@[inline] def PackageSet.empty : PackageSet := HashSet.empty
abbrev OrdPackageSet := OrdHashSet Package
@[inline] def OrdPackageSet.empty : OrdPackageSet := OrdHashSet.empty
/-- The package's name. -/
abbrev Package.name (self : Package) : Name :=
self.config.name
/-- A package with a name known at type-level. -/
structure NPackage (name : Name) extends Package where
name_eq : toPackage.name = name
attribute [simp] NPackage.name_eq
instance : CoeOut (NPackage name) Package := ⟨NPackage.toPackage⟩
instance : CoeDep Package pkg (NPackage pkg.name) := ⟨⟨pkg, rfl⟩⟩
/-- The package's name. -/
abbrev NPackage.name (_ : NPackage n) := n
namespace Package
/-- The package's direct dependencies. -/
@[inline] def deps (self : Package) : Array Package :=
self.opaqueDeps.map (·.get)
/--
The directory for storing the package's remote dependencies.
Either its `packagesDir` configuration or `defaultPackagesDir`.
-/
def relPkgsDir (self : Package) : FilePath :=
self.config.packagesDir.getD defaultPackagesDir
/-- The package's `dir` joined with its `relPkgsDir` -/
def pkgsDir (self : Package) : FilePath :=
self.dir / self.relPkgsDir
/-- The package's JSON manifest of remote dependencies. -/
def manifestFile (self : Package) : FilePath :=
self.dir / self.config.manifestFile
/-- The package's `dir` joined with its `buildDir` configuration. -/
@[inline] def buildDir (self : Package) : FilePath :=
self.dir / self.config.buildDir
/-- The package's `extraDepTargets` configuration. -/
@[inline] def extraDepTargets (self : Package) : Array Name :=
self.config.extraDepTargets
/-- The package's `releaseRepo?` configuration. -/
@[inline] def releaseRepo? (self : Package) : Option String :=
self.config.releaseRepo?
/--
The package's URL × tag release.
Tries `releaseRepo?` first and then falls back to `remoteUrl?`.
-/
def release? (self : Package) : Option (String × String) := do
let url ← self.releaseRepo? <|> self.remoteUrl?
let tag ← self.gitTag?
return (url, tag)
/-- The package's `buildArchive?` configuration. -/
@[inline] def buildArchive? (self : Package) : Option String :=
self.config.buildArchive?
/-- The file name of the package's build archive derived from `buildArchive?`. -/
@[inline] def buildArchive (self : Package) : String :=
nameToArchive self.buildArchive?
/-- The package's `buildDir` joined with its `buildArchive` configuration. -/
@[inline] def buildArchiveFile (self : Package) : FilePath :=
self.buildDir / self.buildArchive
/-- The package's `preferReleaseBuild` configuration. -/
@[inline] def preferReleaseBuild (self : Package) : Bool :=
self.config.preferReleaseBuild
/-- The package's `precompileModules` configuration. -/
@[inline] def precompileModules (self : Package) : Bool :=
self.config.precompileModules
/-- The package's `moreServerArgs` configuration. -/
@[inline] def moreServerArgs (self : Package) : Array String :=
self.config.moreServerArgs
/-- The package's `buildType` configuration. -/
@[inline] def buildType (self : Package) : BuildType :=
self.config.buildType
/-- The package's `moreLeanArgs` configuration. -/
@[inline] def moreLeanArgs (self : Package) : Array String :=
self.config.moreLeanArgs
/-- The package's `weakLeanArgs` configuration. -/
@[inline] def weakLeanArgs (self : Package) : Array String :=
self.config.weakLeanArgs
/-- The package's `moreLeancArgs` configuration. -/
@[inline] def moreLeancArgs (self : Package) : Array String :=
self.config.moreLeancArgs
/-- The package's `moreLinkArgs` configuration. -/
@[inline] def moreLinkArgs (self : Package) : Array String :=
self.config.moreLinkArgs
/-- The package's `dir` joined with its `srcDir` configuration. -/
@[inline] def srcDir (self : Package) : FilePath :=
self.dir / self.config.srcDir
/-- The package's root directory for `lean` (i.e., `srcDir`). -/
@[inline] def rootDir (self : Package) : FilePath :=
self.srcDir
/-- The package's `buildDir` joined with its `leanLibDir` configuration. -/
@[inline] def leanLibDir (self : Package) : FilePath :=
self.buildDir / self.config.leanLibDir
/-- The package's `buildDir` joined with its `nativeLibDir` configuration. -/
@[inline] def nativeLibDir (self : Package) : FilePath :=
self.buildDir / self.config.nativeLibDir
/-- The package's `buildDir` joined with its `binDir` configuration. -/
@[inline] def binDir (self : Package) : FilePath :=
self.buildDir / self.config.binDir
/-- The package's `buildDir` joined with its `irDir` configuration. -/
@[inline] def irDir (self : Package) : FilePath :=
self.buildDir / self.config.irDir
/-- Whether the given module is considered local to the package. -/
def isLocalModule (mod : Name) (self : Package) : Bool :=
self.leanLibConfigs.any (fun _ lib => lib.isLocalModule mod)
/-- Whether the given module is in the package (i.e., can build it). -/
def isBuildableModule (mod : Name) (self : Package) : Bool :=
self.leanLibConfigs.any (fun _ lib => lib.isBuildableModule mod) ||
self.leanExeConfigs.any (fun _ exe => exe.root == mod)
/-- Remove the package's build outputs (i.e., delete its build directory). -/
def clean (self : Package) : IO PUnit := do
if (← self.buildDir.pathExists) then
IO.FS.removeDirAll self.buildDir