Zulip Chat Archive

Stream: mathlib4

Topic: porting `localized`


Mario Carneiro (Nov 17 2022 at 05:06):

Currently, Mathlib.Mathport.Syntax has an implementation of the localized command, and mathport does in fact produce localized applications when translating localized commands: example. However, Mathlib.Mathport.Syntax is not intended to be imported by mathlib4, and in most cases we want to rewrite it to use something else. So what should we do about this command? Options:

  1. Move localized into its own file and start importing it in mathlib4. This amounts to making it an official bit of syntax.
  2. Change mathport to produce the code that localized expands to, i.e. using with_weak_namespace around a scoped syntax. This is what we should do if we are deprecating it.
  3. Change mathport to just use scoped syntax without the namespace. This is closest to the code we would like people to write instead, but it is sometimes wrong if we are not in the right namespace.
  4. Refactor mathlib3 to use the current namespace as the "locale" instead of taking it as an argument. This will make option (3) a more correct course of action.

Gabriel Ebner (Nov 17 2022 at 05:15):

I think (2) is worse than what we have right now. with_weak_namespace is a mathlib extension as well btw.

Mario Carneiro (Nov 17 2022 at 05:16):

using mathlib extensions is fine, mathport is full of mathlib extensions like all the tactics we're porting

Mario Carneiro (Nov 17 2022 at 05:17):

but I grant that with_weak_namespace isn't a nice thing to ask people to write directly post-port

Gabriel Ebner (Nov 17 2022 at 05:17):

It's also a big step backwards, we now have macros so that we don't have to write useless boilerplate. Let's use them.

Mario Carneiro (Nov 17 2022 at 05:17):

okay, but is localized the right abstraction here?

Mario Carneiro (Nov 17 2022 at 05:18):

since then we have to teach people when to use localized vs local vs scoped

Gabriel Ebner (Nov 17 2022 at 05:19):

Maybe we should rename localized to scoped. Then it would be a natural generalization:

scoped notation "foo" => 42 -- scoped in current namespace
scoped[Foo] notation "foo" => 42 -- scoped in Foo namespace

Mario Carneiro (Nov 17 2022 at 05:20):

that makes sense to me. Is that Foo or current namespace + Foo?

Gabriel Ebner (Nov 17 2022 at 05:21):

It's _root_.Foo, which is more useful than current namespace + Foo. But I could also live with prepending the current namespace.

Mario Carneiro (Nov 17 2022 at 05:22):

is it possible to "resolve" a namespace? Like if you have open Lean Meta then Meta refers to namespace Lean.Meta even though you might be in namespace Std.DList or something

Gabriel Ebner (Nov 17 2022 at 05:23):

I only put the localized command in the Mathport/Syntax.lean file because I didn't want to make a new 5-line file.. If I had known that the location of the command would have such huge consequences, I would have put it in its own file.

Mario Carneiro (Nov 17 2022 at 05:24):

well I was going to move the file myself but I took the positioning (and in particular the trivial implementation) as an indicator that we hadn't yet fully settled on a course of action here

Mario Carneiro (Nov 17 2022 at 05:25):

are there circumstances where mathport should not produce a use of localized?

Gabriel Ebner (Nov 17 2022 at 05:26):

I think if scoped notation "foo" has the same effect as scoped[NS] notation "foo" then we should probably drop the unnecessary namespace attribute.

Mario Carneiro (Nov 17 2022 at 05:28):

should this scoped[NS] thing be part of attrKind in core, or a separate mathlib extension?

Mario Carneiro (Nov 17 2022 at 05:29):

the mathlib localized has a rather different syntax from attrKind, since it wraps a command rather than going inside attribute lists and such

Gabriel Ebner (Nov 17 2022 at 05:29):

It would be nicer in core. But it's certainly easier to put it in mathlib for now.

Gabriel Ebner (Nov 17 2022 at 05:30):

I have no idea if we can monkeypatch attribute [scoped[Foo] simp] bar.

Mario Carneiro (Nov 17 2022 at 05:31):

I doubt we can, without replacing half of lean 4 syntax, since attrKind is not extensible

Gabriel Ebner (Nov 17 2022 at 05:47):

Unfortunately syntax "scoped" "[" ident "]" attr : attr doesn't work either. :sad:

Mario Carneiro (Nov 17 2022 at 05:50):

