Open_locale

Stream: general

[Kevin Buzzard]

I'm away from a computer right now so am browsing PRs on my phone. I just saw an open_locale matrix. I've only ever opened classical. Where can I read about what other locales can be opened?

[Bryan Gin-ge Chen]

I don't think there's a list in the docs (yet), but when you get back to a computer you can put the following in a file to get a list of all imported locales:

run_cmd do
  m ← localized_attr.get_cache,
  tactic.trace m.keys -- change to `tactic.trace m.to_list`
  -- to list all the commands in each namespace

I put this in #1874, but that's currently stalled since I haven't been able to reproduce how the current mathlib docs are created.

[Yury G. Kudryashov]

You can also grep sources for the word localized

[Floris van Doorn]

You can also see which commands are executed when writing open_locale matrix by executing

run_cmd print_localized_commands [`matrix]