trouble running lean program

Stream: new members

[Nischal Karki]

i get this error when running lean by pasting lean <filename.lean> in the terminal:

The term 'lean' is not recognized as the name of a cmdlet, function, script file, or operable program. Check the spelling of the name, or
if a path was included, verify that the path is correct and try again.

how to fix this?

[Alex J. Best]

What operating system, how did you install lean? Did you try restarting the terminal?

[Nischal Karki]

Alex J. Best said:

What operating system, how did you install lean? Did you try restarting the terminal?

windows 10. i installed in the same way as mentioned in documentation. Yes i tried restarting the terminal
while running the program, the file should be at the last of directory right? like this: c:\Users\HP\Desktop\lean_files

[Alex J. Best]

Which documentation did you follow?

[Alex J. Best]

Well the lean executable should run no matter what folder you are in does lean --help show?

[Nischal Karki]

the official lean manual.
no same problem. "lean" is not recognized as any cmdlet, function...
aren't there any other ways to run the program?

[Alex J. Best]

Can you link to the manual you are taking about, I can think of at least 3 things you could mean by that.

[Nischal Karki]

@Alex J. Best https://leanprover.github.io/lean4/doc/quickstart.html

[Alex J. Best]

Ok maybe you can report this in the #lean4 stream