diff --git a/I18n.lean b/I18n.lean
index 6b50928..436ad5c 100644
--- a/I18n.lean
+++ b/I18n.lean
@@ -1,6 +1,9 @@
+import I18n.Cli
 import I18n.EnvExtension
 import I18n.InterpolatedStr
+import I18n.Json
 import I18n.Language
 import I18n.PO
+import I18n.Template
 import I18n.Translate
 import I18n.Utils
diff --git a/I18n/Cli.lean b/I18n/Cli.lean
new file mode 100644
index 0000000..4d8a25b
--- /dev/null
+++ b/I18n/Cli.lean
@@ -0,0 +1,53 @@
+import Cli.Basic
+import I18n.Std.Path
+import I18n.Template
+
+namespace I18n
+
+open Lean Cli
+
+open IO.FS IO.Process Name Core in
+/-- Implementation of `lake exe i18n` command. -/
+unsafe def i18nCLI (args : Cli.Parsed) : IO UInt32 := do
+  if args.flags.size == 0 then
+    IO.println <| IO.userError <| "i18n: expected at least one flag, see `lake exe i18n --help`!"
+
+  if  args.hasFlag "template" then
+    let module : Import := {module := (← getCurrentModule)}
+
+    searchPathRef.set compile_time_search_path%
+    try withImportModules #[module] {} (trustLevel := 1024) fun env => do
+      -- same as `createTemplate` but we're not in `CommandElabM`, but have the `env` explicitely
+      let keys := untranslatedKeysExt.getState env
+      let path ← createTemplateAux keys
+      IO.println s!"i18n: File created at {path}"
+    catch err =>
+      throw <| IO.userError <| s!"{err}\n" ++
+        "i18n: You might want to `lake build` your project first!\n"
+      throw err
+
+  if args.hasFlag "export-json" then
+    let files ← findFilesWithExtension ".i18n" "po"
+
+    for file in files do
+      let outFile := file.withExtension "json"
+      let po ← POFile.read file
+      po.saveAsJson outFile
+      IO.println s!"i18n: exported {file} to {outFile}."
+  return 0
+
+/-- Setting up command line options and help text for `lake exe graph`. -/
+unsafe def i18n : Cmd := `[Cli|
+  i18n VIA I18n.i18nCLI; ["0.1.0"]
+  "I18n CLI
+  Tool for internationalisation of Lean projects.
+  "
+
+  FLAGS:
+    t, "template";     "Create an output template `.i18n/en/Game.pot`."
+    e, "export-json"; "Exports all `.po` files in `.i18n/` to i18next-compatible `.json` format."
+]
+
+/-- `lake exe graph` -/
+unsafe def main (args : List String) : IO UInt32 :=
+  i18n.validate args
diff --git a/I18n/EnvExtension.lean b/I18n/EnvExtension.lean
index d84f93c..935721d 100644
--- a/I18n/EnvExtension.lean
+++ b/I18n/EnvExtension.lean
@@ -91,7 +91,7 @@ def readLanguageConfig (lang? : Option Language := none) : IO LanguageState := d
     IO.FS.writeFile file <| "{\n" ++
       "  \"sourceLang\": \"en\",\n" ++
       -- s!"  \"lang\": \"{lang}\",\n" ++
-      "  \"translationContactEmail\": \"\"\n" ++
+      "  \"translationContactEmail\": \"\",\n" ++
       "  \"useJson\": false\n" ++
       "}\n"
     return {}
diff --git a/I18n/Json.lean b/I18n/Json.lean
new file mode 100644
index 0000000..04d9b13
--- /dev/null
+++ b/I18n/Json.lean
@@ -0,0 +1,2 @@
+import I18n.Json.Read
+import I18n.Json.Write
diff --git a/I18n/I18next/Read.lean b/I18n/Json/Read.lean
similarity index 100%
rename from I18n/I18next/Read.lean
rename to I18n/Json/Read.lean
diff --git a/I18n/I18next/Write.lean b/I18n/Json/Write.lean
similarity index 81%
rename from I18n/I18next/Write.lean
rename to I18n/Json/Write.lean
index 12c9290..329b29a 100644
--- a/I18n/I18next/Write.lean
+++ b/I18n/Json/Write.lean
@@ -14,6 +14,6 @@ def POFile.toJson (poFile : POFile) : Json :=
 
 open Elab.Command in
 
-def POFile.saveAsJson (poFile : POFile) (path : FilePath) : CommandElabM Unit := do
+def POFile.saveAsJson (poFile : POFile) (path : FilePath) : IO Unit := do
   -- TODO: add overwrite-check
   IO.FS.writeFile path poFile.toJson.pretty
diff --git a/I18n/PO.lean b/I18n/PO.lean
index 86b7ca2..ea3b9c4 100644
--- a/I18n/PO.lean
+++ b/I18n/PO.lean
@@ -1,16 +1,3 @@
 import I18n.PO.Definition
 import I18n.PO.Read
-import I18n.PO.ToString
 import I18n.PO.Write
-
-namespace I18n
-
-open Lake
-
-open Lean.Elab.Command in
-
-
--- Bug: Introduces too many \n
-def poToJson (path : FilePath) (out : FilePath) : CommandElabM Unit := do
-  let po ← POFile.read path
-  po.saveAsJson out
diff --git a/I18n/PO/ToString.lean b/I18n/PO/ToString.lean
deleted file mode 100644
index fd54fd7..0000000
--- a/I18n/PO/ToString.lean
+++ /dev/null
@@ -1,115 +0,0 @@
-import I18n.PO.Definition
-
-/-!
-This file contains the tools to turn `POEntry` objects into strings.
-
-The other direction, i.e. parsing, happens in `I18n.PO.Read` using `Parsec`.
--/
-
-namespace I18n
-
-namespace POEntry
-
-/-- A file name containing spaces is wrapped in U+2068 and U+2069. -/
-def escapeRef (s : String) : String := if
-  s.contains ' ' then s!"⁨{s}⁩" else s
--- TODO: remove these characters when parsing a file!
-
--- 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):
-
-```
-#  some comment
-#: Project.MyFile
-msgid "untranslated sentence"
-msgstr "übersetzter Satz"
-
-Note that even the comments are sometimes parsed, depending on the second character after `#`.
-```
- -/
-def toString (e : POEntry) : String := Id.run do
-  let mut out := ""
-  if let some comment := e.comment then
-    out := out.append <| "".intercalate <| (escape comment).trim.split (· == '\n') |>.map (s!"\n#  {·}")
-  if let some extrComment := e.extrComment then
-    out := out.append <| "".intercalate <| (escape extrComment).trim.split (· == '\n') |>.map (s!"\n#. {·}")
-  -- print the refs
-  if let some ref := e.ref then
-    -- TODO: One example shows `#: src/msgcmp.c:338 src/po-lex.c:699` which is
-    -- different to what's implemented here.
-    let formattedRefs := ref.map (fun (file, line?) => match line? with
-      | none => s!"\n#: {escapeRef file}"
-      | some line => s!"\n#: {escapeRef file}:{line}" )
-    out := out.append <| "".intercalate formattedRefs
-  -- print the flags
-  if let some flags := e.flags then
-    out := out.append <| "\n#, " ++ ", ".intercalate flags
-
-  if let some prevMsgCtxt := e.prevMsgCtxt then
-    out := out.append <| s!"\n#| msgctxt \"{escape prevMsgCtxt}\""
-  if let some prevMsgId := e.prevMsgId then
-      out := out.append <|
-        "\n#| msgid \"" ++
-        ("\\n\"\n#| \"".intercalate <| (escape prevMsgId).split (· == '\n')) ++ "\""
-  if let some msgCtx := e.msgCtxt then
-    out := out.append <| s!"\nmsgctxt \"{escape msgCtx}\""
-  -- print the translation
-  let msgId := "\"" ++ ("\\n\"\n\"".intercalate <| (escape e.msgId).split (· == '\n')) ++ "\""
-  let msgStr := "\"" ++ ("\\n\"\n\"".intercalate <| (escape e.msgStr).split (· == '\n')) ++ "\""
-  out := out.append <| "\nmsgid " ++ msgId
-  out := out.append <| "\nmsgstr " ++ msgStr
-  return out.trim
-
-instance : ToString POEntry := ⟨POEntry.toString⟩
-
-/-- Paring the header entry into a `POHeaderEntry`. -/
-def toPOHeaderEntry (header : POEntry): POHeaderEntry := Id.run do
-  return {
-    -- TODO: implement!
-    projectIdVersion := ""
-    reportMsgidBugsTo := ""
-    potCreationDate := ""
-    poRevisionDate := ""
-    lastTranslator := ""
-    languageTeam := ""
-    language := ""
-    contentType := ""
-    contentTransferEncoding := ""
-    pluralForms := ""
-  }
-
-end POEntry
-
-namespace POHeaderEntry
-
-/-- The header entry is marked in the PO-file with `msgid = ""`. -/
-def toPOEntry (header : POHeaderEntry): POEntry := Id.run do
-  let mut msgStr := ""
-  msgStr := msgStr.append s!"Project-Id-Version: {header.projectIdVersion}"
-  msgStr := msgStr.append s!"\nReport-Msgid-Bugs-To: {header.reportMsgidBugsTo}"
-  msgStr := msgStr.append s!"\nPOT-Creation-Date: {header.potCreationDate}"
-  if let some revisionDate := header.poRevisionDate then
-    msgStr := msgStr.append s!"\nPO-Revision-Date: {revisionDate}"
-  msgStr := msgStr.append s!"\nLast-Translator: {header.lastTranslator}"
-  msgStr := msgStr.append s!"\nLanguage-Team: {header.languageTeam}"
-  msgStr := msgStr.append s!"\nLanguage: {header.language}"
-  msgStr := msgStr.append s!"\nContent-Type: {header.contentType}"
-  msgStr := msgStr.append s!"\nContent-Transfer-Encoding: {header.contentTransferEncoding}"
-  if let some pluralForms := header.pluralForms then
-    msgStr := msgStr.append s!"\nPlural-Forms: {pluralForms}"
-  return {msgId := "", msgStr := msgStr}
-
-end POHeaderEntry
-
-namespace POFile
-
-/-- Print a PO file as string.
-A PO file is a series of po-entries, the first one should come from the header.
--/
-def toString (f : POFile) : String :=
-  ("\n\n".intercalate (([f.header.toPOEntry] ++ f.entries.toList).map (fun e => s!"{e}"))) ++ "\n"
-
-instance : ToString POFile := ⟨POFile.toString⟩
-
-end POFile
diff --git a/I18n/PO/Write.lean b/I18n/PO/Write.lean
index e351019..2024ede 100644
--- a/I18n/PO/Write.lean
+++ b/I18n/PO/Write.lean
@@ -1,62 +1,120 @@
-import I18n.I18next.Write
-import I18n.PO.ToString
-import I18n.Translate
-import Time
--- import DateTime
-
-/-! # Create PO-file
-
-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
-(or optionally as `.json`).
+import I18n.PO.Definition
+
+/-!
+This file contains the tools to turn `POEntry` objects into strings.
+
+The other direction, i.e. parsing, happens in `I18n.PO.Read` using `Parsec`.
 -/
 
