Zulip Chat Archive

Stream: general

Topic: leanupdate cant install olean files

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):

xz-utils?

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.

shutil.get_archive_formats()

Doesn't include xztar, and

import lzma

is an error.

Last updated: Dec 20 2023 at 11:08 UTC