mathlib:prelude

Stream: lean4

[Daniel Selsam]

Mario Carneiro said:

yes, it's only for tactic stuff and supporting lemmas, like lean 3 core (which is a bit bigger than lean 4 core is right now) + mathlib tactic/

How will this lean3 core compare to the mathport lean3 core? Is the goal to keep them def-eq and then auto-align?

[Mario Carneiro]

there's no way the tactics will align with anything

[Daniel Selsam]

I mean for the supporting lemmas.

[Mario Carneiro]

From the point of view of mathlib, the prelude is just another dependency along with lean 4 core. So it can align to definitions the same way as core lean definitions like Nat

[Daniel Selsam]

I understand, I was just wondering if there was a risk of non-def-eq duplication and clashes. This would not be an issue as long as the prelude repo used Mathlib.Prelude namespace or something like that to distinguish.

[Mario Carneiro]

It's not a ported library, so it doesn't need to dump everything in a namespace, right? I assume that eventually mathlib will just put things in the root, like currently

[Daniel Selsam]

I think mathlib should put everything in Mathlib.

[Mario Carneiro]

I don't want to add an extra 8 characters on a substantial number of fully qualified names in usual mathlib proofs

[Mario Carneiro]

I'm not sure what the point is

[Mario Carneiro]

it's not like it's hard to avoid collision with mathlib

[Kevin Buzzard]

Isn't this pretty normal in stuff like python? The only difference would be that mathlib users would just write open mathlib at the start of their code and mathlib developers would write namespace mathlib at the start of theirs. Or am I being naive?

[Daniel Selsam]

@Kevin Buzzard Yes it is normal for programming, and I use qualified imports all the time (e.g. import tensorflow as tf in python and import qualified Data.Set as Set in haskell). C++ doesn't support qualified imports and so the convention is for every project to use its own namespace, which is what I was suggesting. But I agree with @Mario Carneiro that the extra namespace is effectively zero-cost in C++ but does carry a cost in lean since some metaprogramming contexts require providing full names.

FYI all the mathlib:* threads from last night were from one sprawling conversation, and I was changing the topic names as the conversation progressed. This particular thread continued at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathlib.3Anamespace

[Sebastian Ullrich]

Daniel Selsam said:

but does carry a cost in lean since some metaprogramming contexts require providing full names.

This is an interesting point actually. We have name resolution with `` and in quotations, what parts are we still missing?

[Daniel Selsam]

I was basing that comment on https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathlib.3Aprelude/near/234611307 :)

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

There's another reason to use the global namespace though. And that's dot-notation. For that you need to put declarations in the same namespace as the original definition.

[Gabriel Ebner]

I believe Mario's comment was about disambiguating names like _root_.foo where you have a def foo in the current namespace.

[Daniel Selsam]

Gabriel Ebner said:

There's another reason to use the global namespace though. And that's dot-notation. For that you need to put declarations in the same namespace as the original definition.

But that is just a few files that wouldn't need to be in the mathlib namespace.

[Gabriel Ebner]

There's already 31 files that contain namespace list and I didn't even count other types from core. If half of mathlib is in the root namespace, then adding Mathlib. to the seems to be more of a hassle than it's worth.

[Daniel Selsam]

What about

register_dot `Mathlib.list `list

[Daniel Selsam]

The main concern is people who depend on mathlib. Python would be a mess if you had to from tensorflow import *; from numpy import *.

[Mario Carneiro]

For most projects that depend on mathlib, the scope will be more restricted and so it makes more sense to put everything in a namespace

[Mario Carneiro]

but mathlib is a monorepo, it has a huge variety of things and aims to be both the standard library for lean 3 and the convergence of almost all public work on lean 3

[Mario Carneiro]

Kevin Buzzard said:

Isn't this pretty normal in stuff like python? The only difference would be that mathlib users would just write open mathlib at the start of their code and mathlib developers would write namespace mathlib at the start of theirs. Or am I being naive?

Most of mathlib's category theory library is built on this premise. If you search for uses of category_theory. you will see that it leaks quite a bit

[Daniel Selsam]

Mario Carneiro said:

Kevin Buzzard said:

Isn't this pretty normal in stuff like python? The only difference would be that mathlib users would just write open mathlib at the start of their code and mathlib developers would write namespace mathlib at the start of theirs. Or am I being naive?

Most of mathlib's category theory library is built on this premise. If you search for uses of category_theory. you will see that it leaks quite a bit

This suggests a spectrum/middle-ground, where mathlib doesn't use Mathlib namespace but perhaps as necessary other modules within mathlib could use namespaces (like category_theory does now).

[Mario Carneiro]

sure, that's what we already do

[Scott Morrison]

One reason the category theory development is mostly in the category_theory namespace is because there is this strange version of functor that someone left lying around in the root namespace. :-) It doesn't satisfy any laws, and for some reason only works in the category Type. Must be the influence of these Haskell people. :-)