Making docs for `localized`- format suggestions

Stream: general

[Eric Rodriguez]

Hey all, I'm planning to make some docs for localized and open_locale so you can quickly ctrl+f what a specific locale does. Would anyone have any preference for where it goes, and the format to use for it? I was thinking an alphabetical list, something like this:

##classical

Puts the attributes `classical.prop_decidable`, `eq.decidable` and `decidable_eq_of_decidable_le`
in the local context. Defined at `localized.lean`.

[Kevin Buzzard]

Isn't there also some delicate choice of priority for those attributes?

[Eric Rodriguez]

they've got very low priority, yes; i'll make a note of that too, but right now I'm just trying to figure out what would be a decent format for everything/what would be most useful for everyone

[Eric Wieser]

It would be cool if doc-gen could automatically compile the lists of things in each locale

[Eric Wieser]

Rather than you assembling that list by hand and having it go out of date

[Eric Rodriguez]

that'd be nice, I was gonna suggest that it was made a requirement that if you add any new localization you'd then have to update the file

[Eric Rodriguez]

could you (in theory) put a docstring on localized stuff? for exmaple, documenting why the specific classical instance prios were chosen

[Eric Wieser]

Yeah, I think that's possible

[Eric Wieser]

And a good idea too, if someone can show how it's done

[Patrick Massot]

Experience suggest any such manual documentation would go out of sync.

[Patrick Massot]

Maybe we should rather improve the existing documentation, and put more emphasis on the run_cmd print_localized_commands [my.add]`. The main problem with https://leanprover-community.github.io/mathlib_docs/commands.html#localized%20notation is it suggests this is only about notation, whereas it can also put instances tag (and maybe other things?)

[Gabriel Ebner]

https://github.com/leanprover-community/doc-gen/issues/94
https://github.com/leanprover-community/doc-gen/issues/36

[Eric Wieser]

Presumably it wouldn't be impossible to get the output of docs#print_localized_commands in doc-gen's export.json?

[Gabriel Ebner]

No, it should be comparatively trivial.