Vector namespace

Stream: new members

[Dan Stanescu]

There is a vector namespace in lean/library/data/vector.lean which I've been trying to open with no success:

open vector --> invalid namespace name 'vector'

Anyone can point me to what I could be doing wrong here?

[Kevin Buzzard]

I've not looked at the file but are you sure the namespace exists? That's different to the vector type existing

[Dan Stanescu]

I'm looking at the namespace, line 16 in the file.

[Dan Stanescu]

I just can't seem to be able to use vector in any way.

[Bryan Gin-ge Chen]

Just making sure, did you import data.vector?

[Dan Stanescu]

This may be it. I only tried import vector.
Yes, that is it!
Thanks @Bryan Gin-ge Chen

[Kevin Buzzard]

Aah -- so this file is in core but not imported automatically!

[Kevin Buzzard]

I think everything in lean/library/init is imported when you start Lean up, but perhaps other things are not.

[Mario Carneiro]

yes... and as a result the mathlib version has the awkward name data.vector2

[Kevin Buzzard]

I only learnt about this phenomenon recently.

[Mario Carneiro]

More precisely, any file not starting with prelude has an implicit import init at the start, which does the same thing as actually typing import init in your file. That is, it looks for init.lean or init/default.lean in the search path

[Mario Carneiro]

but lean core has laid claim to that file already so mathlib can't supply it, unfortunately

[Johan Commelin]

Guess why I dumped all the algebra stuff in a folder called init_ :wink:

[Mario Carneiro]

I've been wondering what a good alternative here would be for finding multiple inits

[Mario Carneiro]

for example, we could change import semantics such that if there are multiple matches for a given name, lean imports all of them instead of just a random one. Then mathlib could also have an init file, and both would get imported on an empty input

[Johan Commelin]

How hard do we need that feature?

[Mario Carneiro]

It would be convenient for mathlib extensions to the tactic language, for example

[Gabriel Ebner]

So if we have mathlib/src/init/core.lean, then it would also affect core? I feel like this would cause a lot of recompilation, and I wouldn't even know where to put the oleans for the mathlib-modified core.

[Kenny Lau]

wouldn't VSCode complain about duplicated imports?

[Gabriel Ebner]

This is a response to Mario's proposal. Even with Mario's proposal you should probably add a prelude statement to mathlib/src/init/core.lean to prevent cyclic imports.

[Mario Carneiro]

The intention was that at least files in mathlib/src/init will have prelude in them (and will have precise imports within init of both core and mathlib)

[Mario Carneiro]

but it is a good point that this will also affect non-prelude files in core unless there is some further ordering of imported libraries

[Mario Carneiro]

A simple way to dodge that problem is to remove all non-prelude files from core, though. I don't think there is anything in there currently that isn't a better fit for mathlib anyway