leanproject

Stream: new members

[Michael Beeson]

Suddenly "leanproject" doesn't work:

beeson@iMac inf % leanproject build
zsh: command not found: leanproject
beeson@iMac inf % ls
Junk _target leanpkg.path leanpkg.toml src
beeson@iMac inf %

[Johan Commelin]

maybe reinstall mathlibtools?

[Johan Commelin]

does your shell still find elan and lean executables?

[Michael Beeson]

No, it doesn't. I bet this has to do with making zsh the default shell; I think Apple did that in a recent update.

[Mario Carneiro]

can you just start up bash or whatever you were using before and then access lean et al?

[Patrick Massot]

Can you use other command line tools using python?

[Michael Beeson]

I can start python3, no problem

[Michael Beeson]

bash-3.2$ leanproject build
bash: /Users/beeson/.local/bin/leanproject: /Users/beeson/.local/pipx/venvs/mathlibtools/bin/python: bad interpreter: No such file or directory
bash-3.2$

[Michael Beeson]

So at least bash does recognize "leanproject".

[Michael Beeson]

brew upgrade elan mathlibtools
produced an error message
Error:
homebrew-core is a shallow clone.

[Mario Carneiro]

do python or python3 work?

[Michael Beeson]

Yes python3 works.

[Mario Carneiro]

it looks like you might need to symlink python to python3

[Mario Carneiro]

there is probably a command for this?

[Michael Beeson]

python works too. I don't see the point of a symlink. Would like to know what the problem is rather than try random things. I did not change anything (except to accept making zsh the default shell).

[Mario Carneiro]

but not /bin/python?

[Mario Carneiro]

the error sounds like there is nothing at that location

[Michael Beeson]

Now I did
pipx uninstall mathlibtools && brew install mathlibtools

and after that I get this (so at least leanproject starts up):

beeson@iMac inf % leanproject build
Building project inf
[Errno 2] No such file or directory: 'leanpkg'

[Michael Beeson]

Aha! I did
source ~/.profile

and after that leanproject works normally again. Thanks for trying to help.

[Julian Berman]

Definitely don't symlink python to python3 on macOS

[Julian Berman]

If the instructions we just added for migrating installs don't cover this let me know, but hopefully that final command you ran came from finding https://leanprover-community.github.io/install/macos_details.html#aside-migrating-from-older-installations ?

[Julian Berman]

FWIW, bash: /Users/beeson/.local/bin/leanproject: /Users/beeson/.local/pipx/venvs/mathlibtools/bin/python this error normally means "homebrew upgraded your python, and that breaks all your virtualenvs because that's not a safe thing to do"

[Julian Berman]

That issue is documented here: https://github.com/leanprover-community/mathlib-tools/issues/94 but my recommendation is still that we close that, because this new way that you're now on (which doesn't use pipx directly) does not have that issue anymore.