Zulip Chat Archive

Stream: general

Topic: Open_locale


view this post on Zulip Kevin Buzzard (Jan 28 2020 at 14:17):

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?

view this post on Zulip Bryan Gin-ge Chen (Jan 28 2020 at 15:14):

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.

view this post on Zulip Yury G. Kudryashov (Jan 28 2020 at 15:56):

You can also grep sources for the word localized

view this post on Zulip Floris van Doorn (Jan 28 2020 at 17:42):

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

run_cmd print_localized_commands [`matrix]

Last updated: May 13 2021 at 06:15 UTC