Mathlib Vector namespace

Stream: mathlib4

[Shreyas Srinivas]

Hi all,

With batteries#793 and follow-up PRs, batteries will acquire acquire an extensive Vector API. This means Mathlib's Vector will need to be either renamed or namespaced. I want to ask what your preferred solution would be. Once a decision is reached, I will start a Mathlib PR.

[Eric Wieser]

Another answer is to delete all the definitions with clashing names, and deprecate everything else.

[Eric Wieser]

List.Vector might be an ok name if we decide to keep it as is

[Kim Morrison]

My preference is to delete as much as possible, and deprecate everything else.

[Eric Wieser]

What are you imagining as being in the set of things that are kept but deprecated, in the scenario where we delete as much as possible?

[Mario Carneiro]

I don't really think that Batteries.Vector is a replacement for basically any of the uses of Mathlib.Vector (to the extent it has uses at all). It's used for proving purposes, I don't know any use of it in a programming context

[Mario Carneiro]

So I'm skeptical that deprecation is the right move

[Kim Morrison]

What would you recommend we do with the Mathlib material?

I'm not thrilled with just leaving it as is in the root namespace.

[Mario Carneiro]

namespace it in Mathlib or List, slight preference for the latter

[Eric Wieser]

Doesn't namespacing things mean we need to deprecate the old un-namespaced names (where we can)?

[Eric Wieser]

The compatibility-conscious thing to do here would be to:

• Add a namespace to everything, and deprecate the un-namespaced names now
• wait N days
• remove the deprecations and accept the Batteries change

[Eric Wieser]

Or:

• Call the batteries change Std.Vector or Array.Vector, merge it soon
• Do a slow deprecation / rename shuffle over a longer period

[Frédéric Dupuis]

Mario Carneiro said:

I don't really think that Batteries.Vector is a replacement for basically any of the uses of Mathlib.Vector (to the extent it has uses at all). It's used for proving purposes, I don't know any use of it in a programming context

Is there anything about the Array-based version being introduced in Batteries that would make it unsuitable for proving?

[Mario Carneiro]

no, but if you didn't need Array to begin with it's an unnecessary indirection

[Mario Carneiro]

If I'm doing some abstract CS and am using lists in a nested inductive or similar and use List.Vector for packing up that data when the length of the list is relevant (e.g. well scoped terms in a context), I don't think Array.Vector would be a welcome replacement

[Shreyas Srinivas]

I am not sure it is wise to call the namespace List or Array

[Shreyas Srinivas]

Firstly, it might contain identically named List functions

[Shreyas Srinivas]

And secondly I have to open List.Vector or Array.Vector on top of List or Array to get things running

[Shreyas Srinivas]

The reason for namespacing is that both Batteries and Mathlib will soon have a vector and name spacing them avoids name conflicts

[Shreyas Srinivas]

Eric: the issue with the second solution is that as long as mathlib.vector remains in the root namespace, opening the Batteries namespace will lead to ambiguity

[Shreyas Srinivas]

I might want to use parts of mathlib with Vector

[Mario Carneiro]

And secondly I have to open List.Vector or Array.Vector on top of List or Array to get things running

I don't know what you mean by this. You only need to open List to be able to use List.Vector as Vector

[Shreyas Srinivas]

There is a Vector namespace for Vector functions

[Shreyas Srinivas]

Similar to Array

[Mario Carneiro]

If there is List.Vector.append then you can use dot notation and not open anything, or open List and use Vector.append; you probably don't want to open List.Vector anyway but if you did you would be able to use just append (except not really since it's almost certainly protected anyway)

[Shreyas Srinivas]

I don't have a strong opinion on the namespace names. My reasoning is that the namespaces are a reflection of two identically named entities in different libraries. So the library name should be used for namespaces. There is already the Std namespace in core for example.

[Shreyas Srinivas]

I do think both Vectors ought to be namespaced

[Shreyas Srinivas]

Apart from giving us the choice of which Vector to keep hidden, it also meets the FROs desire to not have a _root_.Vector

[Shreyas Srinivas]

Of course the best systemwide long term solution to this is a system of qualified imports with a hiding keyword to remove specific names like Haskell.

[Mario Carneiro]

These are different structures, the name clash is historical happenstance

[Mario Carneiro]

Namespacing is definitely going to happen, the question is only to what name and how to perform the rename/deprecation

[Shreyas Srinivas]

On second thoughts, I like your namespace name choice, because Mathlib.Vector belongs in batteries

[Shreyas Srinivas]

I suggest going ahead with my plan from yesterday where both Vectors get thrown into a different namespace and the PRs get merged

[Shreyas Srinivas]

This buys us time to think about any renaming/deprecation stuff later

[Eric Wieser]

We can't throw the mathlib Vector into a namespace without thinking about deprecations at the same time

[Shreyas Srinivas]

Why?

[Mario Carneiro]

the point of deprecation is to ensure some continuity for people using the original name

[Shreyas Srinivas]

Oh right

[Eric Wieser]

However, you can put the batteries one in a namespace immediately (because it isn't in main yet)

[Kim Morrison]

Yes please, it's essential the new one is namespaced as Batteries.Vector.

[Shreyas Srinivas]

Okay, batteries.vector it shall be

[Eric Wieser]

Kim Morrison said:

Yes please, it's essential the new one is namespaced as Batteries.Vector.

Is this strongly preferable to Array.Vector from the FRO's perspective?

[Eric Wieser]

The upside of that spelling is that names don't have to change downstream if this is upstreamed to core/Std

[Kim Morrison]

Yes, Batteries.Vector is our preference.

[Shreyas Srinivas]

Done

[Shreyas Srinivas]

What's the preference for the mathlib version of Vector?

[Shreyas Srinivas]

@Mario: about this:

Mario Carneiro said:

If I'm doing some abstract CS and am using lists in a nested inductive or similar and use List.Vector for packing up that data when the length of the list is relevant (e.g. well scoped terms in a context), I don't think Array.Vector would be a welcome replacement

For proof purposes, the Array implementation contains a list. The mathlib vector's list based lemma interface could simply rely on this. It is how I initially started that batteries PR, so I am quite sure the adaptation works.

[Yaël Dillies]

Can we not simply delete it? (after deprecation if you insist)

[Shreyas Srinivas]

My understanding is Mario doesn't want to deprecate anything

[Shreyas Srinivas]

A list based vector has some potential uses, but I don't see why there need to be two different defs. For proof purposes Arrays have a field called data of type List

[Shreyas Srinivas]

That being said, we can think about this separately form that batteries PR now that there are no conflicts.

[Yaël Dillies]

Can we at least get rid of docs#Vector3 ?

[Shreyas Srinivas]

That's probably a separate topic. I would still like Mathlib's vector to go into a namespace as well, because importing various bits and pieces of Mathlib automatically brings in Vectors, which means I can't open the Batteries namespace without getting into trouble.

[Shreyas Srinivas]

It is not convenient to have long names because of the Batteries. prefix : Fixed this

[Mario Carneiro]

Shreyas Srinivas said:

My understanding is Mario doesn't want to deprecate anything

Deprecation implies that there is some equivalent replacement, and Batteries.Vector is not a replacement for Mathlib's Vector. If Mathlib namespaces Vector (and see no one saying it shouldn't), then the deprecation is regarding moving to mathlib's new name, not to Batteries.Vector.

[Mario Carneiro]

Code using mathlib's vector may or may not want to switch to using Batteries.Vector, but that's not a migration path, that's a similar level of complexity as replacing List with Array in a function (which is to say, actually quite complicated because you need to use different functions now if you don't want to write terrible code)

[Mario Carneiro]

