leanproject unable to import mathlib

Stream: general

[Vaibhav Karve]

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

[Bryan Gin-ge Chen]

Did leanproject up give an error message?

[Vaibhav Karve]

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

[Bryan Gin-ge Chen]

Ah, that is indeed bad.

[Bryan Gin-ge Chen]

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

[Vaibhav Karve]

Ubuntu

[Vaibhav Karve]

I have tar installed on my OS

[Bryan Gin-ge Chen]

What version of Python are you using?

[Vaibhav Karve]

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)

[Bryan Gin-ge Chen]

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.

[Vaibhav Karve]

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:

[Vaibhav Karve]

!!SOLVED!!