chore: update stage0

stage0/stdlib/Init/Data/String/Slice.c

@@ -3855,16 +3855,16 @@ block_18:
 {
 if (x_15 == 0)
 {
-x_5 = x_14;
-x_6 = x_13;
+x_5 = x_13;
+x_6 = x_14;
 goto block_12;
 }
 else
 {
 uint8_t x_16; uint8_t x_17; 
 x_16 = 32;
-x_17 = lean_uint8_add(x_13, x_16);
-x_5 = x_14;
+x_17 = lean_uint8_add(x_14, x_16);
+x_5 = x_13;
 x_6 = x_17;
 goto block_12;
 }
@@ -3880,8 +3880,8 @@ x_24 = 65;
 x_25 = lean_uint8_dec_le(x_24, x_23);
 if (x_25 == 0)
 {
-x_13 = x_23;
-x_14 = x_19;
+x_13 = x_19;
+x_14 = x_23;
 x_15 = x_25;
 goto block_18;
 }
@@ -3890,8 +3890,8 @@ else
 uint8_t x_26; uint8_t x_27; 
 x_26 = 90;
 x_27 = lean_uint8_dec_le(x_23, x_26);
-x_13 = x_23;
-x_14 = x_19;
+x_13 = x_19;
+x_14 = x_23;
 x_15 = x_27;
 goto block_18;
 }

stage0/stdlib/Lake/CLI/Help.c

@@ -403,7 +403,7 @@ static lean_object* _init_l___private_Lake_CLI_Help_0__Lake_helpCacheGet___close
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_unchecked("Download artifacts from a remote service into the Lake cache\n\nUSAGE:\n  lake cache get [<mappings>] [--scope=<remote-scope>] [--max-revs=<n>]\n\nDownloads artifacts for packages in the workspace from a remote cache service.\nThe cache service used can be configured via the environment variables:\n\n  LAKE_CACHE_ARTIFACT_ENDPOINT  base URL for artifact downloads\n  LAKE_CACHE_REVISION_ENDPOINT  base URL for the mapping download\n\nIf neither of these are set, Lake will use Reservoir instead.\n\nIf an input-to-outputs mappings file or a scope is provided, Lake will\ndownload artifacts for the root package. Otherwise, it will download artifacts\nfor each package in the root's dependency tree in order (using Reservoir).\nNon-Reservoir dependencies will be skipped.\n\nTo determine the artifacts to download, Lake uses the package's Git revision\n(commit hash) to lookup its input-to-outputs mappings on the cache service.\nLake will download the artifacts for the most recent commit with available\nmappings. It will backtrack up to `--max-revs`, which defaults to 100.\nIf set to 0, Lake will search the repository's whole history.\n\nWhile downloading, Lake will continue on when a download for an artifact\nfails or if the download process for a whole package fails. However, it will\nreport this and exit with a nonzero status code in such cases.", 1332, 1332);
+x_1 = lean_mk_string_unchecked("Download artifacts from a remote service into the Lake cache\n\nUSAGE:\n  lake cache get [<mappings>]\n\nOPTIONS:\n  --max-revs=<n>                  backtrack up to n revisions (default: 100)\n  --rev=<commit-hash>             uses this exact revision to lookup artifacts\n  --repo=<github-repo>            GitHub repository of the package or a fork\n  --platform=<target-triple>      with Reservoir or --repo, sets the platform\n  --toolchain=<name>              with Reservoir or --repo, sets the toolchain\n  --scope=<remote-scope>          scope for a custom endpoint\n\nDownloads artifacts for packages in the workspace from a remote cache service.\nThe cache service used can be configured via the environment variables:\n\n  LAKE_CACHE_ARTIFACT_ENDPOINT  base URL for artifact downloads\n  LAKE_CACHE_REVISION_ENDPOINT  base URL for the mapping download\n\nIf neither of these are set, Lake will use Reservoir.\n\nIf an input-to-outputs mappings file, `--scope`, or `--repo` is provided,\nLake will download artifacts for the root package. Otherwise, it will use\nReservoir to download artifacts for each dependency in workspace (in order).\nNon-Reservoir dependencies will be skipped.\n\nTo determine the artifacts to download, Lake searches for input-to-output\nmappings for a given build of the package via the cache service. This mapping\nis identified by a Git revision and prefixed with a scope derived from the\npackage's name, GitHub repository, Lean toolchain, and current platform.\nThe exact configuration can be customized using options.\n\nFor Reservoir, setting `--repo` will make Lake lookup artifacts for the root\npackage by a repository name, rather than the package's. This can be used to\ndownload artifacts for a fork of the Reservoir package (if such artifacts are\navailable). The `--platform` and `--toolchain` options can be used to download\nartifacts for a different platform/toolchain configuration than Lake detects.\nFor a custom endpoint, the full prefix Lake uses can be set via  `--scope`.\n\nIf `--rev` is not set, Lake uses the package's current revision to lookup\nartifacts. If no mappings are found, Lake will backtrack the Git history up to\n`--max-revs`, looking for a revision with mappings. If `--max-revs` is 0, Lake\nwill search the repository's entire history (or as far as Git will allow).\n\nIf a download for an artifact fails or the download process for a whole\npackage fails, Lake will report this and continue on to the next. Once done,\nif any download failed, Lake will exit with a nonzero status code.", 2517, 2517);
 return x_1;
 }
 }
