Zulip Chat Archive

Stream: new members

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


view this post on Zulip Kevin Sullivan (Mar 29 2020 at 17:52):

Where is ℝ now defined in mathlib?

view this post on Zulip Patrick Massot (Mar 29 2020 at 17:53):

data.real.basic I think

view this post on Zulip Patrick Massot (Mar 29 2020 at 17:53):

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

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 17:57):

Do you have leanproject? The tooling all changed.

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 17:57):

In Lean 3.3.0 I think it was analysis.real

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

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

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

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

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

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

view this post on Zulip Kevin Sullivan (Mar 29 2020 at 18:12):

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

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

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

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

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

view this post on Zulip Patrick Massot (Mar 29 2020 at 18:23):

Yes, that's a problem.

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