## Stream: new members

### Topic: Opening my first lean project

#### Choink Ivt (Oct 03 2019 at 08:20):

Hello, I'm trying to follow the instructions on https://xenaproject.wordpress.com/installing-lean-and-mathlib/ but it says

If you want Lean and mathlib to work on a local installation, you need to open a project. You can tell when a folder contains a Lean project because the folder will have a file called leanpkg.path and another file called leanpkg.toml in it.

I don't have any projects and I can't find a way to create one, and trying to run import data.int.basic without a project gives me the error of neading to install leanpkg.path. How can I solve this issue?

#### Johan Commelin (Oct 03 2019 at 08:24):

Hi @Choink Ivt, do these instructions help: https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md

#### Johan Commelin (Oct 03 2019 at 08:25):

@Kevin Buzzard Can you update that blogpost to point towards the installation instructions in https://github.com/leanprover-community/mathlib/blob/master/README.md

#### Johan Commelin (Oct 03 2019 at 08:26):

@Choink Ivt In that directory there is a bunch of installation instructions depending on OS: Linux/Mac/Windows, etc...

#### Choink Ivt (Oct 03 2019 at 08:28):

Hi @Johan Commelin! When I type #eval 1+1 I get a blue squiggly line, not a green one, but 2 appears in Lean Messages - is that intended? I'm using https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md, and have installed mathlib, elan and VS Code.

#### Johan Commelin (Oct 03 2019 at 08:33):

What happens if you type #check nat and/or #check 3?

#### Johan Commelin (Oct 03 2019 at 08:34):

If those give output Type resp. nat, then I wouldn't be too concerned.

#### Johan Commelin (Oct 03 2019 at 08:34):

Maybe VScode updated their color styles...

#### Choink Ivt (Oct 03 2019 at 08:34):

I get N: Type and 3: N (with blackboard style N). But the import data.int.basic is still showing 2 errors.

#### Johan Commelin (Oct 03 2019 at 08:36):

Ok, so Lean is working

#### Johan Commelin (Oct 03 2019 at 08:38):

Sorry, I need to run

#### Johan Commelin (Oct 03 2019 at 08:39):

You need to use leanpkg to start a project

#### Johan Commelin (Oct 03 2019 at 08:39):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

#### Johan Commelin (Oct 03 2019 at 08:40):

This doesn't seem to be mentioned in the Windows install instructions...

#### Johan Commelin (Oct 03 2019 at 08:40):

I really need to go, maybe someone else can help

#### Choink Ivt (Oct 03 2019 at 08:40):

Ah that seems to be the missing step. Thanks!

#### Patrick Massot (Oct 03 2019 at 09:07):

The last line of https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md is a link to https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md, which is common to all OS

#### Choink Ivt (Oct 03 2019 at 09:34):

Ah thanks, must have missed that. It's working now, though it's taking a long time to check the packages. Are there any recommended ways to get started, or should I just float around the various sites such as https://xenaproject.wordpress.com/ and http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html/?

#### Patrick Massot (Oct 03 2019 at 09:55):

It shouldn't take a long time. Did you run update-mathlib in your project?

#### Choink Ivt (Oct 03 2019 at 10:06):

Yep. I just opened it again and it was a lot quicker this time; perhaps something was running in the background.

#### Marc Huisinga (Oct 03 2019 at 10:21):

TPIL (https://leanprover.github.io/theorem_proving_in_lean/) is a great introduction that covers the basics of lean itself.

#### Choink Ivt (Oct 03 2019 at 11:19):

I'm trying to work through https://xenaproject.wordpress.com/2017/10/31/building-the-non-negative-integers-from-scratch/; I'm trying to prove a=b given a+zero=b+zero, but I don't understand why rw [←add_zero] is not changing this to a+zero=b (perhaps with +zero on the end), since add_zero is the statement n+zero=n.

#### Patrick Massot (Oct 03 2019 at 11:45):

Could you please post some code that we could run on our end? This would make it much more likely that you'll receive help.

#### Patrick Massot (Oct 03 2019 at 11:46):

It is very hard to know what you did wrong with so few information.

#### Choink Ivt (Oct 03 2019 at 12:12):

I would but I discovered a workaround that finished the proof, thanks anyway.

#### Kevin Buzzard (Oct 03 2019 at 15:53):

There was a direct link from the home page which I've now moved to point to the installation part of the readme. Thanks for pointing this out @Johan Commelin

Last updated: May 07 2021 at 00:30 UTC