## Stream: new members

### Topic: Dumb question: where did analysis.real go?

#### Kevin Sullivan (Mar 29 2020 at 17:52):

Where is ℝ now defined in mathlib?

#### Patrick Massot (Mar 29 2020 at 17:53):

data.real.basic I think

#### Patrick Massot (Mar 29 2020 at 17:53):

At least that's what I import when I need reals but nothing fancy.

#### Kevin Sullivan (Mar 29 2020 at 17:55):

Patrick Massot said:

At least that's what I import when I need reals but nothing fancy.

Maybe I've got wrong version of mathlib. No data.real.

#### Kevin Buzzard (Mar 29 2020 at 17:57):

Do you have leanproject? The tooling all changed.

#### Kevin Buzzard (Mar 29 2020 at 17:57):

In Lean 3.3.0 I think it was analysis.real

#### Kevin Buzzard (Mar 29 2020 at 17:59):

leanproject will magically update everything in a project to the newest lean and mathlib, assuming you have elan.

#### Kevin Sullivan (Mar 29 2020 at 18:01):

Can you point me to leanproject?

We're using Lean 3.4.2 as installed by elan followed by leanpkg configure and lean --make. init.algebra.field is importable but not data.real...

Possibly complicating matters, I'm trying to use Lean w/ mathlib as a git submodule of another project, and it's a bit of a nightmare to make that work, as Leanpkg wants to point every Lean project to its own remote. Anyway, that's a mostly separate matter.

#### Kevin Buzzard (Mar 29 2020 at 18:03):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian_details.md but if you have elan then pip install mathlibtools (or pip3, or sudo pip...) might be all you need.

#### Kevin Buzzard (Mar 29 2020 at 18:04):

The advantage of the new tooling is that if you're lucky then it will upgrade a Lean project to current Lean (i.e. it will edit the toml), current mathlib (i.e. it will pull _target/deps/mathlib) and then it will download all the compiled olean files for the mathlib commit you just pulled down from some azure server, so you don't need to compile anything.

#### Kevin Buzzard (Mar 29 2020 at 18:05):

leanpkg is deprecated now, and the author of leanproject might be interested if you have some use case which he hasn't thought of yet.

#### Kevin Sullivan (Mar 29 2020 at 18:07):

Kevin Buzzard said:

leanpkg is deprecated now, and the author of leanproject might be interested if you have some use case which he hasn't thought of yet.

Ok, thank you, Kevin. --Kevin

#### Kevin Sullivan (Mar 29 2020 at 18:12):

By the way, where is this stuff about leanproject and mathlibtools documented? Thanks in advance.

#### Bryan Gin-ge Chen (Mar 29 2020 at 18:13):

Here's the mathlib tools repository. Suggestions as to other places we could add links / info to make it more visible would be appreciated!

#### Patrick Massot (Mar 29 2020 at 18:21):

The canonical path starts at https://github.com/leanprover-community/mathlib/blob/master/README.md, follow installation instructions, end up in https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

#### Patrick Massot (Mar 29 2020 at 18:22):

I guess there should be a link from that last file to https://github.com/leanprover-community/mathlib-tools/blob/master/README.md

#### Kevin Buzzard (Mar 29 2020 at 18:22):

I think Kevin has been around a while though, he probably has a set-up which has worked for ages.

#### Patrick Massot (Mar 29 2020 at 18:23):

Yes, that's a problem.

#### Patrick Massot (Mar 29 2020 at 18:23):

There is not much we can do about that.

Last updated: May 14 2021 at 14:20 UTC