Zulip Chat Archive
Stream: new members
Topic: leanproject command not found
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.
Johan Commelin (Apr 13 2021 at 12:31):
What is the "fast way" on MacOS?
Johan Commelin (Apr 13 2021 at 12:32):
The one-liner installation command from https://leanprover-community.github.io/install/macos.html ?
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
Johan Commelin (Apr 13 2021 at 12:33):
Were there any errors when you ran that command?
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
Johan Commelin (Apr 13 2021 at 12:34):
If those give errors, then you probably had the same errors during the one-line installation
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
Johan Commelin (Apr 13 2021 at 12:39):
Right, so presumably pipx gives an error when you try to execute it.
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...
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?
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
Daoyuan Han (Jun 17 2023 at 06:31):
Hi all. I'm a new member. I successfully installed Lean on Windows. now I'm following the instructions on the [https://leanprover-community.github.io/install/project.html] (url). However, in the terminal (Git bash) I get the following command not found.
leancommandnotfound.PNG. Is git bash the right place to put in this command?
Scott Morrison (Jun 17 2023 at 07:38):
@Daoyuan Han, which instructions did you follow for installing Lean on windows? Can you give a URL? It looks like you just haven't installed leanproject yet (otherwise known as mathlib-tools).
Daoyuan Han (Jun 17 2023 at 16:58):
@Scott Morrison This is the steps I followed https://leanprover-community.github.io/install/windows.html, I followed the steps and checked the #eval 18 + 19, it works fine, then I moved to lean project by clicking on the link and then the problem I mentioned earlier happened.
Daoyuan Han (Jun 17 2023 at 19:12):
@Scott Morrison I guess lean4 doesn't support leanproject command.
Johan Commelin (Jun 17 2023 at 19:14):
That's right. In a Lean 4 setting you should use a combination of git and lake instead.
Patrick Massot (Jun 17 2023 at 19:14):
leanproject is indeed a Lean 3 only tool.
Daoyuan Han (Jun 17 2023 at 19:16):
@Johan Commelin I see. I guess they haven't updated the info on the leanproject page for lean4 yet.
Daoyuan Han (Jun 17 2023 at 19:17):
@Patrick Massot thanks
Daoyuan Han (Jun 17 2023 at 19:18):
@Johan Commelin I guess I will download lean3 then. Maybe after they update the info, I will shift to lean4
Patrick Massot (Jun 17 2023 at 19:19):
I can see https://leanprover-community.github.io/install/windows.html still has a link to https://leanprover-community.github.io/install/project.html which is completely wrong since it means a page about Lean 4 links to a page about Lean 3. We are sorry about the inconvenience.
Patrick Massot (Jun 17 2023 at 19:19):
There is no point learning Lean 3 at this stage, it will be completely deprecated before the end of summer.
Johan Commelin (Jun 17 2023 at 19:19):
@Daoyuan Han Yeah, sorry for the confusion. We are right in the middle of a transition to Lean 4. The website saw a bunch of updates last week. So thanks for reporting this "bug".
Daoyuan Han (Jun 17 2023 at 19:29):
@Patrick Massot Thanks for letting me know; I will stay with Lean4 then; maybe after the community updates the website, I will give it another try.
Daoyuan Han (Jun 17 2023 at 19:30):
@Johan Commelin Thanks.
Johan Commelin (Jun 17 2023 at 19:36):
@Daoyuan Han Feel free to ask questions here. That helps us figure out which questions the docs should answer.
Daoyuan Han (Jun 17 2023 at 19:54):
@Johan Commelin yeah, definitely. Thanks, it's a very helpful chat room.
Last updated: Dec 20 2023 at 11:08 UTC