Internationalization

Stream: lean4

[Patrick Massot]

Has anyone started to think about internationalization of Lean programs? The minimal version would be defining a new kind of interpolated string, a meta-program creating po files and a way to set language used in the current file. The motivation is that I'm trying to port Lean verbose tactics but I would like error messages and suggestions to be translated. In Lean 3 I had two completely different Lean project for French and English but that led to the English version being a lot less usable than the original one.

[Patrick Massot]

It would be great if someone who cares about Lean as a general purpose programming language could be tempted to work on that.

[Mario Carneiro]

I would be interested to know what kind of localization tools are used these days. I have been looking into https://projectfluent.org/, this is what firefox and rustc use, I know less about gettext

[Mario Carneiro]

Internationalizing lean 4 error messages sounds like a pretty big task

[Mario Carneiro]

A framework for writing internationalized programs sounds easier but I don't think it would be that helpful for something like lean-verbose since that's all about tactics and elaboration

[Mario Carneiro]

Internationalizing the input syntax of lean 4 is comparatively easy, I think you had a prototype of that in lean 4 at ICERM

[Mario Carneiro]

Presumably the current work on #lang would make it even easier since then you could change the keywords altogether instead of being merely additive

[Kyle Miller]

#lang français

[Patrick Massot]

I really mean I have a bunch of tactic which use throwError and I want to translate those error messages, not all messages coming from Lean (which would be great but is a much bigger task).

[Patrick Massot]

And I know only gettext but I have nothing against fancier modern solution especially if they are implemented by someone else.

[Mario Carneiro]

If you are okay with conditional compilation you could just have a bunch of string constants and just swap out the file defining them

[Patrick Massot]

Sure, I could use such a very low-tech version, but that's pretty painful compared to using gettext.

[Mario Carneiro]

is it?

[Mario Carneiro]

What's the interface you are after anyway?

[Mario Carneiro]

It doesn't have to be string constants either, it can be arbitrary lean functions

[Patrick Massot]

Yes it is. gettext will automatically collect all strings that needs translations. When you look at the code you see almost nothing special. You see _("This is an error message") instead of "This is an error message". You can write as many such translatable strings as you want without breaking the programming flow.

[Mario Carneiro]

What if you want to interpolate into the string?

[Patrick Massot]

Same.

[Patrick Massot]

Interpolated strings are of course a crucial part of the story.

[Patrick Massot]

You write _("This is an error message about {stuff}") instead of "This is an error message about {stuff}"

[Mario Carneiro]

Okay, so something like:

...
  throwError tr% "This is an error message about {e}"

translations/fr.json:

{"This is an error message about {e}": "Ceci est un message d'erreur pour {e}"}

[Patrick Massot]

Yes. And fr.json is automatically generated.

[Mario Carneiro]

How?

[Mario Carneiro]

What's the input?

[Mario Carneiro]

That's what I'm asking

[Patrick Massot]

Some meta-program crawls your source file and looks for tr%.

[Patrick Massot]

The input is your lean files.

[Mario Carneiro]

Where are the translations coming from?

[Mario Carneiro]

I can see how you can validate this file but not how or where you want to put the translations

[Patrick Massot]

The meta-program generates a json file where all translations are missing originally.

[Patrick Massot]

Then human beings put in translation. And next time the meta-program is ran (because the software was updated) it doesn't touch things that were already translated of course.

[Patrick Massot]

Note that gettext does not use json for this (probably because it long predates json) but its own format po.

[Kyle Miller]

I wonder if this behavior could be implemented using an environment extension, where when a tr!"..." string is elaborated it adds this string to the extension (maybe it tags it with the identifier of the current definition too, just in case that is useful), and then the metaprogram that generates the po-analogue just imports the main Lean file and looks at the contents of the environment extension?

[Patrick Massot]

Yes, I was thinking about using environment extensions.

[Mario Carneiro]

how are the strings keyed? Just by the english interpolation like I showed?

[Patrick Massot]

Yes.

[Mario Carneiro]

are they ordered in any particular way?

[Kyle Miller]

