mathlib3000

Stream: general

[Kevin Buzzard]

buzzard@brutus:~/lean-projects/mathlib$ leanproject get-m
`get-mathlib-cache` is for projects which depend on mathlib, not for mathlib itself. Running `get-cache` instead.
cLooking for mathlib oleans for f178c0e25a
  locally...
  remotely...
ode .
  Found remote mathlib oleans
Using matching cache
  f178c0e25a: 100%|█████████████████████████████████████████████████████████████████████████████████| 83.6M/83.6M [00:23<00:00, 3.77MB/s]
Applying cache
  files extracted: 3000 [00:04, 640.23/s]
buzzard@brutus:~/lean-projects/mathlib$ code .

We have 3000 somethings. olean files perhaps?