cc: @Eric Wieser There is a reason not to deprecate Vector though during the mathlib move and just move it without a deprecation alias, which is that even a deprecated alias will cause interference with using Vector while Batteries is open.

[Shreyas Srinivas]

So there is no easy migration path

[Eric Wieser]

Mario Carneiro said:

cc: Eric Wieser There is a reason not to deprecate Vector though during the mathlib move and just move it without a deprecation alias, which is that even a deprecated alias will cause interference with using Vector while Batteries is open.

I think there's a missing feature here of a global open _root_ hiding Vector that does what you'd expect

[Shreyas Srinivas]

You can rename it to something else which is effectively hiding it

[Shreyas Srinivas]

I don't know if it works for _root_ though

[Shreyas Srinivas]

Because technically _root_ is already open

[Shreyas Srinivas]

I got to a machine and tried this out. Apparently _root_ is not something I can access with open. Maybe the default namespace needs to have an accessible name? I get "unknown namespace _root_" as an error though of course I can use _root_ to access everything:

import Mathlib.Data.Vector

#check _root_.Vector -- works

open _root_ renaming Vector → Vec --error

[Shreyas Srinivas]

Have we reached a conclusion on how to namespace Mathlib's vector and give users a safe migration path?

[Shreyas Srinivas]

I already namespaced the batteries version

[Kim Morrison]

I would suggest moving Vector to Mathlib.Vector, and add deprecation aliases. We can, if necessary, do an unusually short deprecation cycle.

[Shreyas Srinivas]

To make sure I understand, you would like me to :

1. Keep batteries#793 as it is.
2. Create a new mathlib PR with its contents inside the Batteries namespace
3. Move Mathlib Vector into Mathlib namespace.
4. Create deprecation aliases from root namespace to the Mathlib namespaced List Vector
5. Get the Mathlib PR accepted.
6. Then at the end of a short deprecation cycle, add another PR to Mathlib which points the alias to batteries.vector and make this new PR dependent on batteries #793.
7. Merge the second mathlib PR and batteries#793 together.

[Shreyas Srinivas]

I think step2 in this is not necessary

[Shreyas Srinivas]

1. We can simply namespace Mathlib Vector and add deprecation aliases at the root namespace in a mathlib PR.

2. We can independently merge batteries#793 because it is behind a namespace.

3. We eventually remove the deprecation aliases in mathlib vector and free up the root namespace

[Shreyas Srinivas]

That way, we keep both vectors as Mario wants

[Shreyas Srinivas]

And there are fewer interdependent steps

[Kim Morrison]

I don't understand step2, so I guess I agree it is not necessary.

[Kim Morrison]

I think steps 3.4.5 are good and should be done before anything else.

[Kim Morrison]

I either don't understand 6, or if I do, don't think it should be done. Just leave the _root_.Vector aliases forwarding to Mathlib.Vector.

[Shreyas Srinivas]

Steps 6 and 7 are also not necessary

[Shreyas Srinivas]

I initially thought you wanted me to move my existing Batteries PR to mathlib, but now I see that the you are suggesting my second series of steps.

Shreyas Srinivas said:

1. We can simply namespace Mathlib Vector and add deprecation aliases at the root namespace in a mathlib PR.

2. We can independently merge batteries#793 because it is behind a namespace.

3. We eventually remove the deprecation aliases in mathlib vector and free up the root namespace

[Kim Morrison]

What is necessary before batteries#793 can be merged is a that there exists a batteries-pr-testing-793 branch on Mathlib demonstrating that we can update Mathlib to use the branch, so there is no delay after batteries#793 is merged before Mathlib can bump to the new batteries main. That branch should have an open PR attached to it, and that needs approval from a Mathlib maintainer.

[Shreyas Srinivas]

Okay. I assume this is done by adding the last commit ID of the batteries PR to the mathlib lakefile and manifest?

[Shreyas Srinivas]

PR #13407: for namespacing Vector and adding deprecation aliases

