Zulip Chat Archive

Stream: new members

Topic: Vector namespace


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Dan Stanescu (May 18 2020 at 22:25):

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

view this post on Zulip Dan Stanescu (May 18 2020 at 22:25):

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

view this post on Zulip Bryan Gin-ge Chen (May 18 2020 at 22:25):

Just making sure, did you import data.vector?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:52):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 18 2020 at 22:53):

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

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:53):

I only learnt about this phenomenon recently.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 19 2020 at 04:46):

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

view this post on Zulip Mario Carneiro (May 19 2020 at 04:47):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 19 2020 at 04:48):

How hard do we need that feature?

view this post on Zulip Mario Carneiro (May 19 2020 at 04:49):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 19 2020 at 07:19):

wouldn't VSCode complain about duplicated imports?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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: May 18 2021 at 16:25 UTC