Hiding imported constants from dependent files

Stream: general

[Jannis Limperg]

So I just made an innocent PR that adds two functions to meta.expr. One of them is implemented using a parser from data.buffer.parser, so I import data.buffer.parser. Now all hell breaks loose: the global namespace of every file that (transitively) imports meta.expr now contains a constant named parser. Many of these files also open the lean namespace to shorten lean.parser, so we have a conflict.

Is there any way to get parser in meta.expr, but not propagate it to every file that imports meta.expr?

[Reid Barton]

Nope. And I don't think it makes much sense to have init.* modules importing non-init ones.

[Jannis Limperg]

Ah, I meant mathlib's meta.expr. But I suppose this changes little.

[Reid Barton]

Ohh, I didn't realize that existed but that does make more sense.

[Yury G. Kudryashov]

I guess a proper fix is to move the offending global definition to a namespace in stdlib

[Jannis Limperg]

I guess I can suggest that. Don't think anyone else actually uses parser. But the proper proper fix would be to have a less primitive module system. :lucky: