implement i18next-compatible jsons

I18n/EnvExtension.lean

@@ -55,6 +55,9 @@ structure LanguageState where
   /-- The contact email for problems with the generated .POT file.
   This will be written in the POT-header. -/
   translationContactEmail := ""
+  /-- Use i18next-compatible json files. Not that they contain strictly less
+  information than PO files. -/
+  useJson := false
 
 instance : Inhabited LanguageState := ⟨{}⟩ -- all fields have default options.
 
@@ -89,6 +92,7 @@ def readLanguageConfig (lang? : Option Language := none) : IO LanguageState := d
       "  \"sourceLang\": \"en\",\n" ++
       -- s!"  \"lang\": \"{lang}\",\n" ++
       "  \"translationContactEmail\": \"\"\n" ++
+      "  \"useJson\": false\n" ++
       "}\n"
     return {}
   else
@@ -110,6 +114,11 @@ def readLanguageConfig (lang? : Option Language := none) : IO LanguageState := d
           | .ok mm => mm
           | .error _ => panic! s!"in {file}, key `translationContactEmail`: not a string!"
         | .error _ => panic! s!"{file} does not contain key `translationContactEmail`!"
+      let useJson := match res.getObjVal? "useJson" with
+        | .ok m => match m.getBool? with
+          | .ok mm => mm
+          | .error _ => panic! s!"in {file}, key `useJson`: not a boolean"
+        | .error _ => panic! s!"{file} does not contain key `useJson`!"
 
       let lang := match lang? with
       | some l => l
@@ -118,7 +127,8 @@ def readLanguageConfig (lang? : Option Language := none) : IO LanguageState := d
       return {
         lang := lang
         sourceLang := sourceLang
-        translationContactEmail := email }
+        translationContactEmail := email
+        useJson := useJson }
     | .error err =>
       panic! s!"Failed to read {file}! ({err})"
 

I18n/I18next/Write.lean

@@ -14,14 +14,6 @@ def POFile.toJson (poFile : POFile) : Json :=
 
 open Elab.Command in
 
-def POFile.saveAsJson (poFile : POFile) : CommandElabM Unit := do
-  let langConfig ← readLanguageConfig
-  let sourceLang := langConfig.sourceLang.toString
-
-  let projectName ← liftCoreM getProjectName
-  let fileName := s!"{projectName}.json"
-  let path := (← IO.currentDir) / ".i18n" / sourceLang
-  IO.FS.createDirAll path
+def POFile.saveAsJson (poFile : POFile) (path : FilePath) : CommandElabM Unit := do
   -- TODO: add overwrite-check
-  IO.FS.writeFile (path / fileName) poFile.toJson.pretty
-  logInfo s!"Json-file created at {path / fileName}"
+  IO.FS.writeFile path poFile.toJson.pretty

I18n/InterpolatedStr.lean

@@ -1,4 +1,5 @@
 import Lean
+import I18n.Utils
 
 /-!
 Functions to convert an interpolated string into a string and back.
@@ -34,7 +35,7 @@ open Parser
 /-- Parse a string as an interpolated string. (Modified from `Lean.Parser.runParserCategory`) -/
 def String.parseAsInterpolatedStr (env : Environment) (input : String) (fileName := "<input>") :
     Except String <| TSyntax `interpolatedStrKind :=
-  let input := s!"\"{input}\""
+  let input := s!"\"{escape input}\""
   let p := interpolatedStrFn <| andthenFn whitespace (categoryParserFnImpl `term)
   let ictx := mkInputContext input fileName
   let s := p.run ictx { env, options := {} } (getTokenTable env) (mkParserState input)

I18n/PO/ToString.lean

@@ -15,11 +15,6 @@ def escapeRef (s : String) : String := if
   s.contains ' ' then s!"⁨{s}⁩" else s
 -- TODO: remove these characters when parsing a file!
 
-
-def escape (s : String) : String :=
-  s.replace "\\" "\\\\"
-    |>.replace "\"" "\\\""
-
 -- TODO: escape '"' everywhere
 /-- Turn a PO-entry intro a string as it would appear in the PO-file. Such a string
 starts with a bunch of comment lines, followed by `msgid` and `msgstr` (and other options):

I18n/PO/Write.lean

@@ -8,7 +8,8 @@ import Time
 
 To create a template PO-file, one needs to call `createPOTemplate`. This can for example
 be done by adding `#create_pot` at the very end of the main file of the package.
-The template is written to a folder `.i18n/` in the package's directory as a `.pot` file.
+The template is written to a folder `.i18n/` in the package's directory as a `.pot` file
+(or optionally as `.json`).
 -/
 
 open Lean System
@@ -22,30 +23,37 @@ def POFile.save (poFile : POFile) (path : FilePath) : IO Unit :=
 open Elab.Command in
 
 /--
-Write all collected untranslated strings into a PO file
-which can be found at `.i18n/[projectName].pot`
+Write all collected untranslated strings into a template file.
 -/
-def createPOTemplate : CommandElabM Unit := do
+def createTemplate : CommandElabM Unit := do
   let projectName ← liftCoreM getProjectName