@@ -419,7 +419,7 @@ static lean_object* _init_l___private_Lake_CLI_Help_0__Lake_helpCachePut___close
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_unchecked("Upload artifacts from the Lake cache to a remote service\n\nUSAGE:\n  lake cache put <mappings> --scope=<remote-scope>\n\nUploads the input-to-outputs mappings contained in the specified file along\nwith the corresponding output artifacts to a remote cache. The cache service\nused is configured via the environment variables:\n\n  LAKE_CACHE_KEY                authentication key for requests\n  LAKE_CACHE_ARTIFACT_ENDPOINT  base URL for artifact uploads\n  LAKE_CACHE_REVISION_ENDPOINT  base URL for the mapping upload\n\nFiles are uploaded using the AWS Signature Version 4 authentication protocol\nvia `curl`. Thus, the service should generally be an S3-compatible bucket.\n\nArtifacts are uploaded to the artifact endpoint under the prefix `scope`\nwith a file name corresponding to their Lake content hash. The mappings file\nis uploaded  to the revision endpoint under the prefix `scope` with a file name\ncorresponding to the package's current Git revision. As such, the command will\nfail if the the work tree currently has changes.", 1022, 1022);
+x_1 = lean_mk_string_unchecked("Upload artifacts from the Lake cache to a remote service\n\nUSAGE:\n  lake cache put <mappings> <scope-option>\n\nUploads the input-to-outputs mappings contained in the specified file along\nwith the corresponding output artifacts to a remote cache. The cache service\nused is configured via the environment variables:\n\n  LAKE_CACHE_KEY                  authentication key for requests\n  LAKE_CACHE_ARTIFACT_ENDPOINT    base URL for artifact uploads\n  LAKE_CACHE_REVISION_ENDPOINT    base URL for the mapping upload\n\nFiles are uploaded using the AWS Signature Version 4 authentication protocol\nvia `curl`. Thus, the service should generally be an S3-compatible bucket.\n\nSince Lake does not currently use cryptographically secure hashes for\nartifacts and outputs, uploads to the cache are prefixed with a scope to avoid\nclashes. This scoped is configured with the following options:\n\n  --scope=<remote-scope>          sets a fixed scope\n  --repo=<github-repo>            uses the repository + toolchain & platform\n  --toolchain=<name>              with --repo, sets the toolchain\n  --platform=<target-triple>      with --repo, sets the platform\n\nAt least one of `--scope` or `--repo` must be set. If `--repo` is used, Lake\nwill produce a scope by augmenting the repository with toolchain and platform\ninformation as it deems necessary. If `--scope` is set, Lake will use the\nspecified scope verbatim.\n\nArtifacts are uploaded to the artifact endpoint with a file name derived\nfrom their Lake content hash (and prefixed by the repository or scope).\nThe mappings file is uploaded to the revision endpoint with a file name\nderived from the package's current Git revision (and prefixed by the\nfull scope). As such, the command will warn if the the work tree currently\nhas changes.", 1767, 1767);
 return x_1;
 }
 }

