file 'data\int\basic' not found in the LEAN_PATH

Stream: new members

[Fames Yasd]

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]

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

[Fames Yasd]

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]

uninstall your super-old lean like it says

[Fames Yasd]

Do I simply delete the folder?

[Kevin Buzzard]

Why don't you restart the installation with -y like it says?

[Kevin Buzzard]

Oh, I see

[Kevin Buzzard]

I would strongly recommend not just simply deleting random folders though, that is almost never the correct way to uninstall something nowadays

[Kevin Buzzard]

I'm afraid I don't know anything about macs. Why don't you just google for how to uninstall something?

[Fames Yasd]

what is macs?

[Kevin Buzzard]

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]

Can you remember how you installed Lean?

[Fames Yasd]

I followed some instruction

[Fames Yasd]

I guess the old one

[Kevin Buzzard]

Do you know what, if this is Windows then I suspect that you can just delete the directory.

[Fames Yasd]

ok

[Kevin Buzzard]

I thought you had installed Lean using some package manager with a mac.

[Kevin Buzzard]

But there is no package manager which installs Lean for windows so you're on safer ground

[Fames Yasd]

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]

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]

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

[Reid Barton]

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

[Fames Yasd]

Thank you

[Fames Yasd]

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:
file 'data\int\basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

[Kevin Buzzard]

Did you read the first bullet point in the link?

[Fames Yasd]

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.
I guess I have to read the page about projects now.

[Fames Yasd]

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]

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

[Kevin Buzzard]

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

[Fames Yasd]

I believe you

[Kevin Buzzard]

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]

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

[Scott Morrison]

@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]

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

[Fames Yasd]

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

[Mario Carneiro]

what popups?

[Fames Yasd]

staged changes

[Fames Yasd]

I don't know what that means

[Mario Carneiro]

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

[Mario Carneiro]

it's currently showing git staged changes

[Mario Carneiro]

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

[Mario Carneiro]

you can hide the sidebar with ctrl-B

[Bryan Gin-ge Chen]

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]

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