## Stream: new members

#### Fames Yasd (Sep 06 2020 at 14:49):

I was working through "theorem proving in lean" and got the message in the op.
I somehow installed lean (on windows) several years ago and it highlights commands, shows info. I got to chapter 4 in that book not knowing something was off.
It also says lean-3.4.1-windows at the top of vscode.
What do I need to do?

#### Kevin Buzzard (Sep 06 2020 at 15:08):

Read the instructions on how to install a modern Lean and mathlib at https://leanprover-community.github.io/get_started.html

#### Fames Yasd (Sep 06 2020 at 17:09):

Kevin Buzzard
it says me this:
Users@User MINGW64 ~
$curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh info: downloading installer Archive: elan-init.zip inflating: elan-init.exe error: it looks like you have an existing installation of Lean at: error: C:\Users\Users\Downloads\lean-3.4.1-windows\lean-3.4.1-windows\bin error: elan cannot be installed alongside Lean. Please uninstall first error: if this is what you want, restart the installation with -y' error: cannot install while Lean is installed #### Kevin Buzzard (Sep 06 2020 at 17:10): uninstall your super-old lean like it says #### Fames Yasd (Sep 06 2020 at 17:14): Do I simply delete the folder? #### Kevin Buzzard (Sep 06 2020 at 17:16): Why don't you restart the installation with -y like it says? #### Kevin Buzzard (Sep 06 2020 at 17:17): Oh, I see #### Kevin Buzzard (Sep 06 2020 at 17:17): I would strongly recommend not just simply deleting random folders though, that is almost never the correct way to uninstall something nowadays #### Kevin Buzzard (Sep 06 2020 at 17:17): I'm afraid I don't know anything about macs. Why don't you just google for how to uninstall something? #### Fames Yasd (Sep 06 2020 at 17:18): what is macs? #### Kevin Buzzard (Sep 06 2020 at 17:18): Oh sorry, I assumed you were on a mac. This is Windows? I'm afraid I don't know anything about that either :-) #### Kevin Buzzard (Sep 06 2020 at 17:19): Can you remember how you installed Lean? #### Fames Yasd (Sep 06 2020 at 17:19): I followed some instruction #### Fames Yasd (Sep 06 2020 at 17:19): I guess the old one #### Kevin Buzzard (Sep 06 2020 at 17:19): Do you know what, if this is Windows then I suspect that you can just delete the directory. #### Fames Yasd (Sep 06 2020 at 17:19): ok #### Kevin Buzzard (Sep 06 2020 at 17:19): I thought you had installed Lean using some package manager with a mac. #### Kevin Buzzard (Sep 06 2020 at 17:20): But there is no package manager which installs Lean for windows so you're on safer ground #### Fames Yasd (Sep 06 2020 at 17:25): okay, so it writes this: Elan is installed now. Great! To get started you need Elan's bin directory (%USERPROFILE%\.elan\bin) in your PATH environment variable. Future applications will automatically have the correct environment, but you may need to restart your current shell. Press the Enter key to continue. Users@User MINGW64 ~$ echo 'PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile Users@User MINGW64 ~$
I assume everything went fine?

#### Reid Barton (Sep 06 2020 at 17:27):

Kevin, I'm not sure if you know as little about Macs as you claim, but they tend not to use drive letters (C:), have backslashes in paths, or contain the string windows in the path of the lean installation.

#### Fames Yasd (Sep 06 2020 at 17:27):

this is off-topic but how do you find the threads that you've participated in?

#### Reid Barton (Sep 06 2020 at 17:29):

Click on the icon next to your messages and then choose "View messages sent"

Thank you

#### Fames Yasd (Sep 07 2020 at 06:58):

Kevin Buzzard
okay, so I did everything on a page that you linked me, now when I write
"import data.int.basic" it writes me this:
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

#### Fames Yasd (Sep 07 2020 at 07:15):

I read it but I have not understood much, I think my file was pretty bare though, as it only had one command "import data.int.basic" in it.

#### Fames Yasd (Sep 07 2020 at 07:27):

It says in a first bullet under working with an existing project that I need to log-in somewhere. The first commands " source ~/.profile " seemingly did nothing? And the second command "source ~/.bash_profile" said
bash: /c/Users/Users/.bash_profile: No such file or directory

#### Fames Yasd (Sep 07 2020 at 07:28):

I then proceeded with the command "leanproject get tutorials" and it showed me this window 1.png

#### Kevin Buzzard (Sep 07 2020 at 07:31):

You can't just open a file and expect imports to work

I believe you

#### Kevin Buzzard (Sep 07 2020 at 07:31):

You need to be working in a project. If you want to download the tutorial project from GitHub then go ahead and click yes

#### Kevin Buzzard (Sep 07 2020 at 07:32):

If you want to make your own project you can do that too. All this is explained in the docs

#### Scott Morrison (Sep 07 2020 at 07:35):

@Fames, the OpenSSH dialog you've shown is there because leanproject is using git, which is using ssh to communicate with the github.com server. The first time you ever do this, you need to allow this connection. If you click OK it shouldn't happen again.

#### Scott Morrison (Sep 07 2020 at 07:36):

An easier alternative to all the source` commands if you're not sure what you're doing is to restart your computer. :-)

#### Fames Yasd (Sep 07 2020 at 18:19):

I think I did everything on a page with projects.
How do I make the pop-ups on the left disappear? 2.png

what popups?

staged changes

#### Fames Yasd (Sep 07 2020 at 18:20):

I don't know what that means

#### Mario Carneiro (Sep 07 2020 at 18:21):

the sidebar shows several things, you can switch between them by pressing the buttons along the left side

#### Mario Carneiro (Sep 07 2020 at 18:21):

it's currently showing git staged changes

#### Mario Carneiro (Sep 07 2020 at 18:22):

which are useful for version control and if you eventually want to publish your work on github

#### Mario Carneiro (Sep 07 2020 at 18:22):

you can hide the sidebar with ctrl-B

#### Bryan Gin-ge Chen (Sep 07 2020 at 18:23):

There's general documentation for VS Code here: https://code.visualstudio.com/docs

It might be worth skimming some of it to see what all the parts of the interface do.

#### Fames Yasd (Sep 07 2020 at 18:33):

@Mario Carneiro ctrl-B does not do it, I figured out what I wanted with Ctrl-Shift-G

Last updated: May 13 2021 at 06:15 UTC