Update lean4 toolchain to v4.28.0

.github/workflows/build.yaml

@@ -49,15 +49,15 @@ jobs:
           if-no-files-found: error
 
   build-linux:
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     steps:
       - uses: extractions/setup-just@v2
 
       - name: Setup Rust
         run: rustup toolchain install stable --profile minimal
 
       - name: Install raylib deps
-        run: sudo apt-get install -y --no-install-recommends libuv1-dev libglfw3 libglfw3-dev libx11-dev libxcursor-dev libxrandr-dev libxinerama-dev libxi-dev libxext-dev libxfixes-dev libwayland-dev libxkbcommon-dev
+        run: sudo apt-get install -y --no-install-recommends libuv1-dev libglfw3 libglfw3-dev libx11-dev libxcursor-dev libxrandr-dev libxinerama-dev libxi-dev libxext-dev libxfixes-dev libwayland-dev libxkbcommon-dev libc++-dev libc++abi-dev
 
       - name: install elan
         run: |

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c0121c73d85ae3539add5b69b3345123ac4606e1",
+   "rev": "0c90e83fd65f3b845dc46c1454309e0dbda25a71",
    "name": "«lens-demo»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c0121c73d85ae3539add5b69b3345123ac4606e1",
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0",
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "raylean",

lakefile.lean

@@ -5,9 +5,9 @@ def optionUseBundle : Bool := get_config? bundle == some "on"
 
 def optionDisableResvg : Bool := get_config? resvg == some "disable"
 
-require batteries from git "https://github.com/leanprover-community/batteries.git" @ "v4.20.0"
+require batteries from git "https://github.com/leanprover-community/batteries.git" @ "v4.28.0"
 
-require «lens-demo» from git "https://github.com/funexists/lens-demo.git" @ "c0121c73d85ae3539add5b69b3345123ac4606e1"
+require «lens-demo» from git "https://github.com/funexists/lens-demo.git" @ "v4.28.0"
 
 package «raylean» where
   srcDir := "lean"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.1
+leanprover/lean4:v4.28.0

lean/Examples/Selector.lean

@@ -18,7 +18,7 @@ inductive Demo where
 def Demo.all := allElements Demo
 
 def stringToDemo (s : String) : Option Demo :=
-  match s.trim.toLower with
+  match s.trimAscii.toString.toLower with
   | "window" => some .window
   | "platformer2d" => some .platformer2d
   | "cube3d" => some .cube3d