-  let fileName := s!"{projectName}.pot"
-  let path := (← IO.currentDir) / ".i18n"
+  let langConfig ← readLanguageConfig
+  let sourceLang := langConfig.sourceLang.toString
+  let langState ← getLanguageState
+  let ending := if langState.useJson then "json" else "po"
+  let fileName := s!"{projectName}.{ending}"
+  let path := (← IO.currentDir) / ".i18n" / sourceLang
   IO.FS.createDirAll path
 
   let keys := untranslatedKeysExt.getState (← getEnv)
-  let langConfig ← readLanguageConfig
-  let sourceLang := langConfig.sourceLang.toString
+
   let poFile : POFile := {
     header := {
       projectIdVersion := s!"{projectName} v{Lean.versionString}"
       reportMsgidBugsTo := langConfig.translationContactEmail
       potCreationDate := ← Time.getLocalTime -- (← DateTime.now).extended_format
       language := sourceLang }
     entries := keys }
-  poFile.save (path / fileName)
-  logInfo s!"PO-file created at {path / fileName}"
+
+  if langConfig.useJson then
+    poFile.saveAsJson (path / fileName)
+    logInfo s!"Json-file created at {path / fileName}"
+  else
+    poFile.save (path / fileName)
+    logInfo s!"PO-file created at {path / fileName}"
   -- -- save a copy as Json file for i18next support
   -- poFile.saveAsJson
 
-/-- Create a PO-template-file now! -/
-elab "#create_pot" : command => do
-  createPOTemplate
+/-- Create a i18n-template-file now! -/
+elab "#export_i18n" : command => do
+  createTemplate

I18n/Translate.lean

@@ -1,6 +1,7 @@
 import Lean
 import I18n.EnvExtension
 import I18n.PO.Read
+import I18n.I18next.Read
 import I18n.InterpolatedStr
 
 open Lean Elab Term System
@@ -21,11 +22,18 @@ def loadTranslations : CoreM Unit := do
   let langState ← getLanguageState
   let projectDir ← IO.currentDir
   let projectName ← getProjectName
-  let file := projectDir / ".i18n" / s!"{projectName.toString}-{langState.lang}.po"
+
+  let ending := if langState.useJson then "json" else "po"
+  let file := projectDir / ".i18n" / s!"{langState.lang}" / s!"{projectName.toString}.{ending}"
   if ¬ (← FilePath.pathExists file) then
     logWarning s!"Translation file not found: {file}"
     return ()
-  let f ← POFile.read file
+
+  let f ← if langState.useJson then
+    POFile.readFromJson file
+  else
+    POFile.read file
+
   for e in f.entries do
     modifyEnv (translationExt.addEntry · (e.msgId, e.msgStr))
 

I18n/Utils.lean

@@ -12,3 +12,7 @@ def getProjectName : CoreM Name := do
     return `project
   | some manifest =>
     return manifest.name
+
+def escape (s : String) : String :=
+  s.replace "\\" "\\\\"
+    |>.replace "\"" "\\\""

README.md

@@ -17,12 +17,12 @@ There are three options to mark strings for translation:
 * `String.translate`: to translate a string (meta code)
 
 Marking strings with these three options will collect untranslated strings throughout
-your project. To save them all to a PO-template file, you can call `#create_pot`, e.g. in your
+your project. To save them all to a PO-template file, you can call `#export_i18n`, e.g. in your
 project's main file.
-(Alternatively you can call `I18n.createPOTemplate` at any suitable point in your (meta-) code.)
+(Alternatively you can call `I18n.createTemplate` at any suitable point in your (meta-) code.)
 
-Both will create a file `.i18n/[yourProject].pot` which you can translate using any
-"PO Editor". The translated files should be saved as `.i18n/[yourProject]-[lang].po`
+Both will create a file `.i18n/en/[yourProject].pot` which you can translate using any
+"PO Editor". The translated files should be saved as `.i18n/[lang]/[yourProject].po`
 
 Once you have a translation present, you can use `set_language` to translate everything
 in the current document: e.g. set `set_language fr` at the top of your lean document and you should get
@@ -39,6 +39,14 @@ merging an updated `.pot` file.
 If your third-party software produces a PO-file which can't be parsed (correctly) in Lean,
 please create a bug report here with a sample PO-file!
 
+## Json Files
+
+You can also choose to use i18next-compatiple json files instead of PO-files.
+Note however, that these are much less expressive therefore it is recommended to work
+with PO-files.
+
+To use `Json` files, set `"useJson": true` inside `.i18n/config.json`.
+
 ## Contribution
 
 This is merely a prototype. Contributions are very welcome!

lakefile.lean

@@ -5,6 +5,7 @@ package i18n where
   -- add package configuration options here
 
 -- require datetime from git "https://github.com/T-Brick/DateTime.git" @ "main"
+-- require importGraph from git "https://github.com/leanprover-community/import-graph" @ "v4.6.1"
 
 @[default_target]
 lean_lib I18n where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.6.1