Skip to content

Commit 23f46b2

Browse files
committed
doc(Cache): mention arguments to cache lookup help (leanprover-community#21701)
Further, fix docstring refering to `Lean.versionString` even though `Lean.gitHash` is used, and fix a Zulip link.
1 parent 3706323 commit 23f46b2

File tree

3 files changed

+13
-13
lines changed

3 files changed

+13
-13
lines changed

Cache/Hashing.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -60,9 +60,9 @@ Computes the root hash, which mixes the hashes of the content of:
6060
* `lakefile.lean`
6161
* `lean-toolchain`
6262
* `lake-manifest.json`
63-
and the hash of `Lean.versionString`.
63+
and the hash of `Lean.gitHash`.
6464
65-
(We hash `Lean.versionString` in case the toolchain changes even though `lean-toolchain` hasn't.
65+
(We hash `Lean.gitHash` in case the toolchain changes even though `lean-toolchain` hasn't.
6666
This happens with the `lean-pr-testing-NNNN` toolchains when Lean 4 PRs are updated.)
6767
-/
6868
def getRootHash : CacheM UInt64 := do

Cache/Main.lean

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -11,16 +11,16 @@ Usage: cache [COMMAND]
1111
1212
Commands:
1313
# No privilege required
14-
get [ARGS] Download linked files missing on the local cache and decompress
15-
get! [ARGS] Download all linked files and decompress
16-
get- [ARGS] Download linked files missing to the local cache, but do not decompress
17-
pack Compress non-compressed build files into the local cache
18-
pack! Compress build files into the local cache (no skipping)
19-
unpack Decompress linked already downloaded files
20-
unpack! Decompress linked already downloaded files (no skipping)
21-
clean Delete non-linked files
22-
clean! Delete everything on the local cache
23-
lookup Show information about cache files for the given lean files
14+
get [ARGS] Download linked files missing on the local cache and decompress
15+
get! [ARGS] Download all linked files and decompress
16+
get- [ARGS] Download linked files missing to the local cache, but do not decompress
17+
pack Compress non-compressed build files into the local cache
18+
pack! Compress build files into the local cache (no skipping)
19+
unpack Decompress linked already downloaded files
20+
unpack! Decompress linked already downloaded files (no skipping)
21+
clean Delete non-linked files
22+
clean! Delete everything on the local cache
23+
lookup [ARGS] Show information about cache files for the given lean files
2424
2525
# Privilege required
2626
put Run 'mk' then upload linked files missing on the server

Cache/Requests.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import Cache.Hashing
88

99
namespace Cache.Requests
1010

11-
-- FRO cache is flaky so disable until we work out the kinks: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
11+
-- FRO cache is flaky so disable until we work out the kinks: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
1212
def useFROCache : Bool := false
1313

1414
/-- Public URL for mathlib cache -/

0 commit comments

Comments
 (0)