Namespacing Mathlib

Stream: mathlib4

[Ruben Van de Velde]

But what with all the code you're upstreaming to core?

[Thomas Murrills]

I have a rough design for project namespacing that I think has reasonable ergonomics (which imo is the biggest problem/obstacle; the friction with namespacing is real):

project-wide namespacing

• introduce a project-wide setting to open namespaces in the lakefile—downstream repos would e.g. be able to open the namespaces of their dependencies
  • new math projects would open Mathlib project-wide by default
  • this needs an escape hatch: the ability to close or hide these namespaces on demand in specific files

and the dual of that:

• a project-wide setting to automatically namespace all top-level declarations by the project name (which would be the default for all new projects). this would be like living in the namespace MyProject for the most part (and turn def foo into MyProject.foo ), except when…
  • …you use a namespace that exists at the root level, e.g. def Array.newOp (which should not become MyProject.Array.newOp)
  • …your pre-project-namespaced declaration conflicts completely with an existing def at the root level (e.g. if foo already exists at the root level, then to prevent confusion, you need to write def MyProject.foo explicitly instead of just def foo, or face an error/warning)
  • And _root_ would behave as usual, bringing you to the “true root” and disabling any project namespacing.

[Thomas Murrills]

(We should probably move these messages, though...)

[Kim Morrison]

Ruben Van de Velde said:

But what with all the code you're upstreaming to core?

Could you clarify, I don't understand. I'm not proposing that anything about Nat/Int/List/Array in Mathlib or Batteries would be in namespaces. Just everything not defined in lean4.

[Thomas Murrills]

It looks like my attempt to make this conversation read reasonably upon moving messages didn't work. :) For those just joining us, this thread began in #mathlib4 > Linter for overlapping instances with
Alex Meiburg said:

the biggest crime in that list [of declarations with overlapping instance hypotheses] is having a declaration simply known as docs#impl

Kim Morrison said:

My fault! :-) At least it is already deprecated.

Can I say again: please, please, can we namespace Mathlib? :-)

[Notification Bot]

4 messages were moved here from #mathlib4 > Linter for overlapping instances by Thomas Murrills.

[Jon Eugster]

I'd love a namespaced mathlib! I think it would suffice to simply add namespace Mathlib to most files (except the ones which should live in a namespace from somewhere else as mentioned. Requiring downstream projects to open Mathlib in their files seems perfectly acceptable to me.

@Thomas Murrills, on first thought, your suggestion sounds a bit like overcomplicating things, though I might be missing something.

[Thomas Murrills]

There’s long been pushback to namespacing Mathlib (in previous conversations on this topic) based in part on the friction involved in asking every math project to write open Mathlib in their files before anything works; these sorts of boilerplate commands are an ergonomic pain point that programmers have by and large accepted as a fact of life, but they’re simply not great UX. And for new users such as mathematicians new to lean who have not accepted these pain points as inevitable, UX issues like that can be a big turn-off. :)

[Thomas Murrills]

Another point often brought up is that the Mathlib version of these declarations aims to be the canonical version. This at least still functions as the case for math projects if they automatically “buy in” to the Mathlib namespace.

[Thomas Murrills]

So, I’m making this rough proposal to try to satisfy both sides of that debate, and let us get the benefits of namespacing without the issues that provoke resistance. :)

[Chris Henson]

As a datapoint from downstream, I've been mostly happy with our decision to fully namespace CSLib and enforce this with an environment linter. The biggest annoyance from my perspective has been that scoped notations don't appear in documentation. (And we scope all notations in compliance with the linter!). I also think it is polite to scope grind annotations in your library's namespace, but Mathlib doesn't seem to use scoped grind. Maybe this is not so important though if the upcoming grind equivalent of simp sets becomes the preferred way to group grind rules.

I've not carefully thought through your proposal, but I think there is something to the idea of having a special relationship to the current project's namespace. You could easily argue however that implicit rules like this are also confusing to new users.

[Violeta Hernández]

I mostly view the CGT repo as an extension of Mathlib with material that the maintainers would not be able to otherwise review. I like that we can keep e.g. surreal numbers in the same namespace as everything else. A namespace would just be drawing an arbitrary division, in my view.

[Tomas Skrivan]