stage0/stdlib/Lake/Config/Package.c

@@ -68,6 +68,7 @@ LEAN_EXPORT lean_object* l___private_Lake_Config_Package_0__Lake_OpaquePostUpdat
 lean_object* l_Id_instMonad___lam__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_utf8_byte_size(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_instToStringPackage;
+static lean_object* l_Lake_Package_isPlatformIndependent___closed__1;
 LEAN_EXPORT lean_object* l_Lake_Package_rootDir(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_preferReleaseBuild___boxed(lean_object*);
 static lean_object* l_Lake_Package_relLicenseFiles___closed__4;
@@ -77,6 +78,7 @@ LEAN_EXPORT lean_object* l_Lake_Package_findTargetDecl_x3f(lean_object*, lean_ob
 LEAN_EXPORT lean_object* l_Lake_instBEqPackage___lam__0___boxed(lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lake_Package_isLocalModule(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_lintDriverArgs___boxed(lean_object*);
+static lean_object* l_Lake_Package_isPlatformIndependent___closed__0;
 static lean_object* l_Lake_instInhabitedPackage_default___closed__1;
 static lean_object* l_Lake_OrdPackageSet_empty___closed__2;
 LEAN_EXPORT lean_object* l_Lake_PostUpdateHook_ctorIdx(lean_object*, lean_object*);
@@ -123,6 +125,7 @@ LEAN_EXPORT lean_object* l_Lake_instInhabitedPostUpdateHook_default___lam__0___b
 LEAN_EXPORT lean_object* l_Lake_Package_releaseRepo_x3f___boxed(lean_object*);
 static lean_object* l_Lake_PackageSet_empty___closed__3;
 static lean_object* l_Lake_instImpl___closed__2____x40_Lake_Config_Package_1275829001____hygCtx___hyg_26_;
+lean_object* l_instDecidableEqBool___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_reservoir___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_PackageSet_empty;
 LEAN_EXPORT lean_object* l_Lake_instHashablePackage;
@@ -130,6 +133,7 @@ LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___
 lean_object* l_IO_FS_removeDirAll(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_extraDepTargets___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_testDriverArgs___boxed(lean_object*);
+lean_object* l_instBEqOfDecidableEq___redArg(lean_object*);
 static lean_object* l_Lake_instInhabitedPackage_default___closed__0;
 LEAN_EXPORT lean_object* l_Lake_Package_binDir(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_PostUpdateHook_ctorIdx___boxed(lean_object*, lean_object*);
@@ -195,6 +199,7 @@ LEAN_EXPORT lean_object* l_Lake_Package_ctorIdx___boxed(lean_object*);
 static lean_object* l_Lake_Package_relLicenseFiles___closed__8;
 lean_object* lean_nat_mul(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lake_instToJsonPackage;
+LEAN_EXPORT lean_object* l_Lake_Package_isPlatformIndependent___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_findTargetDecl_x3f___boxed(lean_object*, lean_object*);
 lean_object* l_Nat_nextPowerOfTwo(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_restoreAllArtifacts___boxed(lean_object*);
@@ -215,6 +220,7 @@ size_t lean_array_size(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_OpaquePostUpdateHook_instInhabitedOfPostUpdateHook___redArg___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_buildType___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Package_weakLeancArgs(lean_object*);
+uint8_t l_Option_instBEq_beq___redArg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_mkStr1(lean_object*);
 LEAN_EXPORT uint8_t l_Lake_Package_buildType(lean_object*);
 LEAN_EXPORT lean_object* l_Lake_instInhabitedPostUpdateHook(lean_object*);
@@ -244,6 +250,7 @@ static lean_object* l_Lake_PackageSet_empty___closed__4;
 LEAN_EXPORT lean_object* l_Lake_Package_bootstrap___boxed(lean_object*);
 lean_object* l_Id_instMonad___lam__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lake_Config_Package_0__Lake_OpaquePostUpdateHook_unsafeGet(lean_object*, lean_object*);
+LEAN_EXPORT uint8_t l_Lake_Package_isPlatformIndependent(lean_object*);
 static lean_object* l_Lake_Package_licenseFiles___closed__0;
 static lean_object* l_Lake_PackageSet_empty___closed__1;
 static lean_object* l_Lake_Package_relLicenseFiles___closed__9;
@@ -1412,6 +1419,54 @@ lean_dec_ref(x_1);
 return x_2;
 }
 }
+static lean_object* _init_l_Lake_Package_isPlatformIndependent___closed__0() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_alloc_closure((void*)(l_instDecidableEqBool___boxed), 2, 0);
+x_2 = l_instBEqOfDecidableEq___redArg(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lake_Package_isPlatformIndependent___closed__1() {
+_start:
+{
+uint8_t x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = 1;
+x_2 = lean_box(x_1);
+x_3 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_3, 0, x_2);
+return x_3;
+}
+}
+LEAN_EXPORT uint8_t l_Lake_Package_isPlatformIndependent(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; 
+x_2 = lean_ctor_get(x_1, 4);
+lean_inc_ref(x_2);
+lean_dec_ref(x_1);
+x_3 = lean_ctor_get(x_2, 1);
+lean_inc_ref(x_3);
+lean_dec_ref(x_2);
+x_4 = lean_ctor_get(x_3, 10);
+lean_inc(x_4);
+lean_dec_ref(x_3);
+x_5 = l_Lake_Package_isPlatformIndependent___closed__0;
+x_6 = l_Lake_Package_isPlatformIndependent___closed__1;
+x_7 = l_Option_instBEq_beq___redArg(x_5, x_4, x_6);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lake_Package_isPlatformIndependent___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lake_Package_isPlatformIndependent(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
 LEAN_EXPORT lean_object* l_Lake_Package_releaseRepo_x3f(lean_object* x_1) {
 _start:
 {
@@ -2649,6 +2704,10 @@ l_Lake_Package_licenseFiles___closed__0 = _init_l_Lake_Package_licenseFiles___cl
 lean_mark_persistent(l_Lake_Package_licenseFiles___closed__0);
 l_Lake_Package_relLakeDir___closed__0 = _init_l_Lake_Package_relLakeDir___closed__0();
 lean_mark_persistent(l_Lake_Package_relLakeDir___closed__0);
+l_Lake_Package_isPlatformIndependent___closed__0 = _init_l_Lake_Package_isPlatformIndependent___closed__0();
+lean_mark_persistent(l_Lake_Package_isPlatformIndependent___closed__0);
+l_Lake_Package_isPlatformIndependent___closed__1 = _init_l_Lake_Package_isPlatformIndependent___closed__1();
+lean_mark_persistent(l_Lake_Package_isPlatformIndependent___closed__1);
 l_Lake_Package_barrelFile___closed__0 = _init_l_Lake_Package_barrelFile___closed__0();
 lean_mark_persistent(l_Lake_Package_barrelFile___closed__0);
 l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___Lake_Package_isLocalModule_spec__0___closed__0 = _init_l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___Lake_Package_isLocalModule_spec__0___closed__0();

stage0/stdlib/Lake/Reservoir.c

@@ -158,7 +158,7 @@ LEAN_EXPORT lean_object* l_Lake_RegistrySrc_instToJson;
 LEAN_EXPORT lean_object* l_Lake_RegistrySrc_ctorElim(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lake_RegistrySrc_ctorIdx(lean_object*);
 lean_object* l_Option_fromJson_x3f___redArg(lean_object*, lean_object*);
-lean_object* l_Lake_uriEncode(lean_object*);
+lean_object* l_Lake_uriEncode(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lake_ReservoirResp_data_elim(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Json_getNat_x3f(lean_object*);
 LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Array_fromJson_x3f___at___Option_fromJson_x3f___at___Lake_RegistryPkg_fromJson_x3f_spec__1_spec__1_spec__1(size_t, size_t, lean_object*);
@@ -2721,21 +2721,22 @@ return x_1;
 LEAN_EXPORT lean_object* l_Lake_Reservoir_pkgApiUrl(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
 x_4 = lean_ctor_get(x_1, 3);
 lean_inc_ref(x_4);
 lean_dec_ref(x_1);
 x_5 = l_Lake_Reservoir_pkgApiUrl___closed__0;
 x_6 = lean_string_append(x_4, x_5);
-x_7 = l_Lake_uriEncode(x_2);
-x_8 = lean_string_append(x_6, x_7);
-lean_dec_ref(x_7);
-x_9 = l_Lake_Reservoir_pkgApiUrl___closed__1;
-x_10 = lean_string_append(x_8, x_9);
-x_11 = l_Lake_uriEncode(x_3);
-x_12 = lean_string_append(x_10, x_11);
-lean_dec_ref(x_11);
-return x_12;
+x_7 = l_Lake_instInhabitedRegistrySrc_default___closed__0;
+x_8 = l_Lake_uriEncode(x_2, x_7);
+x_9 = lean_string_append(x_6, x_8);
+lean_dec_ref(x_8);
+x_10 = l_Lake_Reservoir_pkgApiUrl___closed__1;
+x_11 = lean_string_append(x_9, x_10);
+x_12 = l_Lake_uriEncode(x_3, x_7);
+x_13 = lean_string_append(x_11, x_12);
+lean_dec_ref(x_12);
+return x_13;
 }
 }
 LEAN_EXPORT lean_object* l_Lake_Reservoir_pkgApiUrl___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@@ -4521,23 +4522,24 @@ return x_1;
 LEAN_EXPORT lean_object* l_Lake_Reservoir_pkgVersionsApiUrl(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
 x_4 = lean_ctor_get(x_1, 3);
 lean_inc_ref(x_4);
 lean_dec_ref(x_1);
 x_5 = l_Lake_Reservoir_pkgApiUrl___closed__0;
 x_6 = lean_string_append(x_4, x_5);
-x_7 = l_Lake_uriEncode(x_2);
-x_8 = lean_string_append(x_6, x_7);
-lean_dec_ref(x_7);
-x_9 = l_Lake_Reservoir_pkgApiUrl___closed__1;
-x_10 = lean_string_append(x_8, x_9);
-x_11 = l_Lake_uriEncode(x_3);
-x_12 = lean_string_append(x_10, x_11);
-lean_dec_ref(x_11);
-x_13 = l_Lake_Reservoir_pkgVersionsApiUrl___closed__0;
-x_14 = lean_string_append(x_12, x_13);
-return x_14;
+x_7 = l_Lake_instInhabitedRegistrySrc_default___closed__0;
+x_8 = l_Lake_uriEncode(x_2, x_7);
+x_9 = lean_string_append(x_6, x_8);
+lean_dec_ref(x_8);
+x_10 = l_Lake_Reservoir_pkgApiUrl___closed__1;
+x_11 = lean_string_append(x_9, x_10);
+x_12 = l_Lake_uriEncode(x_3, x_7);
+x_13 = lean_string_append(x_11, x_12);
+lean_dec_ref(x_12);
+x_14 = l_Lake_Reservoir_pkgVersionsApiUrl___closed__0;
+x_15 = lean_string_append(x_13, x_14);
+return x_15;
 }
 }
 LEAN_EXPORT lean_object* l_Lake_Reservoir_pkgVersionsApiUrl___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {