Zulip Chat Archive

Stream: new members

Topic: leanproject command not found


view this post on Zulip Leonardo Rosso (Apr 13 2021 at 12:21):

Hi all. I'm a new member and I'm following lftcm2020. I successfully installed Lean (on MacOS with the fast way) and VS code, and now following the instructions on the page "Lean projects" as in Patrick Massot's video. However in the terminal I get the following command not found: issue.jpeg. I tried to log out and log back in but it doesn't help.

view this post on Zulip Johan Commelin (Apr 13 2021 at 12:31):

What is the "fast way" on MacOS?

view this post on Zulip Johan Commelin (Apr 13 2021 at 12:32):

The one-liner installation command from https://leanprover-community.github.io/install/macos.html ?

view this post on Zulip Leonardo Rosso (Apr 13 2021 at 12:32):

The "fast way" is: https://leanprover-community.github.io/install/macos.html#installing-lean-and-mathlib with the one-line copy paste

view this post on Zulip Johan Commelin (Apr 13 2021 at 12:33):

Were there any errors when you ran that command?

view this post on Zulip Johan Commelin (Apr 13 2021 at 12:33):

You can try to execute the following three commands: https://leanprover-community.github.io/install/macos_details.html#installing-mathlib-supporting-tools

view this post on Zulip Johan Commelin (Apr 13 2021 at 12:34):

If those give errors, then you probably had the same errors during the one-line installation

view this post on Zulip Leonardo Rosso (Apr 13 2021 at 12:37):

During the one-liner I didn't find any errors but not sure. I just tried the first command "brew install python3 pipx" and it gives an error at some point:

Downloading https://ghcr.io/v2/homebrew/core/pipx/manifests/0.15.1.3_1
curl: (22) The requested URL returned error: 404
Error: Failed to download resource "pipx_bottle_manifest"
Download failed: https://ghcr.io/v2/homebrew/core/pipx/manifests/0.15.1.3_1

view this post on Zulip Johan Commelin (Apr 13 2021 at 12:39):

Right, so presumably pipx gives an error when you try to execute it.

view this post on Zulip Leonardo Rosso (Apr 13 2021 at 12:49):

Do you know of any fix? I have to admit I have next to zero experience with this kind of things...

view this post on Zulip Anne Baanen (Apr 13 2021 at 12:53):

I am not very familiar with brew, but it seems like you have an old version of the "formulas". Could you try running brew update, then the commands linked by Johan again?

view this post on Zulip Leonardo Rosso (Apr 13 2021 at 15:38):

I did as Anne suggested (I ran "brew update" and "brew upgrade", which took a long time) and then rerun the commands suggested by Johan. Now everything works! Many thanks to both


Last updated: May 13 2021 at 22:15 UTC