Waiting for lean server to start

Stream: new members

[Ali Alamen]

hi everyone ..it is my first time using lean and leaninfoviewer doesn't show me anythins just "Waiting for Lean server to start..." can anyone please help me for this problem ? Capture.PNG

[Kevin Buzzard]

You can't just run Lean on a file, you need to run it as part of a project. Read about how to create a project of your own, or how to download an existing project, here.

[Eric Taucher]

What helped me understand all of the getting it installed were the YouTube playlist tutorial videos found here.

[Ali Alamen]

https://www.youtube.com/watch?v=y3GsHIe4wZ4&list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv&index=5 I have watched it and I have followed the steps but I still have the same problem

[Kevin Buzzard]

Your problem -- or at least one of your problems -- is that you are not using Lean within a project. I can reproduce your problem by creating a random lean file somewhere on my computer and opening that file within VS Code. Lean doesn't start. This is expected behaviour.

When you have set up a project and have opened the root directory of project using "open folder" in VS Code and moved your file into the project -- if you still have the same error then get back in touch.

[Ali Alamen]

Capture.PNG
I still have the same problem even after making it inside a folder

[Alex J. Best]

The button on the left of your screenshot that says open folder is what you need to use

[Ali Alamen]

same problem :sweat_smile: Capture1.PNG

[Alex J. Best]

Ok well maybe we should back up a bit

[Alex J. Best]

It looks like you have both the lean and lean4 extensions installed and active at the same time

[Alex J. Best]

The video you linked to refers to lean 3

[Alex J. Best]

Which means you should probably disable the lean 4 extension unless you actually want to play with lean 4 (it's currently not released)

[Kevin Buzzard]

The problem is still what I am saying, it's nothing to do with Lean 4

[Ali Alamen]

Oh!! I have unistalled lean4 , :heart_eyes: :grinning_face_with_smiling_eyes: worked

[Kevin Buzzard]

You are posting exactly the right kind of screenshot @Ali Alamen . Your screenshot indicates that you have a directory hopefully called "lean projects" but this directory does not contain any Lean projects, it just contains a random file. A Lean project is a well-defined thing -- it is a directory with certain specific system files in which leanproject new my_project will create for you.

[Alex J. Best]

In Scott's video typing #eval 2+2 in a blank file does work though

[Kevin Buzzard]

Oh OK if you've got it working, great :-)

[Kevin Buzzard]

I just tried it and it didn't work for me, the server didn't start. Maybe he had a random leanpkg.toml in ~?

[Alex J. Best]

Even without a project. But yes as Kevin says to really use lean you need to me in a project, there is also a video for this I think https://youtu.be/CM0wYOrYII8

[Ali Alamen]

thanks a million :pray:

[Kevin Buzzard]

I can see that Ali's setup still isn't correct because if you have done the "open folder" stuff correctly you can see files like leanpkg.toml

[Kevin Buzzard]

Ali I'm not convinced you're out of the woods yet

[Kevin Buzzard]

waiting.png
If I open a file in ~ with VS Code I have the same problem as Ali.

[Kevin Buzzard]

If I open a correctly-formatted Lean project with VS Code then I can see the system files in the file explorer on the left, and my Lean works fine. ok.png

[Ali Alamen]

okay .. I didn't get it yet ... how can I open it correctly and make a directory with certain specific system files leannpic.PNG

[Kevin Buzzard]

have you got a lean project on your computer? I don't mean "a directory called lean_project" or "a file which I'm calling a project", I mean the link I posted above about how to make Lean projects with system files in them called things like _target and leanpkg.toml. Until the answer to this question is "yes" you will be experiencing problems.

[Ali Alamen]

I think I have got it leanphoto.PNG

[Kevin Buzzard]

For sure you are now up and running!

[Kevin Buzzard]

I can tell it's now working because you have the tactic state on the right, and you only get that sort of stuff when everything is working OK

[Ali Alamen]

thanks a lot Kevin :)

[Kevin Buzzard]

Sorry it took so long!

[Ali Alamen]

yeah :sweat_smile:

[Ali Alamen]

it was my problem :sweat_smile:

[Ali Alamen]

my fault*

[Ali Alamen]

that I didn't see the video .. anyway thanks again Kevin :pray:

[Eric Taucher]

Ali Alamen said:

that I didn't see the video

Glad to hear you have it working. :heart:

In order to help me better understand to help others in the future. Which tutorial video(s) did you watch? Which ones helped you? Which ones would you recommend? Would you recommend watching all of the videos first before attempting any of the steps?

[Ali Alamen]

https://www.youtube.com/channel/UCWe5B7Ikr0AI9727doEUxPg/playlists this channal
and this one specifically https://www.youtube.com/watch?v=T4yt53dCqCU&list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv

[Ali Alamen]

the video which Alex mentioned what I didn't wathc .. at this playlist