Zulip Chat Archive

Stream: general

Topic: leanproject unable to import mathlib


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

Bryan Gin-ge Chen (Nov 10 2020 at 19:21):

Did leanproject up give an error message?

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

Bryan Gin-ge Chen (Nov 10 2020 at 19:23):

Ah, that is indeed bad.

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.

Vaibhav Karve (Nov 10 2020 at 19:23):

Ubuntu

Vaibhav Karve (Nov 10 2020 at 19:24):

I have tar installed on my OS

Bryan Gin-ge Chen (Nov 10 2020 at 19:24):

What version of Python are you using?

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)

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.

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:

Vaibhav Karve (Nov 10 2020 at 19:41):

!!SOLVED!!


Last updated: Dec 20 2023 at 11:08 UTC