-open Lean System
 namespace I18n
 
-/-- Write a PO-file to disk. -/
-def POFile.save (poFile : POFile) (path : FilePath) : IO Unit :=
-  -- TODO: add overwrite-check
-  IO.FS.writeFile path poFile.toString
+namespace POEntry
+
+/-- A file name containing spaces is wrapped in U+2068 and U+2069. -/
+def escapeRef (s : String) : String := if
+  s.contains ' ' then s!"⁨{s}⁩" else s
+-- TODO: remove these characters when parsing a file!
+
+-- 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):
+
+```
+#  some comment
+#: Project.MyFile
+msgid "untranslated sentence"
+msgstr "übersetzter Satz"
+
+Note that even the comments are sometimes parsed, depending on the second character after `#`.
+```
+ -/
+def toString (e : POEntry) : String := Id.run do
+  let mut out := ""
+  if let some comment := e.comment then
+    out := out.append <| "".intercalate <| (escape comment).trim.split (· == '\n') |>.map (s!"\n#  {·}")
+  if let some extrComment := e.extrComment then
+    out := out.append <| "".intercalate <| (escape extrComment).trim.split (· == '\n') |>.map (s!"\n#. {·}")
+  -- print the refs
+  if let some ref := e.ref then
+    -- TODO: One example shows `#: src/msgcmp.c:338 src/po-lex.c:699` which is
+    -- different to what's implemented here.
+    let formattedRefs := ref.map (fun (file, line?) => match line? with
+      | none => s!"\n#: {escapeRef file}"
+      | some line => s!"\n#: {escapeRef file}:{line}" )
+    out := out.append <| "".intercalate formattedRefs
+  -- print the flags
+  if let some flags := e.flags then
+    out := out.append <| "\n#, " ++ ", ".intercalate flags
+
+  if let some prevMsgCtxt := e.prevMsgCtxt then
+    out := out.append <| s!"\n#| msgctxt \"{escape prevMsgCtxt}\""
+  if let some prevMsgId := e.prevMsgId then
+      out := out.append <|
+        "\n#| msgid \"" ++
+        ("\\n\"\n#| \"".intercalate <| (escape prevMsgId).split (· == '\n')) ++ "\""
+  if let some msgCtx := e.msgCtxt then
+    out := out.append <| s!"\nmsgctxt \"{escape msgCtx}\""
+  -- print the translation
+  let msgId := "\"" ++ ("\\n\"\n\"".intercalate <| (escape e.msgId).split (· == '\n')) ++ "\""
+  let msgStr := "\"" ++ ("\\n\"\n\"".intercalate <| (escape e.msgStr).split (· == '\n')) ++ "\""
+  out := out.append <| "\nmsgid " ++ msgId
+  out := out.append <| "\nmsgstr " ++ msgStr
+  return out.trim
+
+instance : ToString POEntry := ⟨POEntry.toString⟩
 
