Zulip Chat Archive

Stream: general

Topic: Hiding imported constants from dependent files

Jannis Limperg (Oct 08 2020 at 15:42):

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 (Oct 08 2020 at 15:48):

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

Jannis Limperg (Oct 08 2020 at 15:54):

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

Reid Barton (Oct 08 2020 at 16:01):

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

Yury G. Kudryashov (Oct 08 2020 at 20:38):

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

Jannis Limperg (Oct 08 2020 at 22:44):

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:

Last updated: Aug 03 2023 at 10:10 UTC