bump to v4.8.0

I18n/Language.lean

@@ -36,13 +36,13 @@ def ofString (s : String) : Language :=
   match s.split (· = '_') with
   | [langVariant] =>
     match langVariant.split (· = '@') with
-    | [lang]          => ⟨lang, none, none⟩
-    | [lang, variant] => ⟨lang, none, variant⟩
+    | [lang]          => ⟨.mkSimple lang, none, none⟩
+    | [lang, variant] => ⟨.mkSimple lang, none, some <| .mkSimple variant⟩
     | _               => panic! s!"Invalid language string: {s}"
   | [lang, countryVariant] =>
     match countryVariant.split (· = '@') with
-    | [country]          => ⟨lang, country, none⟩
-    | [country, variant] => ⟨lang, country, variant⟩
+    | [country]          => ⟨.mkSimple lang, some <| .mkSimple country, none⟩
+    | [country, variant] => ⟨.mkSimple lang, some <| .mkSimple country, some <| .mkSimple variant⟩
     | _                  => panic! s!"Invalid language string: {s}"
   | _ =>
     panic! s!"Invalid language string: {s}"

lake-manifest.json

@@ -4,19 +4,19 @@
  [{"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/std4",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
-   "name": "std",
+   "rev": "51e6e0d24db9341fb031288c298b7e6b56102253",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "v4.8.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "i18n",

lakefile.lean

@@ -7,7 +7,7 @@ package i18n where
 def leanVersion : String := s!"v{Lean.versionString}"
 
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
-require std from git "https://github.com/leanprover/std4" @ leanVersion
+require batteries from git "https://github.com/leanprover-community/batteries" @ leanVersion
 
 -- require datetime from git "https://github.com/T-Brick/DateTime.git" @ "main"
 -- require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
@@ -31,7 +31,7 @@ target time.o pkg : FilePath := do
   let oFile := pkg.buildDir / "c" / "time.o"
   let srcJob ← inputFile <| pkg.dir / "time" / "c" / "time.cpp"
   let weakArgs := #["-I", (← getLeanIncludeDir).toString]
-  buildO "time.cpp" oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
+  buildO oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
 
 extern_lib libLeanTime pkg := do
   let name := nameToStaticLib "leanTime"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0