Thomas Murrills said:

Another point often brought up is that the Mathlib version of these declarations aims to be the canonical version. This at least still functions as the case for math projects if they automatically “buy in” to the Mathlib namespace.

On the other hand, I have a library for numerical linear algebra for which I would like to write a spec with mathlib. However, the library has a very different idea of what the canonical Matrix type is and mathlib prevents me from defining my matrix type as MyLibrary.Matrix because after open MyLibrary I get an ambiguous symbol for Matrix.

[Tomas Skrivan]

Can't we have a Mathlib namespace and every project including mathlib will automatically open the namespace? And you can turn this off with a setting in the lakefile.

[Chris Henson]

Violeta Hernández said:

I mostly view the CGT repo as an extension of Mathlib with material that the maintainers would not be able to otherwise review. I like that we can keep e.g. surreal numbers in the same namespace as everything else. A namespace would just be drawing an arbitrary division, in my view.

I think if you chose to do so, you could still make everything CGT fall under the Mathlib namespace? I don't think it has to force any division.

[Violeta Hernández]

Assuming that we do namespace Mathlib, and that we ever get downstream users from CGT, I think that's what I'd like to do.

[Kevin Buzzard]

If I recall correctly, writing NNG was also a pain because mathlib's stuff wasn't namespaced (but I can't remember the details); again this is an example where you want to do things using big chunks of mathlib (e.g. its tactics) but without using all of it (e.g. its lemmas about Nat, which you are to reprove).

I am torn between "mathlib is the true way to do mathematics and if you are depending on mathlib then you buy into this" and "there are situations where you both want to import mathlib and also do some stuff your own way". I think I alternate between these two beliefs, which lead to contradictory conclusions about whether mathlib should be namespaced.

[Yaël Dillies]

What if one could import the content of a library into a namespace? Then I don't think anyone would complain anymore

[Kim Morrison]

Yaël Dillies said:

What if one could import the content of a library into a namespace? Then I don't think anyone would complain anymore

This wouldn't work for Mathlib, where we add lots of material in the Nat/List/etc namespaces. It's also a big and complicated RFC. It's fine to think about how we could achieve this in the long term, but I don't think we should let this distract us from thinking about namespacing today.

[Thomas Murrills]

Tomas Skrivan said:

Can't we have a Mathlib namespace and every project including mathlib will automatically open the namespace? And you can turn this off with a setting in the lakefile.

My rough draft above takes this as a starting point; the problem with only doing it like is that there's currently no way to close a namespace like that! These rough edges are what I'm trying to figure out there. (But I'm sure I haven't thought of all of them.)

Also, it would be nice to think about going in the other direction: the ergonomics of making your whole project properly namespaced introduces some friction. It'd be nice if project-wide namespacing was ergonomic enough to be the standard, not just a Mathlib thing, and I don't think it's too hard.

We can attack this problem incrementally instead of all at once, though.

[Siddhartha Gadgil]

Thomas Murrills said:

There’s long been pushback to namespacing Mathlib (in previous conversations on this topic) based in part on the friction involved in asking every math project to write open Mathlib in their files before anything works; these sorts of boilerplate commands are an ergonomic pain point that programmers have by and large accepted as a fact of life, but they’re simply not great UX. And for new users such as mathematicians new to lean who have not accepted these pain points as inevitable, UX issues like that can be a big turn-off. :)

Since users need to begin with import Mathlib asking addition of open Mathlib is not a big addition.

[Shreyas Srinivas]

Siddhartha Gadgil said:

Since users need to begin with import Mathlib asking addition of open Mathlib is not a big addition.

This was my argument as well. In Thomas’s proposal it would be nice if specific declarations could be hidden.

[Shreyas Srinivas]

Usually my situation is, I want to use pieces of mathlib and ignore others. So my best case solution would be to open Mathlib (-<clashing_decl_1>, -<clashing_decl_2>).

In other situations I might want to give the Mathlib an alternative name instead of just opening it. open Mathlib as M

[Jovan Gerbscheid]

I think it would be very inconvenient if every #wme had to include an extra open Mathlib line, and all previous existing MWEs in this channel became invalid because of a missing open Mathlib

[Snir Broshi]

MWEs can already become invalid when Mathlib updates when stuff are renamed/moved/deleted/etc

