Noam Atar (Jun 27 2020 at 14:59):
When I run
leanproject up I get the following error:
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/ Something wrong happened with the olean archive. I will now retry downloading. Looking for remote mathlib oleans Trying to download https://oleanstorage.azureedge.net/mathlib/e7e9f30cd2c79a125322baf4cef4a49d94bf6119.tar.xz to /home/noam/.mathlib/e7e9f30cd2c79a125322baf4cef4a49d94bf6119.tar.xz 100%|█████████████████████████████████████| 23.5M/23.5M [00:11<00:00, 2.11MiB/s] Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/ Unknown archive format '/home/noam/.mathlib/e7e9f30cd2c79a125322baf4cef4a49d94bf6119.tar.xz'
I am on Ubuntu and have tar installed, so I don't know why this happens.
Jiekai (Jun 27 2020 at 15:08):
Shing Tak Lam (Jun 27 2020 at 15:14):
I think we've probably figured out why on Discord. I think this is an issue with the Python installation, not leanproject. However I don't know how to fix it since I'm not on Ubuntu.
is an error.
Last updated: May 09 2021 at 19:11 UTC