Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 17:10):

uninstall your super-old lean like it says

view this post on Zulip Fames Yasd (Sep 06 2020 at 17:14):

Do I simply delete the folder?

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 17:16):

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

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 17:17):

Oh, I see

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Fames Yasd (Sep 06 2020 at 17:18):

what is macs?

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 17:19):

Can you remember how you installed Lean?

view this post on Zulip Fames Yasd (Sep 06 2020 at 17:19):

I followed some instruction

view this post on Zulip Fames Yasd (Sep 06 2020 at 17:19):

I guess the old one

view this post on Zulip 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.

view this post on Zulip Fames Yasd (Sep 06 2020 at 17:19):

ok

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 17:19):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Fames Yasd (Sep 06 2020 at 17:27):

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

view this post on Zulip Reid Barton (Sep 06 2020 at 17:29):

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

view this post on Zulip Fames Yasd (Sep 06 2020 at 17:31):

Thank you

view this post on Zulip 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:
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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 07:09):

Did you read the first bullet point in the link?

view this post on Zulip 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.
I guess I have to read the page about projects now.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 07:31):

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

view this post on Zulip Fames Yasd (Sep 07 2020 at 07:31):

I believe you

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 18:20):

what popups?

view this post on Zulip Fames Yasd (Sep 07 2020 at 18:20):

staged changes

view this post on Zulip Fames Yasd (Sep 07 2020 at 18:20):

I don't know what that means

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 18:21):

it's currently showing git staged changes

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 18:22):

you can hide the sidebar with ctrl-B

view this post on Zulip 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.

view this post on Zulip 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