[Snir Broshi]

Maybe live-lean can support something like --! Mathlib v4.26.0 or --! Lean v4.1 at the start to make it switch to the corresponding version, and the mathlib one can automatically import+open mathlib.
Then we can add a "copy" button that automatically adds this comment with the current version.

[Thomas Murrills]

Siddhartha Gadgil said:

Since users need to begin with import Mathlib asking addition of open Mathlib is not a big addition.

It increases boilerplate necessary for Mathlib by factor of 2! :grinning_face_with_smiling_eyes:But, unironically, having to point to Mathlib not once but twice in every file is qualitatively different imo, and enough to make it feel worse.

[Lua Viana Reis]

What if there was a way to import a module inside a namespace, like import Module qualified as MyNamespace in Haskell?

[Lua Viana Reis]

Yaël Dillies said:

What if one could import the content of a library into a namespace? Then I don't think anyone would complain anymore

oops, sorry, Yaël had already suggested that

[Lua Viana Reis]

Kim Morrison said:

This wouldn't work for Mathlib, where we add lots of material in the Nat/List/etc namespaces. It's also a big and complicated RFC. It's fine to think about how we could achieve this in the long term, but I don't think we should let this distract us from thinking about namespacing today.

This is very interesting to think about, the following example works:

namespace Foo

def List.foolen (l : List α) := l.length

end Foo


open Foo

#eval [1, 2].foolen

My expectation would be that when using import Mathlib qualified as Math, then the material added to Nat/List/... would only be available in the current module after open Math, which seems to be more or less how Lean behaves now

[Lua Viana Reis]

can you clarify in what sense it wouldn't work for Mathlib?

[Thomas Murrills]

One thing that'd have to be figured out there is what happens with diamond-like imports (i.e. I import a module which imports mathlib under a namespace, and one which doesn't. What do I see?). If we were to go this route, maybe importing-as-a-different-namespace could be a change local to that module, or only local to a project (and not its downstream repos), or something?

[Thomas Murrills]

Lua Viana Reis said:

This is very interesting to think about, the following example works:

Whoa, this is pretty surprising to me!

[Jovan Gerbscheid]

The really annoying thing is that you need the open Foo. Just namespace Foo is not enough:

namespace Foo
open Foo -- this is necessary

def List.foolen (l : List α) := l.length

#eval [1, 2].foolen

[Lua Viana Reis]

Thomas Murrills said:

Whoa, this is pretty surprising to me!

I like that it works that way :slight_smile: and if import qualified is to import all the declarations inside a namespace, then it's even better, as someone could complain of Mathlib polluting the Nat namespace inasmuch as the root namespace.

[Lua Viana Reis]

it just makes it obvious that l.foolen is syntactic sugar for List.foolen and not a "field" of the object l

[Shreyas Srinivas]

@Lua Viana Reis : in principle that’s similar to what I am asking. I want to have qualified opening of namespaces. The flaw in your specific suggestion is that lean doesn’t use module names as namespaces unlike Haskell. Namespaces and modules are pretty much orthogonal concepts in lean unlike Haskell. Also I recall from one year old discussions that lean absolutely needs imports to be on top of the file.

[Lua Viana Reis]

What do you mean by it being a flaw? And if I understand what you wrote, then you are asking to put Mathlib inside a namespace but add an option to rename the namespace, which is quite different from what I and Yaël suggested?

[Shreyas Srinivas]

The latter is not feasible in lean. I don’t recall why but the imports of a file are always processed first.

EDIT: I am responding to Yael’s suggestion to import inside a namespace.

[Shreyas Srinivas]

About the former: you ask for qualified imports but lean doesn’t namespace files under module names. So you want qualified opening of namespaces.

[Lua Viana Reis]

Shreyas Srinivas said:

EDIT: I am responding to Yael’s suggestion to import inside a namespace.

The suggestion is to define a different syntax for a import statement that is elaborated differently. "Wrapping" around a namespace of course doesn't (and wouldn't) work

[Lua Viana Reis]

The idea is the imported file would be compiled as if there was no namespace around it, but the constants it defined would be imported into the current module's environment with the namespace prefix (or somehow hidden and aliased). I'm also not claiming that this is simple to implement