Zulip Chat Archive

Stream: new members

Topic: Creating Lean project


view this post on Zulip Saroj N (Dec 03 2020 at 23:52):

I havent been able to create a lean project. When I type "leanproject new my_project" on command prompt, it says "zsh: /Users/saroj/.local/bin/leanproject: bad interpreter: /Users/saroj/.local/pipx/venvs/mathlibtools/bin/python: no such file or directory". Can anyone help?

view this post on Zulip Adam Topaz (Dec 03 2020 at 23:54):

Is looks like you installed mathlibtools in a python venv, and the environment hasn't been activated

view this post on Zulip Adam Topaz (Dec 03 2020 at 23:55):

In any case, this looks like a path issue

view this post on Zulip Adam Topaz (Dec 04 2020 at 00:03):

Can you recall how you installed mathlibtools?

view this post on Zulip Saroj N (Dec 04 2020 at 00:07):

I followed the detailed instructions from lean prover community website

view this post on Zulip Saroj N (Dec 04 2020 at 01:12):

i followed the detailed instructions on lean prover community

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:14):

What operating system are you using? Did you use the same terminal to create the lean project as you did when installing? Did you try rebooting? On unix I'd suggest source ~/.profile.

view this post on Zulip Julian Berman (Dec 04 2020 at 05:25):

That looks unlikely to be a venv created manually

view this post on Zulip Julian Berman (Dec 04 2020 at 05:25):

And should work even without being activated

view this post on Zulip Julian Berman (Dec 04 2020 at 05:25):

It seems more likely that that interpreter just actually doesn't exist

view this post on Zulip Julian Berman (Dec 04 2020 at 05:26):

What is ls /Users/saroj/.local/pipx/venvs/mathlibtools/bin?

view this post on Zulip Julian Berman (Dec 04 2020 at 05:28):

If it comes back not existing, probably rerun pipx install mathlibtools


Last updated: May 13 2021 at 06:15 UTC