One question is how translation substitutions work. If it's a compile-time transformation, then that's clearer, but if you want it runtime, I suppose you can validate that the substitutions refer to the exact same expressions between the {...}s, up to some permutation.

[Patrick Massot]

I don't think there is any particular order. Again the wikipedia page shows examples.

[Mario Carneiro]

I was thinking to do it as a compile time transformation

[Patrick Massot]

I don't say that we have to use the exact same format, bit those files have tooling such as https://poedit.net/

[Mario Carneiro]

you would just look up the interpolation at elaboration time and return the results of interpolating into the translated string

[Mario Carneiro]

One reason not to use po is that you would not be able to use lean style interpolated strings with them

[Mario Carneiro]

I suppose you could translate the format?

[Kyle Miller]

Maybe you could use %1, %2, etc. in place of the {...}s sequentially

[Kyle Miller]

And then at the site of the tr! string you use that to permute the interpolated expressions

[Mario Carneiro]

I wonder whether we need a typeclass to unify s! ,f!, m! because otherwise this causes issues here

[Joachim Breitner]

For general programming, I'd expect that language can be changed at runtime. For that it seems that tr! probably ought to be monadic in a suitable monad for getting the current language, and the translations database.

[Mario Carneiro]

That could be a separate mode/macro, I would expect it to be more annoying to use that way

[Joachim Breitner]

Yup, but hard to avoid in a pure language, I fear.

[Patrick Massot]

Many software require to restart to apply language preferences. My use case is a bit special, I want to translate messages coming from tactics.

[Patrick Massot]

Ideally I want to have simply import MyTactics.French and get messages in French.

[Joachim Breitner]

Restarting is fine, but (for general programming) not recompilation, I’d say. But if that's not the use-case needed right now, don’t let me distract you at this point :-)

[Patrick Massot]

In the long run it would be really nice to have a robust internationalization framework that would accommodate many use cases. But indeed in the short run I'd happy to have something that is good enough for my use case.

[Patrick Massot]

And my use case is very important for teaching outside the US, so hopefully this is something the FRO also finds interesting.

[Mario Carneiro]

I'm not sure this is something the FRO itself needs to do, this can be an external project well enough

[Patrick Massot]

Anyone should feel free to try, I was only trying to encourage Joachim.

[Joachim Breitner]

Ah, I didn’t even notice :-D

[Bulhwi Cha]

Patrick Massot said:

I don't say that we have to use the exact same format, bit those files have tooling such as https://poedit.net/

Minju Kim, @Shim SeongWoo (Shim is the surname) and I used OmegaT to translate NNG3 into Korean early last year. It's a translation memory application and free software.

[Kyle Miller]

@Patrick Massot I got a prototype of this together. It's only for String at the moment. It provides tr!"" strings that are monad-valued, and they read the current value of the lang option. When compiling, the system checks to see if there are translations for every declared language, and if there are not it suggests a new @[translation] definition to add to the environment. This system expects all translations of all keys to exist ahead of their use.

Here's an example of usage:

import Mathlib.I18n.Basic

decl_lang fr "français"

@[translation fr "Expecting an identifier, not {1}"]
def tr1 (x : String) : String :=
  s!"attendu : un identifiant, pas {x}"

elab "foo" x:num : tactic => do
  throwError ← tr!"Expecting an identifier, not {x.getNat}"

example : true := by
  foo 1 -- Expecting an identifier, not 1

set_option lang "fr"

example : true := by
  foo 1 -- attendu : un identifiant, pas 1

elab "foo2" : tactic => do
  throwError ← tr!"unknown error"
/-
Warning: Missing translation for fr (français) with key "unknown error".

Template:

@[translation fr "unknown error"]
def tr : String :=
  s!"unknown error"
-/

elab "foo3" : tactic => do
  throwError ← tr!"The following are not equal: {1} and {2}"
/-
Missing translation for fr (français) with key "The following are not equal:{1} and {2}".

Template:

@[translation fr "The following are not equal:{1} and {2}"]
def tr (s_1 : String) (s_2 : String) : String :=
  s! "The following are not equal: {s_1 } and {s_2}"
