Zulip Chat Archive

Stream: general

Topic: leanproject unable to import mathlib


view this post on Zulip Vaibhav Karve (Nov 10 2020 at 19:06):

I have a mysterious error with leanproject. My editor (emacs) is getting stuck on the import tactic line indefinitely. Can someone help me debug this? So far I have tried leanproject up but it did not fix the issue.

My leanpkg.toml file:

[package]
name = "igl2020"
version = "0.1"
lean_version = "leanprover-community/lean:3.23.0"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "d3fff8a054f671e405ce5dd28ee6f1572e4336db"}

My leanpkg.path file

builtin_path
path _target/deps/mathlib/src
path ./src

view this post on Zulip Bryan Gin-ge Chen (Nov 10 2020 at 19:21):

Did leanproject up give an error message?

view this post on Zulip Vaibhav Karve (Nov 10 2020 at 19:22):

It seems to run a checkout but it ends on the line Unknown archive format '/home/vaibhav/.mathlib/d3fff8a054f671e405ce5dd28ee6f1572e4336db.tar.xz'
I don't know if that's unusual

view this post on Zulip Bryan Gin-ge Chen (Nov 10 2020 at 19:23):

Ah, that is indeed bad.

view this post on Zulip Bryan Gin-ge Chen (Nov 10 2020 at 19:23):

What OS are you using? You'll need a program that can extract tar.xz files.

view this post on Zulip Vaibhav Karve (Nov 10 2020 at 19:23):

Ubuntu

view this post on Zulip Vaibhav Karve (Nov 10 2020 at 19:24):

I have tar installed on my OS

view this post on Zulip Bryan Gin-ge Chen (Nov 10 2020 at 19:24):

What version of Python are you using?

view this post on Zulip Vaibhav Karve (Nov 10 2020 at 19:26):

I just checked and seems that there is some mismatch there. I am on python version 3.8.5 but my pip is on version 20.2.4 (corresponding to python 3.9)

view this post on Zulip Bryan Gin-ge Chen (Nov 10 2020 at 19:29):

I think leanproject uses Python's shutil standard library to extract archives. From my random googling it looks like tar.xz support was added in Python 3.5, so I'm not sure why you're having trouble.

view this post on Zulip Vaibhav Karve (Nov 10 2020 at 19:40):

Thanks for your help Bryan. I solved it -- though it is not clear to me what the issue was.

  1. I deleted the ~/.mathlib directory that leanproject was having trouble reading the tar.xz file from
  2. I reinstalled mathlibtools using pip
  3. I ran leanproject up. This time the error about the tar file did not show up.
  4. Editor is now reading/importing file correctly. Problem solved :smile:

view this post on Zulip Vaibhav Karve (Nov 10 2020 at 19:41):

!!SOLVED!!


Last updated: May 11 2021 at 12:15 UTC