-open Elab.Command in
+/-- Paring the header entry into a `POHeaderEntry`. -/
+def toPOHeaderEntry (header : POEntry): POHeaderEntry := Id.run do
+  return {
+    -- TODO: implement!
+    projectIdVersion := ""
+    reportMsgidBugsTo := ""
+    potCreationDate := ""
+    poRevisionDate := ""
+    lastTranslator := ""
+    languageTeam := ""
+    language := ""
+    contentType := ""
+    contentTransferEncoding := ""
+    pluralForms := ""
+  }
 
-/--
-Write all collected untranslated strings into a template file.
+end POEntry
+
+namespace POHeaderEntry
+
+/-- The header entry is marked in the PO-file with `msgid = ""`. -/
+def toPOEntry (header : POHeaderEntry): POEntry := Id.run do
+  let mut msgStr := ""
+  msgStr := msgStr.append s!"Project-Id-Version: {header.projectIdVersion}"
+  msgStr := msgStr.append s!"\nReport-Msgid-Bugs-To: {header.reportMsgidBugsTo}"
+  msgStr := msgStr.append s!"\nPOT-Creation-Date: {header.potCreationDate}"
+  if let some revisionDate := header.poRevisionDate then
+    msgStr := msgStr.append s!"\nPO-Revision-Date: {revisionDate}"
+  msgStr := msgStr.append s!"\nLast-Translator: {header.lastTranslator}"
+  msgStr := msgStr.append s!"\nLanguage-Team: {header.languageTeam}"
+  msgStr := msgStr.append s!"\nLanguage: {header.language}"
+  msgStr := msgStr.append s!"\nContent-Type: {header.contentType}"
+  msgStr := msgStr.append s!"\nContent-Transfer-Encoding: {header.contentTransferEncoding}"
+  if let some pluralForms := header.pluralForms then
+    msgStr := msgStr.append s!"\nPlural-Forms: {pluralForms}"
+  return {msgId := "", msgStr := msgStr}
+
+end POHeaderEntry
+
+namespace POFile
+
+/-- Print a PO file as string.
+A PO file is a series of po-entries, the first one should come from the header.
 -/
