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):

image.png

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):

image.png

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):

image.png

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