Zulip Chat Archive
Stream: new members
Topic: Can someone help me to solve this problem in VSCode
Kyle Yank (Feb 01 2024 at 18:00):
Kyle Yank (Feb 01 2024 at 18:00):
I don't know how to download the package
Riccardo Brasca (Feb 01 2024 at 18:01):
Have you opened the folder of the project rather than the single file?
Kyle Yank (Feb 01 2024 at 18:01):
Where's the folder?
Riccardo Brasca (Feb 01 2024 at 18:03):
You are working on mathlib, right? I mean the mathlib folder where the file you opened is located
Kyle Yank (Feb 01 2024 at 18:03):
yep
Kyle Yank (Feb 01 2024 at 18:04):
And then,what should I do
Riccardo Brasca (Feb 01 2024 at 18:04):
In vs code you need to select "open folder" and open the mathlib4 folder
Kyle Yank (Feb 01 2024 at 18:06):
If I don't have mathlib4 ,then what should Ido
Riccardo Brasca (Feb 01 2024 at 18:08):
How did you get the file you have already opened?
Kyle Yank (Feb 01 2024 at 18:08):
in mathlib
Riccardo Brasca (Feb 01 2024 at 18:08):
So you have mathlib
Kyle Yank (Feb 01 2024 at 18:09):
I opened a new text file, and just pasted the code from mathlib
Kyle Yank (Feb 01 2024 at 18:10):
Should I download the mathlib4 folder in my computer?
Riccardo Brasca (Feb 01 2024 at 18:10):
I see.
git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4
lake exe cache get
Will download for you everything you need to work with mathlib.
Riccardo Brasca (Feb 01 2024 at 18:11):
You can also do it via the vs code interface, click on the \forall
symbol, then download project or something similar (I am on mobile)
Kyle Yank (Feb 01 2024 at 18:15):
I actually still do not understand what you told me to do
Kyle Yank (Feb 01 2024 at 18:19):
Where is the \forall symbol
Kyle Yank (Feb 01 2024 at 18:34):
You mean,I paste this in the git CMD?
Kyle Yank (Feb 01 2024 at 18:40):
Martin Dvořák (Feb 01 2024 at 18:42):
I think this icon (in VS Code, assuming you have the right plugin) was meant:
image.png
Kyle Yank (Feb 01 2024 at 18:46):
Dan Velleman (Feb 01 2024 at 19:53):
@Kyle Yank : Have you read this: https://leanprover-community.github.io/install/project.html?
Kyle Yank (Feb 02 2024 at 04:23):
I’m gonna check it right now.
Last updated: May 02 2025 at 03:31 UTC