[Kevin Buzzard]

Thanks! Remember to tag it awaiting-review when it's ready.

[Shreyas Srinivas]

One question:

1. Is there a label that stops CI runs when I am pushing commits that I know won't build. It seems wasteful to run CI for such commits.

One observation:

1. The tedious part of this PR is going over all #align because even when they are inside a namespace #align seems to require fully qualified names. This could come up when more parts of Mathlib get namespaced.

[Kim Morrison]

Don't worry about CI resources; for now there are plenty, and when you push it automatically cancels any running builds on the same branch.

[Shreyas Srinivas]

Questions about adding deprecated annotations:

1. Is there a way to add a string letting users know that Vector will now be available in namespace Mathlib.
2. Should every lemma, theorem, and def receive a deprecated alias in the entire Vector folder?

[Shreyas Srinivas]

Although the CI is currently still building my last commit, I am certain that at least the build part of CI will pass on this commit. This leaves maybe lint issues and the addition of deprecated tags.

[Eric Wieser]

Kim Morrison said:

What is necessary before batteries#793 can be merged is a that there exists a batteries-pr-testing-793 branch on Mathlib demonstrating that we can update Mathlib to use the branch, so there is no delay after batteries#793 is merged before Mathlib can bump to the new batteries main. That branch should have an open PR attached to it, and that needs approval from a Mathlib maintainer.

@Shreyas Srinivas, I think it might make more sense to do this first, rather than worrying about deprecations first

[Shreyas Srinivas]

On it. But these are independent

[Shreyas Srinivas]

When I do lake update batteries after changing the revisions, I get error: external command 'git' exited with code 128

[Shreyas Srinivas]

Fixed it.

[Shreyas Srinivas]

PR #13415

[Shreyas Srinivas]

Update

1. PR #13407 namespaces Vector in mathlib. CI passes :check: . deprecations yet to be added. See my earlier questions.
2. PR #13415 tests Mathlib on top of batteries#793 and passes CI :check:

[Kim Morrison]

Shreyas Srinivas said:

Questions about adding deprecated annotations:

1. Is there a way to add a string letting users know that Vector will now be available in namespace Mathlib.
2. Should every lemma, theorem, and def receive a deprecated alias in the entire Vector folder?

1. No. 2. I think it's actually fine to just deprecate the type. You can't use any of the results without hitting the warning about the type itself.

[Kim Morrison]

Use @[deprecated Mathlib.Vector]. This tells the user what to replace it with.

[Eric Wieser]

Maybe deprecate the type with @[deprecated Mathlib.Vector "Vector is now Mathlib.Vector. Use `open Mathlib (Vector)` to fix your old code"] or something

[Eric Wieser]

Not deprecating all the lemmas means that there's no code action for the replacement, but if we tell the user to use open Mathlib (Vector) then we don't need a code action anyway

[Kim Morrison]

Oh, apparently I am wrong about 1.

[Eric Wieser]

I apparently cannot read and did not see that 1 was being asked

[Eric Wieser]

I think there's a quirk here where the code action doesn't work if you use the string argument

[Eric Wieser]

But that's probably just a bug that can be fixed separately

[Eric Wieser]

Maybe I'm imagining the code action...

[Yaël Dillies]

Yeah, the code action is rotting in one of Damiano's PRs

[Eric Wieser]

It's very unfortunate that Damiano found time to make all these great automation PRs around the same time I lost much of my review time...

[Shreyas Srinivas]

Done.

[Shreyas Srinivas]

I have put the awaiting CI tag, but I think the changes can be reviewed even if the CI isn't finished

[Shreyas Srinivas]

One file that gave me slightly extra trouble was the Vector namespace part of Topology/List.Lean

[Shreyas Srinivas]

Which was a surprising thing, because after opening Mathlib namespace and despite already being inside the Vector namespace, certain commonly named functions were being interpreted as List functions. I fixed it by adding Vector. namespace prefix to the relevant function calls.

