starting a new project

Stream: new members

[Conrad]

hey guys,in lean4 how could i start a project?

[Scott Morrison]

Have you installed Lean 4 per https://leanprover-community.github.io/get_started.html?

[Filippo A. E. Nuccio]

@Conrad Perhaps your question should be posted in this stream. At any rate, have you tried looking here?

[Scott Morrison]

After that, you should look at https://leanprover-community.github.io/install/project.html, which will tell you how to create a new project.

[Notification Bot]

4 messages were moved here from #general > two github questions by Scott Morrison.

[Filippo A. E. Nuccio]

(deleted)

[Filippo A. E. Nuccio]

Ops, my answer overlapped with Scott's, sorry!

[Conrad]

@Filippo A. E. Nuccio thank you ,i just can't find the instructions for lean4

[Conrad]

do you have more information about it?

[Filippo A. E. Nuccio]

Do you mean the instructions to install it or to use it (like "how can I state in lean4 that 1+1 = 2 and prove this "theorem")?

[Conrad]

i have install lean4,but i can't follow the instruction aboutsth like,Getting mathlib oleans,
Upgrading mathlib

[Conrad]

i mean in this part
image.png

[Filippo A. E. Nuccio]

Oh, but this is lean3!

[Conrad]

@Filippo A. E. Nuccio

[Riccardo Brasca]

leanproject is for lean 3

[Johan Commelin]

There's a massive blue warning box at the top of that page

[Filippo A. E. Nuccio]

The way lean3 and lean4 work are very different.

[Filippo A. E. Nuccio]

Well, at least the way you install them...

[Johan Commelin]

Scott Morrison said:

After that, you should look at https://leanprover-community.github.io/install/project.html, which will tell you how to create a new project.

You should try this link instead

[Conrad]

yes, so what is lean4's sustitution to it.

[Riccardo Brasca]

It's called lake. You find some basic documentation here

[Conrad]

oh, so what are you usually using,either lean or lean4?

[Filippo A. E. Nuccio]

Defnitely lean4

[Filippo A. E. Nuccio]

There is not such a thing as lean, actually: there are/were lean1-lean2, then we played a lot with lean3, now there is lean4. This is the one we all currently use, basically, and it is the one you should focus on.

[Conrad]

Wow, thanks guys!

[Conrad]

And another question,you said "post questions in this stream",where is it in the interface of zulipchat? @Filippo A. E. Nuccio

[Filippo A. E. Nuccio]

If you have a GitPod account, you can have a look at the section To use this repository with Gitpod in this page. This would allow you to play a bit with lean4 without installing it. Getting such an account is free and easy.

[Filippo A. E. Nuccio]

Conrad said:

And another question,you said "post questions in this stream",where is it in the interface of zulipchat? Filippo A. E. Nuccio

Some magic happened and now we are in the stream I was speaking of, you can ignore that message of mine and keep asking your questions in this strem :magic:

[Conrad]

ok

[Conrad]

hi,i wonder how to build a lake(a kind of project)@Filippo A. E. Nuccio
image.png
image.png

[Conrad]

in vs code ,it is the same
image.png

[Bulhwi Cha]

@Conrad Do you really want to build Lake from the source?

[Conrad]

yes

[Conrad]

Maybe i shall ask another question first(i don't know ,i am confused):i follow this guide:https://leanprover-community.github.io/install/project.html . But i met trouble here:
image.png
image.png

[Bulhwi Cha]

Did you install Lean 4?

[Conrad]

yes,in vs code

[Bulhwi Cha]

Did you install Git for Windows?

[Conrad]

yes

[Conrad]

i mean i already have downloded it,i am Creating a Lean project

[Bulhwi Cha]

Do you know how to run Git Bash on VS Code?

[Conrad]

i don't know

[Bulhwi Cha]

Hang on—I'm switching from Linux to Windows.

[Conrad]

however,git bash can run well in windows as an app

[Bulhwi Cha]

Do you want to create a Lean project that depends on Mathlib?

[Bulhwi Cha]

If so, run lake new your_project_name math on Git Bash.

[Conrad]

yes

[Conrad]

what's wrong with it:
image.png

[Conrad]

how to fix it?

[Conrad]

And the cache and lake_package is dimming:
image.png

[Bulhwi Cha]

On Git Bash, use cd to change your working directory to your project's directory. For example, if your project playground is in ~/lean-projects, run cd ~/lean-projects/playground. (~ is your home directory.)

[Bulhwi Cha]

On VS Code, open your project using "File > Open Folder..." (Ctrl+K Ctrl+O).

[Conrad]

hi bro ,can you help me ,i wanna create a new project on lean4,but "unknown package 'Mathlib'" happens. How to deal with it
image.png

[Notification Bot]

Scott Morrison has marked this topic as unresolved.

[Notification Bot]

A message was moved here from #new members > ✔ get-mathlib-cache on Lean 4? by Scott Morrison.

[Scott Morrison]

@Conrad, I've moved your message here. If you've already started a topic, please try to write follow-up messages in the same topic, rather than in unrelated other topics.

[Scott Morrison]

Can you show us the contents of your lakefile.lean?

[Scott Morrison]

(Also, I see you posted duplicate messages in multiple topics. Please do not do this!)

[Conrad]

oh ,i am really sorry,i don't know how this chatroom works

[Conrad]

image.png
@Scott Morrison

[Kevin Buzzard]

You need to open the root directory of your project using VS Code's open folder functionality. In your screenshot you have opened a folder called 0 instead.