-def createTemplate : CommandElabM Unit := do
-  let projectName ← liftCoreM getProjectName
-
-  -- read config instead of `languageState` because that state only
-  -- gets initialised if `set_language` is used in the document.
-  let langConfig ← readLanguageConfig
-
-  let sourceLang := langConfig.sourceLang.toString
-  let ending := if langConfig.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 poFile : POFile := {
-    header := {
-      projectIdVersion := s!"{projectName} v{Lean.versionString}"
-      reportMsgidBugsTo := langConfig.translationContactEmail
-      potCreationDate := ← Time.getLocalTime -- (← DateTime.now).extended_format
-      language := sourceLang }
-    entries := keys }
-
-  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 i18n-template-file now! -/
-elab "#export_i18n" : command => do
-  createTemplate
+def toString (f : POFile) : String :=
+  ("\n\n".intercalate (([f.header.toPOEntry] ++ f.entries.toList).map (fun e => s!"{e}"))) ++ "\n"
+
+instance : ToString POFile := ⟨POFile.toString⟩
+
+open Lean System
+
+/-- Write a PO-file to disk. -/
+def save (poFile : POFile) (path : FilePath) : IO Unit :=
+  -- TODO: add overwrite-check
+  IO.FS.writeFile path poFile.toString
diff --git a/I18n/Std/Path.lean b/I18n/Std/Path.lean
new file mode 100644
index 0000000..b588f2f
--- /dev/null
+++ b/I18n/Std/Path.lean
@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2022 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+
+NOTE(!): This is an unmodified copy of [Std](https://github.com/leanprover/std4), but
+requiring std as a package currently inflicts problems with version management,
+especially when `lean-i18n` is used in combination with `mathlib`.
+-/
+import Lean.Elab.Term
+
+/-!
+# `compile_time_search_path%` term elaborator.
+
+Use this as `searchPathRef.set compile_time_search_path%`.
+-/
+
+open Lean System
+
+-- Ideally this instance would be constructed simply by `deriving instance ToExpr for FilePath`
+-- but for now we have decided not to upstream the `ToExpr` derive handler from `Mathlib`.
+-- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/ToExpr.20derive.20handler/near/386476438
+instance : ToExpr FilePath where
+  toTypeExpr := mkConst ``FilePath
+  toExpr path := mkApp (mkConst ``FilePath.mk) (toExpr path.1)
+
+/--
+Term elaborator that retrieves the current `SearchPath`.
+
+Typical usage is `searchPathRef.set compile_time_search_path%`.
+
+This must not be used in files that are potentially compiled on another machine and then
+imported.
+(That is, if used in an imported file it will embed the search path from whichever machine
+compiled the `.olean`.)
+-/
+elab "compile_time_search_path%" : term =>
+  return toExpr (← searchPathRef.get)
diff --git a/I18n/Template.lean b/I18n/Template.lean
new file mode 100644
index 0000000..b3b5b08
--- /dev/null
+++ b/I18n/Template.lean
@@ -0,0 +1,66 @@
+import I18n.Json
+import I18n.PO
+
+import I18n.Translate
+import Time
+-- import DateTime
+
+/-! # Create PO-file
+
+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
+(or optionally as `.json`).
+-/
+
+open Lean System
+
+namespace I18n
+
+/--
+Write all collected untranslated strings into a template file.
+
+Note: returns the `FilePath` of the created file, simply to display a `logInfo` in `CommandElabM`.
+-/
+def createTemplateAux (keys : Array POEntry) : IO FilePath := do
+  let projectName ← getProjectName
+
+  -- read config instead of `languageState` because that state only
+  -- gets initialised if `set_language` is used in the document.
+  let langConfig ← readLanguageConfig
+
+  let sourceLang := langConfig.sourceLang.toString
+  let ending := if langConfig.useJson then "json" else "pot"
+  let fileName := s!"{projectName}.{ending}"
+  let path := (← IO.currentDir) / ".i18n" / sourceLang
+  IO.FS.createDirAll path
+
+  let poFile : POFile := {
+    header := {
+      projectIdVersion := s!"{projectName} v{Lean.versionString}"
+      reportMsgidBugsTo := langConfig.translationContactEmail
+      potCreationDate := ← Time.getLocalTime -- (← DateTime.now).extended_format
+      language := sourceLang }
+    entries := keys }
+
+  if langConfig.useJson then
+    poFile.saveAsJson (path / fileName)
+  else
+    poFile.save (path / fileName)
+
+  return (path / fileName)
+
+open Elab.Command in
+
+/--
+Write all collected untranslated strings into a template file.
+-/
+def createTemplate : CommandElabM Unit := do
+  let keys := untranslatedKeysExt.getState (← getEnv)
+  let path ← createTemplateAux keys
+  logInfo s!"File created at {path}"
+
+
+/-- Create a i18n-template-file now! -/
+elab "#export_i18n" : command => do
+  createTemplate
diff --git a/I18n/Translate.lean b/I18n/Translate.lean
index 71c9e0f..dd80b90 100644
--- a/I18n/Translate.lean
+++ b/I18n/Translate.lean
@@ -1,7 +1,7 @@
 import Lean
 import I18n.EnvExtension
 import I18n.PO.Read
-import I18n.I18next.Read
+import I18n.Json.Read
 import I18n.InterpolatedStr
 
 open Lean Elab Term System
diff --git a/I18n/Utils.lean b/I18n/Utils.lean
index 1f2d0fd..8dcbd86 100644
--- a/I18n/Utils.lean
+++ b/I18n/Utils.lean
@@ -5,14 +5,45 @@ open Lean
 namespace I18n
 
 /-- Read the name of the current package from the lake-manifest. -/
-def getProjectName : CoreM Name := do
+def getProjectName : IO Name := do
   match (← Lake.Manifest.load? ⟨"lake-manifest.json"⟩) with
   | none =>
-    logWarning "I18n: Could not read lake-manifest.json!"
+    -- TODO: What warnings can I print in `IO`?
+    -- logWarning "I18n: Could not read lake-manifest.json!"
     return `project
   | some manifest =>
     return manifest.name
 
+/-- Read the name of the main module from the `lake-manifest`. -/
+def getCurrentModule : IO Name := do
+
+  match (← Lake.Manifest.load? ⟨"lake-manifest.json"⟩) with
+  | none =>
+    -- TODO: should this be caught?
+    pure .anonymous
+  | some manifest =>
+    -- TODO: This assumes that the `package` and the default `lean_lib`
+    -- have the same name up to capitalisation.
+    -- Would be better to read the `.defaultTargets` from the
+    -- `← getRootPackage` from `Lake`, but I can't make that work with the monads involved.
+    return manifest.name.capitalize
+
+open System in
+
+/-- Return a list of all `.po` files inside the specified folder and its subfolders. -/
+partial def findFilesWithExtension (path : FilePath) (extension : String) :
+    IO <| Array FilePath := do
+  let dirContent ← path.readDir
+  let mut poFiles : Array FilePath := #[]
+  for entry in dirContent do
+    let file := entry.root / entry.fileName
+    if ← file.isDir then
+      poFiles := poFiles ++ (← findFilesWithExtension file extension)
+      pure ()
+    else if file.extension = some extension then
+      poFiles := poFiles.push file
+  return poFiles
+
 def escape (s : String) : String :=
   s.replace "\\" "\\\\"
     |>.replace "\"" "\\\""
diff --git a/README.md b/README.md
index 2046e02..c58fb54 100644
--- a/README.md
+++ b/README.md
@@ -17,35 +17,46 @@ 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 `#export_i18n`, e.g. in your
-project's main file.
-(Alternatively you can call `I18n.createTemplate` at any suitable point in your (meta-) code.)
+your project. To save them all to a template file, you have multiple options (choose one):
 
-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`
+* Call `lake exe i18n --template` inside your project (after `lake build`).
+* Place `#export_i18n` inside any Lean document. This will be executed every time that Lean
+  document is built.
+* call `I18n.createTemplate` at any suitable point in your (meta-) code.
+
+Any of these options will create a file `.i18n/en/[YourProject].pot` which you can
+translate using any a suitable editor like "Poedit" (these editors also help you merging a modified `.pot` into an existing translation).
+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
-your French translation of strings printed.
+in the current document: e.g. set `set_language fr` at the top of your lean document and you
+should get your French translation of strings printed.
 
 ## PO Files
 
-This package aims to add support for PO files as specified
+This package aims to support PO files as specified
 in the [GNU gettext manual](https://www.gnu.org/software/gettext/manual/html_node/PO-Files.html).
 
-You can use existing "PO editors" to manage the translations. For example, they help with
-merging an updated `.pot` file.
+(currently no plural forms!)
 
-If your third-party software produces a PO-file which can't be parsed (correctly) in Lean,
+If your third-party software can not import a PO-file or 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.
+Currently the recommended workflow to retrieve i18next-compatible JSON files is the following:
+
+1. use `lake exe i18n --template` to create a `.pot` file
+2. create/manage the translated `.po` files as described above.
+3. run `lake exe i18n --export`. This will export *every* `.po` file inside the `.i18n/` folder
+   into a Json located in the same folder.
+
+### Avoiding PO files
 
-To use `Json` files, set `"useJson": true` inside `.i18n/config.json`.
+However, you might want to choose to avoid PO-files and exclusively manage the less expressive
+Json files. In this case, you can set `"useJson": true` inside `.i18n/config.json`. With this
+option the template will be `.i18n/en/[YourProject].json` and it will look for translations
+at `.i18n/[lang]/[YourProject].json`
 
 ## Contribution
 
diff --git a/lake-manifest.json b/lake-manifest.json
index dec388d..f7244a2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,5 +1,14 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
  "name": "i18n",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index ff1021d..2528f86 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,6 +4,8 @@ open Lake DSL
 package i18n where
   -- add package configuration options here
 
+require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
+
 -- 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"
 
@@ -11,21 +13,11 @@ package i18n where
 lean_lib I18n where
   -- add library configuration options here
 
--- @[default_target]
--- lean_exe gettext where
---   root := `Main
---   -- Enables the use of the Lean interpreter by the executable (e.g.,
---   -- `runFrontend`) at the expense of increased binary size on Linux.
---   -- Remove this line if you do not need such functionality.
---   supportInterpreter := true
-
--- @[default_target]
--- lean_exe createPOT where
---   root := `Main
---   -- Enables the use of the Lean interpreter by the executable (e.g.,
---   -- `runFrontend`) at the expense of increased binary size on Linux.
---   -- Remove this line if you do not need such functionality.
---   supportInterpreter := false
+@[default_target]
+lean_exe i18n where
+  root := `I18n.Cli
+  -- Apparently it's needed!
+  supportInterpreter := true
 
 -- temporary replacement for `datetime` package.
 lean_lib Time where