Mario Carneiro said:

is it possible to "resolve" a namespace? Like if you have open Lean Meta then Meta refers to namespace Lean.Meta even though you might be in namespace Std.DList or something

Oh, it's already being resolved by the current version of with_weak_namespace Foo / localized [Foo]

Mario Carneiro (Nov 17 2022 at 05:51):

so you do have to use _root_.Foo if you want the root version

Mario Carneiro (Nov 17 2022 at 05:52):

and actually there are some mathlib examples where the locale name should really be prefixed, like this

Gabriel Ebner (Nov 17 2022 at 06:02):

Uhm, localized [Foo] expands to with_weak_namespace _root_.Foo so you don't need to write _root_ yourself.

Mario Carneiro (Nov 17 2022 at 06:02):

oh, missed that part

Kyle Miller (Nov 17 2022 at 13:47):

I think it would be nice if we port localized so that there is a special namespace for scoped notation. For example, put notation localized to Foo into Locale.Foo (or Foo.Locale). Then open_locale Foo becomes open Locale.Foo (or open Foo.Locale). This helps separate notation from other declarations in a given namespace.

Kyle Miller (Nov 17 2022 at 13:52):

There might be a better name for this than Locale. Mathlib3 uses locales for both local notation and local instances, and it might make sense to separate these into scoped notations and scoped instances with more specific names. Potential examples:

  • open_locale big_operators --> open Notation.BigOperators
  • open_locale pointwise --> open Instances.Pointwise

Mario Carneiro (Nov 17 2022 at 13:59):

Note that you can open scoped Foo to just get the notations of Foo without the declarations

Mario Carneiro (Nov 17 2022 at 14:00):

and while I don't think it currently exists, we could also have open Foo hiding scoped to do the opposite

Kyle Miller (Nov 17 2022 at 14:13):

Even with the open scoped feature, it would be good to think about logical namespaces to put notation extensions, since we have generally been careful in mathlib3 to make these be opt-in.

Mario Carneiro (Nov 17 2022 at 14:21):

I am reminded of the old eq.ops namespace from lean 2 which held some funny symbols for eq.symm, eq.trans and congr_arg

Mario Carneiro (Nov 17 2022 at 14:23):

@Floris van Doorn can probably say more about how scoped notations were organized in lean 2

Floris van Doorn (Nov 17 2022 at 15:31):

I am in favor of mixing declarations and scoped notation in the same namespace. So open TopologicalSpace gives you both the declarations in that namespace, and all the scoped notation in that namespace. Of course, we might have a few "notation namespaces" that happen to have only scoped notation and no declarations in them (like BigOperators and Pointwise), but other than that I think we can mix them.

In Lean 2 it also worked like that. We indeed had the weird eq.ops namespace with some (scoped) notation, but (at least in the HoTT library) we generally mixed notation and declarations.

Yaël Dillies (Nov 17 2022 at 18:55):

Another one would be FinsetFamily.

Mario Carneiro (Nov 17 2022 at 19:02):

I implemented most of the stuff mentioned in this thread in mathport. With that I have a refactor request: mathport now handles the case where a localized command uses the same name as the namespace you happen to be in specially, so it would be good to make sure mathlib is using this style wherever possible.

localized "notation `foo` := bar" in boo   -- bad
namespace boo
...
namespace boo
localized "notation `foo` := bar" in boo   -- good
...

Yaël Dillies (Nov 17 2022 at 19:07):

Wait, what do you mean? that now everything must be localized in the namespace we're in?

Floris van Doorn (Nov 17 2022 at 19:31):

I expect that both work, but the ported command is simpler if you're already in the namespace.

Yaël Dillies (Nov 17 2022 at 19:32):

Does that mean

localized ... in pointwise

should become

namespace pointwise
localized ... in pointwise
end pointwise

Gabriel Ebner (Nov 17 2022 at 19:36):

must be localized in the namespace we're in?

No, it's completely optional and both variants will translate just fine. Don't add extra namespaces!

Gabriel Ebner (Nov 17 2022 at 19:37):

It's just that if you already have a namespace block, consider moving the localized commands there.

Gabriel Ebner (Nov 17 2022 at 19:37):

Think of it like def boo.foo := 42 vs namespace boo def foo := 42 end.


Last updated: Dec 20 2023 at 11:08 UTC