-/

[Kyle Miller]

Mathlib.I18n.Init

import Lean

open Lean

namespace I18n

/-- A language known to the translation system. -/
structure Language where
  lang : Name
  description : String

abbrev LanguageState := NameMap Language

abbrev LanguageExtension := SimplePersistentEnvExtension Language LanguageState

def LanguageState.addEntry (s : NameMap Language) (l : Language) : NameMap Language :=
  s.insert l.lang l

initialize languageExtension : LanguageExtension ←
  registerSimplePersistentEnvExtension {
    addImportedFn := mkStateFromImportedEntries LanguageState.addEntry {}
    addEntryFn    := LanguageState.addEntry
  }


def getLanguages (env : Environment) : NameMap Language := languageExtension.getState env

def isLanguage (env : Environment) (lang : Name) : Bool := getLanguages env |>.contains lang

def addLanguage (env : Environment) (l : Language) : Except String Environment := do
  if let some l' := (getLanguages env).find? l.lang then
    if l'.description != l.description then
      throw s!"Language description does not match pre-existing description: {l'.description}"
    return env
  else
    return languageExtension.addEntry env l

/-- Declare a new language for translation. -/
elab "decl_lang " n:ident s:str : command => do
  let n := n.getId.eraseMacroScopes
  let l : Language := {lang := n, description := s.getString}
  let env ← ofExcept <| addLanguage (← getEnv) l
  setEnv env

structure Translation where
  lang : Name
  key : String
  expander : Name

/-- For each key, a map of languages to expanders -/
abbrev TranslationState := HashMap String (NameMap Name)

abbrev TranslationExtension := SimplePersistentEnvExtension Translation TranslationState

def TranslationState.addEntry (s : TranslationState) (tr : Translation) : TranslationState :=
  let forKey := s.findD tr.key {}
  s.insert tr.key (forKey.insert tr.lang tr.expander)

initialize translationExtension : TranslationExtension ←
  registerSimplePersistentEnvExtension {
    addImportedFn := mkStateFromImportedEntries TranslationState.addEntry {}
    addEntryFn    := TranslationState.addEntry
  }

/-- For a given key, returns the translations as a map from languages to expansion functions. -/
def TranslationExtension.getTranslations (env : Environment) (key : String) :
    NameMap Name :=
  (translationExtension.getState env).findD key {}

def addTranslation (env : Environment) (tr : Translation) : Except String Environment := do
  unless isLanguage env tr.lang do
    throw s!"Undefined language {tr.lang}"
  return translationExtension.addEntry env tr

syntax (name := translationAttr) "translation " ident ppSpace str : attr

