Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC