leanpkg does not work

Stream: general

[Blair Shi]

after git clone Xena-UROP-2018 from GitHub, I want to do leanpkg upgrade but it failed and post many error:

/usr/local/leanpkg/leanpkg/main.lean:1:0: error: file 'init' not found in the LEAN_PATH /usr/local/leanpkg/leanpkg/resolve.lean:1:0: error: file 'init' not found in the LEAN_PATH /usr/local/leanpkg/leanpkg/manifest.lean:1:0: error: file 'init' not found in the LEAN_PATH /usr/local/leanpkg/leanpkg/toml.lean:1:0: error: file 'init' not found in the LEAN_PATH

I don't know how to do.

[Kevin Buzzard]

Which OS?

[Kevin Buzzard]

Are you using the command line? What's the output of lean --version?

[Blair Shi]

it gives me Lean (version 3.4.1, commit 17fe3decaf8a, Release)

[Blair Shi]

I run this on Mac

[Sebastian Ullrich]

How did you install Lean?

[Kevin Buzzard]

If you type leanpkg, what is the first line of the output? I have files with the same names as those which are giving you errors, in my unix install, but there is no mention of init. It's certainly possible to get it all working on a mac.

[Sebastian Ullrich]

@Blair Shi

[Blair Shi]

Macos high Sierra 10.13.2

[Blair Shi]

@Kevin Buzzard

dyn3159-100:xena-UROP-2018 shifengzheng$ leanpkg
/usr/local/leanpkg/leanpkg/main.lean:1:0: error: file 'init' not found in the LEAN_PATH

[Blair Shi]

@Sebastian Ullrich I just downloaded the package lean-3.4.1 and then in my vscode I set
"lean.executablePath": "/Users/shifengzheng/lean-3.4.1-darwin/bin/lean",

[Sebastian Ullrich]

@Blair Shi Why do you have files in /usr/local/ then? Do you have an old Homebrew installation or something like that?

[Kevin Buzzard]

@Blair Shi @Blair Shi (wait -- there are two?) the error shows that the version of leanpkg which is running is not the one in Users/shifengzheng/lean-3.4.1-darwin/bin/, it is some other version installed in usr/local. You might want to completely remove the /usr/local/leanpkg directory and add Users/shifengzheng/lean-3.4.1-darwin/bin/ to the path on your command line

[Blair Shi]

@Sebastian Ullrich before I did not have leanpkgin my /usr/local/ but when I typed leanpkg in terminal, it reported <unknown>:1:1: error: file '/usr/local/leanpkg/leanpkg/main.lean' not found. So I put leanpkg into my /usr/local/

[Kevin Buzzard]

I don't think you can just move leanpkg and hope for things to still work

[Kevin Buzzard]

I think you have to move the entire installation

[Kevin Buzzard]

What I'm saying is that you can move the directory /Users/shifengzheng/lean-3.4.1-darwin to anywhere you like

[Kevin Buzzard]

but you should leave the contents intact.

[Kevin Buzzard]

When you've decided where to put it, point VS Code and your command line PATH to it, and then things should be OK.

[Blair Shi]

I moved lean-3.4.1-darwin to /usr/local/ and added path to LEAN_PATH and removed the previous leanpkgin local

dyn3159-100:xena-UROP-2018 shifengzheng$ echo $LEAN_PATH
/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/usr/local/lean-3.4.1-darwin/bin/

But stil not work.

dyn3159-100:xena-UROP-2018 shifengzheng$ leanpkg
<unknown>:1:1: error: file '/usr/local/leanpkg/leanpkg/main.lean' not found

Did I set the wrong path or did I miss to do something?

[Sebastian Ullrich]

Kevin said to modify PATH, not LEAN_PATH. Please unset LEAN_PATH.

[Sebastian Ullrich]

Could you post the output of which leanpkg and bash -x leanpkg?

[Blair Shi]

@Sebastian Ullrich sorry for my misunderstanding. I unset LEAN_PATH and did what you said

dyn3159-100:xena-UROP-2018 shifengzheng$ which leanpkg
/usr/local/bin/leanpkg
dyn3159-100:xena-UROP-2018 shifengzheng$ bash -x leanpkg
++ uname
+ unamestr=Darwin
+ [[ Darwin == \D\a\r\w\i\n ]]
+ command -v greadlink
+ READLINK=greadlink
+++ greadlink -f leanpkg
++ dirname /Users/shifengzheng/xena-UROP-2018/leanpkg
+ leandir=/Users/shifengzheng/xena-UROP-2018/..
++ greadlink -f /Users/shifengzheng/xena-UROP-2018/..
+ leandir=/Users/shifengzheng
+ librarydir=/Users/shifengzheng/lib/lean
+ test -d /Users/shifengzheng/lib/lean
+ librarydir=/Users/shifengzheng
+ LEAN_PATH=/Users/shifengzheng/library:/Users/shifengzheng/leanpkg
+ PATH=/Users/shifengzheng/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin
+ exec lean --run /Users/shifengzheng/leanpkg/leanpkg/main.lean
<unknown>:1:1: error: file '/Users/shifengzheng/leanpkg/leanpkg/main.lean' not found

[Sebastian Ullrich]

Apparently you still have an old leanpkg at /usr/local/bin

[Kevin Buzzard]

Blair -- I'll be at Imperial in about 10 minutes and will try and sort things out. Sorry it's taken so long -- I had other things to do this morning.

[Blair Shi]

I find a solution to deal with this issue. I just put the Xena-UROP-2018 to my my_playground which already set up mathlib. Now it works