[Richard Copley]

Eric Wieser said:

I think there's a quirk here where the code action doesn't work if you use the string argument

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/machineApplicableDeprecated.20tag.20attribute/near/397630086

[Shreyas Srinivas]

Uh... help needed. It seems adding this deprecation alias triggered an avalance of errors arising from "possible ambiguous interpretations"

[Shreyas Srinivas]

and also a host of warnings wherever Vector is used even if I opened the namespace, because of course _root_.Vector has been deprecated

[Shreyas Srinivas]

It seems opening the namespace might have been a bad idea although not doing so means long names

[Shreyas Srinivas]

The straightforward solution for now is to "not" open these names and be okay with prefixes everywhere Vector and its theorems are used.

[Shreyas Srinivas]

I am hoping there is something less painful and more elegant

[Shreyas Srinivas]

I somehow thought alias would automatically handle this issue.

[Mario Carneiro]

This is the issue I was referring to earlier:
Mario Carneiro said:

cc: Eric Wieser There is a reason not to deprecate Vector though during the mathlib move and just move it without a deprecation alias, which is that even a deprecated alias will cause interference with using Vector while Batteries is open.

[Shreyas Srinivas]

What's the fix to be applied now? Should I find every occurrence of a Vector or Vector lemma and explicitly prefix it?

[Mario Carneiro]

you should be able to use open Mathlib (Vector) after namespacing it

[Shreyas Srinivas]

That's what I am doing now

[Shreyas Srinivas]

Oh wait, does putting (Vector) in brackets supersede root.Vector?

[Mario Carneiro]

oh right, you have root.Vector too because of the alias

[Mario Carneiro]

yeah I think it would be better to just not deprecate-rename

[Eric Wieser]

I guess a really dumb solution would be to add VectorIsGone as an alias

[Eric Wieser]

And then at least autocomplete would find it

[Shreyas Srinivas]

That serves no purpose

[Mario Carneiro]

autocomplete will find Mathlib.Vector already

[Mario Carneiro]

I would really like to make alias be more of a name resolution hint a la open

[Mario Carneiro]

so that it doesn't cause conflicts with itself

[Eric Wieser]

image.png

[Mario Carneiro]

it's there just below

[Eric Wieser]

I'm confused, this seems to work fine:

axiom Mathlib.Bar : Type

@[deprecated] abbrev Bar := Mathlib.Bar

open Mathlib (Bar)

#check Bar

[Eric Wieser]

Oh, this is just #check being weird

[Shreyas Srinivas]

Namespaces are weird.

[Shreyas Srinivas]

When I open Mathlib and there is a downstream open Vector, all the Vector defs work perfectly fine.

[Shreyas Srinivas]

If instead I do open Mathlib (Vector) and then open Vector, that somehow makes lean not capable of recognising the Vector functions right under this open Vector.

[Shreyas Srinivas]

To see what I mean, open the PartRec Computability/Halting.lean file in the latest commit of my PR. Change the open Mathlib to open Mathlib (Vector).

[Shreyas Srinivas]

Found a fix: The fix is to change open Vector to open Mathlib.Vector

[Shreyas Srinivas]

Mario Carneiro said:

yeah I think it would be better to just not deprecate-rename

Followed this. PR #13407 passes CI :check: and is ready for review

[Shreyas Srinivas]

Hi I need some help with git. I took PR #13407 out of merge conflict today. This unfortunately added a large number of commits from the last two weeks. How do I squash them or get rid of them. Obviously I didn't touch 2000 files with this PR, but it did affect some two dozen files. This PR has a high chance of running into merge conflicts.

[Shreyas Srinivas]

Update : Resolved the merge conflict issues and the extra commit issues with some resets and merges. This PR is ready for review. Since it touches some 25 files, I request and hope this PR can be processed faster since this PR is much more likely to have merge conflicts than most PRs