Zulip Chat Archive

Stream: new members

Topic: Vector namespace


Dan Stanescu (May 18 2020 at 22:21):

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 (May 18 2020 at 22:24):

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

Dan Stanescu (May 18 2020 at 22:25):

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

Dan Stanescu (May 18 2020 at 22:25):

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

Bryan Gin-ge Chen (May 18 2020 at 22:25):

Just making sure, did you import data.vector?

Dan Stanescu (May 18 2020 at 22:26):

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

Kevin Buzzard (May 18 2020 at 22:52):

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

Kevin Buzzard (May 18 2020 at 22:53):

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

Mario Carneiro (May 18 2020 at 22:53):

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

Kevin Buzzard (May 18 2020 at 22:53):

I only learnt about this phenomenon recently.

Mario Carneiro (May 18 2020 at 22:54):

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 (May 18 2020 at 22:54):

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

Johan Commelin (May 19 2020 at 04:46):

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

Mario Carneiro (May 19 2020 at 04:47):

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

Mario Carneiro (May 19 2020 at 04:48):

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 (May 19 2020 at 04:48):

How hard do we need that feature?

Mario Carneiro (May 19 2020 at 04:49):

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

Gabriel Ebner (May 19 2020 at 07:18):

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 (May 19 2020 at 07:19):

wouldn't VSCode complain about duplicated imports?

Gabriel Ebner (May 19 2020 at 07:25):

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 (May 19 2020 at 07:32):

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 (May 19 2020 at 07:33):

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 (May 19 2020 at 07:36):

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


Last updated: Dec 20 2023 at 11:08 UTC