You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Downloads artifacts for packages in the workspace from a remote cache service to the local Lake {tech (key:="local cache")}[artifact cache].
1174
-
The remote cache service used can be configured using {envVar}`LAKE_CACHE_ARTIFACT_ENDPOINT` and {envVar}`LAKE_CACHE_REVISION_ENDPOINT`.
1175
-
If neither of these are set, Lake will use Reservoir instead.
1176
-
The variable {envVar}`LAKE_CACHE_SERVICE` can be used to provide an identifier to be recorded in outputs.
1171
+
The cache service used can be specified via the {lakeOpt}`--service` option.
1172
+
Otherwise, Lake will use the system default, or, if none is configured, Reservoir.
1173
+
See {lake}`cache services` for more information on how to configure services.
1177
1174
1178
1175
If an input-to-outputs {lakeMeta}`mappings` file, a {lakeMeta}`remote-scope`, or a {lakeMeta}`github-repo` is provided, Lake will download artifacts for the root package.
1179
1176
Otherwise, it will download artifacts for each package in the root's dependency tree in order (using Reservoir).
@@ -1202,18 +1199,17 @@ USAGE:
1202
1199
1203
1200
Uploads the input-to-outputs mappings contained in the specified file along
1204
1201
with the corresponding output artifacts to a remote cache. The cache service
1205
-
used is configured via the environment variables:
1206
-
1207
-
LAKE_CACHE_KEY authentication key for requests
1208
-
LAKE_CACHE_ARTIFACT_ENDPOINT base URL for artifact uploads
1209
-
LAKE_CACHE_REVISION_ENDPOINT base URL for the mapping upload
1202
+
used via be specified via `--service` option. If not specifed, Lake will used
1203
+
the system default, or error if none is configured. See `lake cache services`
1204
+
for more information on how to configure services.
1210
1205
1211
1206
Files are uploaded using the AWS Signature Version 4 authentication protocol
1212
-
via `curl`. Thus, the service should generally be an S3-compatible bucket.
1207
+
via `curl`. Thus, the service should generally be an S3-compatible bucket. The
1208
+
authentication key is set via the `LAKE_CACHE_KEY` environment variable.
1213
1209
1214
1210
Since Lake does not currently use cryptographically secure hashes for
1215
1211
artifacts and outputs, uploads to the cache are prefixed with a scope to avoid
1216
-
clashes. This scoped is configured with the following options:
1212
+
clashes. This scope is configured with the following options:
1217
1213
1218
1214
--scope=<remote-scope> sets a fixed scope
1219
1215
--repo=<github-repo> uses the repository + toolchain & platform
@@ -1235,9 +1231,13 @@ has changes.
1235
1231
1236
1232
::::lake cache put "mappings «scope-option»"
1237
1233
Uploads the input-to-outputs mappings contained in the specified file along with the corresponding output artifacts to a remote cache.
1238
-
The remote cache service used can be configured using {envVar}`LAKE_CACHE_KEY`, {envVar}`LAKE_CACHE_ARTIFACT_ENDPOINT` and {envVar}`LAKE_CACHE_REVISION_ENDPOINT`.
1234
+
The cache service used can be specified via the {lakeOpt}`--service` option.
1235
+
If not specified, Lake will use the system default, or error if none is configured.
1236
+
See {lake}`cache services` for more information on how to configure services.
1239
1237
1240
-
Files are uploaded using the AWS Signature Version 4 authentication protocol via `curl`. Thus, the service should generally be an S3-compatible bucket.
1238
+
Files are uploaded using the AWS Signature Version 4 authentication protocol via `curl`.
1239
+
Thus, the service should generally be an S3-compatible bucket.
1240
+
The authentication key is set via the {envVar}`LAKE_CACHE_KEY` environment variable.
1241
1241
1242
1242
Since Lake does not currently use cryptographically secure hashes for
1243
1243
artifacts and outputs, uploads to the cache are prefixed with a scope to avoid
@@ -1284,6 +1284,51 @@ If a workspace configuration exists, this will delete the cache directory it use
1284
1284
Otherwise, it will delete the default Lake cache directory for the system.
1285
1285
:::
1286
1286
1287
+
```lakeCacheHelp services
1288
+
Print configured remote cache services
1289
+
1290
+
USAGE:
1291
+
lake cache services
1292
+
1293
+
Prints the name of each configured remote cache services (one per line).
1294
+
Additional services can be added by modifying the system Lake configuration.
1295
+
The exact location of the this configuration file is system dependent and can
1296
+
be set by `LAKE_CONFIG`, but it is usually located at `~/.lake/config.toml`.
1297
+
1298
+
The configuration of the system cache could look something like the following:
1299
+
1300
+
cache.defaultService = "my-s3"
1301
+
cache.defaultUploadService = "my-s3"
1302
+
1303
+
[[cache.service]]
1304
+
name = "my-s3"
1305
+
kind = "s3"
1306
+
artifactEndpoint = "https://my-s3.com/a0"
1307
+
revisionEndpoint = "https://my-s3.com/r0"
1308
+
1309
+
If no `cache.defaultService` is configured, Lake will use Reservoir by default.
1310
+
```
1311
+
1312
+
::::lake cache services
1313
+
Prints the name of each configured remote cache service (one per line).
1314
+
Additional services can be added by modifying the system Lake configuration file, which is usually located at `~/.lake/config.toml` but can be set via the {envVar}`LAKE_CONFIG` environment variable.
1315
+
1316
+
:::paragraph
1317
+
The configuration of the system cache could look something like the following:
1318
+
```toml -link
1319
+
cache.defaultService = "my-s3"
1320
+
cache.defaultUploadService = "my-s3"
1321
+
1322
+
[[cache.service]]
1323
+
name = "my-s3"
1324
+
kind = "s3"
1325
+
artifactEndpoint = "https://my-s3.com/a0"
1326
+
revisionEndpoint = "https://my-s3.com/r0"
1327
+
```
1328
+
If no `cache.defaultService` is configured, Lake will use Reservoir by default.
Copy file name to clipboardExpand all lines: Manual/Language/InductiveTypes/Structures.lean
+46-12Lines changed: 46 additions & 12 deletions
Original file line number
Diff line number
Diff line change
@@ -65,29 +65,63 @@ tag := "structure-fields"
65
65
%%%
66
66
67
67
Each field of a structuredeclarationcorrespondstoaparameteroftheconstructor.
68
+
69
+
::::example"Inferring Universes"
70
+
71
+
The structure {lean}`MyProd`isthesameas {lean}`Prod`.
72
+
```lean
73
+
structureMyProd (α β : Type _) where
74
+
fst : α
75
+
snd : β
76
+
```
77
+
The two parameters and the two fields are constructor parameters:
78
+
```signature
79
+
MyProd.mk.{u, v}
80
+
{α : Type u}
81
+
{β : Type v}
82
+
(fst : α)
83
+
(snd : β)
84
+
: MyProd.{u, v} α β
85
+
```
86
+
Additionally, the constructor is {tech (key := "universe polymorphism")}[universe polymorphic]; the type constructor {name}`MyProd` takes two universe parameters:
87
+
```signature
88
+
MyProd.{u, v} (α : Type u) (β : Type v) : Type (max u v)
89
+
```
90
+
91
+
```lean -show
92
+
universe u v
93
+
```
94
+
The universe level of each type of each field must be less than or equal to the universe level of the structure.
95
+
Lean infers that {lean}`Type (max u v)` is the least universe that can accommodate both {lean}`Type u` and {lean}`Type v`.
96
+
97
+
::::
98
+
68
99
Auto-implicit arguments are inserted in each field separately, even if their names coincide, and the fields become constructor parameters that quantify over types.
69
100
70
-
::::example"Auto-implicit parameters in structure fields"
101
+
::::example"Auto-Implicit Parameters in Structure Fields"
71
102
72
-
The structure {lean}`MyStructure`containsafieldwhosetypeisanauto-implicitparameter:
103
+
The structure {lean}`MyStructure`containsfieldswhosetypeshaveauto-implicitparameters:
73
104
74
105
```lean
75
106
structureMyStructurewhere
76
-
field1 : α
77
-
field2 : α
107
+
field1 : Fin n
108
+
field2 : Fin n
109
+
```
110
+
```lean -show
111
+
variable {n : Nat}
78
112
```
79
-
The type constructor {name}`MyStructure` takes two universe parameters:
113
+
Each fields in the constructor {name}`MyStructure.mk` takes its own implicit parameter {lean}`n` of type {lean}`Nat`:
80
114
```signature
81
-
MyStructure.{u, v} : Type (max u v)
115
+
MyStructure.mk
116
+
(field1 : {n : Nat} → Fin n)
117
+
(field2 : {n : Nat} → Fin n)
118
+
: MyStructure
82
119
```
83
-
The resulting type is in `Type` rather than `Sort` because the constructor fields quantify over types in `Sort`. In particular, both fields in its constructor {name}`MyStructure.mk` take an implicit type parameter:
120
+
The type constructor {name}`MyStructure` takes no universe parameters, and the resulting type is in `Type`,
121
+
which is the universefor {name}`Nat` and {lean}`Fin n`:
0 commit comments