initialize
  registerBuiltinAttribute {
    name := `translationAttr
    descr := "add a translation"
    add   := fun decl stx kind => do
      unless kind == AttributeKind.global do
        throwError "invalid `[translation]` attribute, must be global"
      match stx with
      | `(attr| translation $lang' $key) => withRef stx[0] do
        let lang := lang'.getId.eraseMacroScopes
        let key := key.getString
        let tr : Translation := {lang, key, expander := decl}
        setEnv <| ← withRef lang' <| ofExcept <| addTranslation (← getEnv) tr
      | _  => throwError "invalid `[translation]` attribute"
  }

register_option lang : String := {
  defValue := ""
  descr := "Language to use when translating strings" }

Mathlib.I18n.Basic

import Mathlib.I18n.Init

open Lean

namespace I18n

/-- Like `s!"..."` strings but use the current `lang` option for localization. -/
syntax "tr!" interpolatedStr(term) : term

def expandInterpolatedStrChunks
    (chunks : Array Syntax) (mkAppend : Term → Term → MacroM Term) (mkElem : Term → MacroM Term) :
    MacroM (String × Array (Ident × Term) × Term) := withFreshMacroScope do
  let mut i := 0
  let mut result : Term := ⟨Syntax.missing⟩
  let mut elems : Array (Ident × Term) := #[]
  let mut key := ""
  for elem in chunks do
    let elem ← match elem.isInterpolatedStrLit? with
      | none     =>
        let j := elems.size + 1
        let n := mkIdentFrom elem (← MonadQuotation.addMacroScope (Name.appendIndexAfter `n j))
        key := key ++ "{" ++ toString j ++ "}"
        elems := elems.push (n, ← mkElem ⟨elem⟩)
        pure n.raw
      | some str =>
        key := key ++ str
        mkElem (Syntax.mkStrLit str)
    if i == 0 then
      result := ⟨elem⟩
    else
      result ← mkAppend result ⟨elem⟩
    i := i+1
  return (key, elems, result)

def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (toTypeFn : Term) :
    MacroM (String × Array (Ident × Term) × Term) := do
  let (key, elems, result) ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
  return (key, elems, ← `(($result : $type)))

open Parser Term
def mkSugg (interpStr : TSyntax interpolatedStrKind) (lang : Name) (key : String) :
    Elab.TermElabM Command := do
  let mut i := 0
  let mut args : TSyntaxArray ``Parser.Term.bracketedBinder := #[]
  let mut chunks : Array Syntax := #[]
  for elem in interpStr.raw.getArgs do
    match elem.isInterpolatedStrLit? with
    | none =>
      i := i + 1
      let arg := Name.appendIndexAfter `s i
      args := args.push <| ← `(bracketedBinderF| ($(mkIdent arg):ident : $(mkIdent `String)))
      chunks := chunks.push (mkIdent arg)
    | some _ => chunks := chunks.push elem
  let s2 : TSyntax interpolatedStrKind := ⟨interpStr.raw.modifyArgs fun _ => chunks⟩
  `(command|
    @[translation $(mkIdent lang) $(quote key)]
    def $(mkIdent `tr) $args* : $(mkIdent `String) :=
      s!$s2
    )


open Elab in
elab_rules : term
  | `(tr! $interpStr) => withFreshMacroScope do
    let (key, elems, result) ← liftMacroM <| expandInterpolatedStr interpStr (← `(String)) (← `(toString))
    let args : TSyntaxArray `term := elems.map (fun (n, _) => n)
    let translations := TranslationExtension.getTranslations (← getEnv) key
    let langs := getLanguages (← getEnv)
    let mut body := result
    for (lang, l) in langs do
      match translations.find? lang with
      | some tr =>
        body ← `(if lang == $(quote lang) then $(mkIdent tr) $args* else $body)
      | none =>
        let sugg ← mkSugg interpStr lang key
        logWarning m!"Missing translation for {lang} ({l.description}) with key {toExpr key}.{
          ""}\n\nTemplate:\n\n{sugg}"
    body ← `(term| do pure (let lang := KVMap.getString (← getOptions) `lang; $body)
      )
    let lets ← elems.foldrM (fun (id, val) b => `(let $id := $val; $b)) body
    --logInfo m!"generated: {lets}"
    Term.elabTerm lets none

[Kyle Miller]

These are basically for s!"" string translation, and I was imagining that it could be additionally keyed by whether it's for an s!, f!, or m! translation. You'd need some other prefixes for these options; maybe ts!, tf!, and tm!, or a tr% prefix that's aware of these three types of strings.

[Patrick Massot]

Thanks! That's already great. Of course translating before using isn't the most convenient thing to do, but this is definitely usable.

[Kyle Miller]

The workflow I'm imagining is this:

• You want to translate a new language, so you add a decl_lang
• You compile your project
• The collection of warnings is new translation tasks
• You create a module with all these translations and import it
• You rebuild

[Kyle Miller]

Either some tool could look at the output and collect the warnings, or the elaborator could write them to a file (say if there's some option set that you pass in on the command line)

[Patrick Massot]

Having some mechanism to write templates to a file would definitely be a huge boost of usability.

[Kyle Miller]

Right now it's not convenient for people who want to translate without recompiling, and you also can't use these translations from within the MacroM monad (it doesn't have getOptions)

[Kyle Miller]

For m! strings, I believe there's not that sort of limitation, since you can use docs#Lean.MessageData.ofPPFormat to have it lazily translate once it finally gets displayed, rather translated when it's generated.