chore: Update Lean to 4.23

.github/workflows/ci.yml

@@ -57,137 +57,3 @@ jobs:
 
       - name: List library dependencies
         run: ./bin/check-libs ./.lake/build/bin/klr
-
-      # temporarily disabled until after prod release
-      #- name: Install Python
-      #  uses: actions/setup-python@v5
-      #  with:
-      #    python-version: '3.x'
-      #    cache: 'pip'
-
-      #- name: Install dependencies
-      #  working-directory: ./interop
-      #  run: |
-      #    python -m pip install --upgrade pip
-      #    pip install -r requirements.txt
-
-      # temporarily disabled until we fix klr gather
-      #- name: Run pytest
-      #  working-directory: ./interop
-      #  run: |
-      #    pytest
-
-      # temporarily disabled until after prod release
-      #- name: Make a wheel
-      #  # https://github.com/pypa/cibuildwheel
-      #  # Hit this: https://github.com/pypa/cibuildwheel/discussions/1926
-      #  env:
-      #    # https://github.com/leanprover/lean4/pull/6631/files
-      #    MACOSX_DEPLOYMENT_TARGET: 99.0
-      #    CIBW_BUILD_VERBOSITY: 1
-      #  run: |
-      #    pip install cibuildwheel build
-      #    bin/make-wheel
-      #- uses: actions/upload-artifact@v4
-      #  with:
-      #    name: cibw-wheels-${{ matrix.os }}-${{ strategy.job-index }}
-      #    path: ./.wheel/wheelhouse/*.whl
-
-      # Only upload sdist from an x64 linux machine.
-      # In a normal python package the sdist would be identical regardless of which
-      # platform/arch generated it. But we want to include klr.bin, which is
-      # platform specific and currently built outside the normal python tool ecosystem.
-      # So let's include the one platform-arch that's most useful to us right now.
-      #- name: Upload sdist (Ubuntu x64 only)
-      #  if: matrix.os == 'ubuntu-latest'
-      #  uses: actions/upload-artifact@v4
-      #  with:
-      #    name: sdist-${{ matrix.os }}-${{ strategy.job-index }}
-      #    path: ./.wheel/wheelhouse/*.tar.gz
-
-  # Mostly followed guides here:
-  # - https://github.com/pypa/gh-action-pypi-publish?tab=readme-ov-file
-  # - https://packaging.python.org/en/latest/guides/publishing-package-distribution-releases-using-github-actions-ci-cd-workflows/
-  # NB: I needed to set the trusted publisher to repo NKL, not KLR, since that was its original name. Scary detail! No idea how I'd figure that out without knowing the original name.
-  publish-to-testpypi:
-    name: Publish Python 🐍 distribution 📦 to TestPyPI
-    needs:
-    - build
-    if: startsWith(github.ref, 'refs/tags/')  # only publish to pypi on tag pushes
-    runs-on: ubuntu-latest
-
-    # The `environment` just restricts the scope of trusted publishing. You
-    # add this to the things you trust in the pypi UI.
-    environment:
-      name: testpypi
-
-    permissions:
-      id-token: write  # IMPORTANT: mandatory for trusted publishing
-
-    steps:
-    - uses: actions/checkout@v4 # for scripts
-
-    - name: Download all the dists
-      uses: actions/download-artifact@v4
-      with:
-        # name: python-package-distributions
-        # # unpacks all CIBW artifacts into dist/
-        # pattern: cibw-*
-        path: dist/
-        merge-multiple: true
-
-    - name: List the wheels
-      run: |
-        ls -1 dist/
-
-    - name: Rename OSX wheels
-      working-directory: ./dist
-      run: ../bin/rename-wheels # .. because we are starting in ./dist
-
-    - name: Publish distribution 📦 to TestPyPI
-      uses: pypa/gh-action-pypi-publish@release/v1
-      with:
-        repository-url: https://test.pypi.org/legacy/
-        verbose: true
-        skip-existing: true
-
-  # For this step to succeed, you must have bumped the klr version in interop/pyproject.toml
-  publish-to-pypi:
-    name: Publish Python 🐍 distribution 📦 to PyPI
-    needs:
-    - build
-    if: startsWith(github.ref, 'refs/tags/')  # only publish to pypi on tag pushes
-    runs-on: ubuntu-latest
-
-    # The `environment` just restricts the scope of trusted publishing. You
-    # add this to the things you trust in the pypi UI.
-    environment:
-      name: pypi
-
-    permissions:
-      id-token: write  # IMPORTANT: mandatory for trusted publishing
-
-    steps:
-    - uses: actions/checkout@v4 # for scripts
-
-    - name: Download all the dists
-      uses: actions/download-artifact@v4
-      with:
-        # name: python-package-distributions
-        # # unpacks all CIBW artifacts into dist/
-        # pattern: cibw-*
-        path: dist/
-        merge-multiple: true
-
-    - name: List the wheels
-      run: |
-        ls -1 dist/
-
-    - name: Rename OSX wheels
-      working-directory: ./dist
-      run: ../bin/rename-wheels # .. because we are starting in ./dist
-
-    - name: Publish distribution 📦 to TestPyPI
-      uses: pypa/gh-action-pypi-publish@release/v1
-      with:
-        verbose: true

KLR.lean

@@ -16,7 +16,7 @@ limitations under the License.
 
 import KLR.Compile
 import KLR.Core
-import KLR.Export
+-- import KLR.Export -- Requires being in the root dir of this package, so other packages can't import with this
 import KLR.File
 import KLR.NKI
 --import KLR.Py

KLR/Extract/lake-manifest.json

@@ -39,20 +39,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e75c008a471a29793ef323cd15ac1ae6258085df",
+   "rev": "d8137a41053423de98c528d75a5fa1a01fa58567",
    "name": "TensorLib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.15",
+   "inputRev": "v0.0.16",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
+   "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.23.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"type": "path",
@@ -73,10 +73,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.23.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"type": "path",
@@ -86,34 +86,34 @@
    "inherited": true,
    "dir": "../../KLR/Util/Archive",
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
-   "name": "Qq",
+   "scope": "",
+   "rev": "247ff80701c76760523b5d7c180b27b7708faf38",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "stable",
+   "inputRev": "v4.23.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/aesop",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
-   "name": "aesop",
+   "scope": "leanprover-community",
+   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "stable",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "scope": "",
+   "rev": "d117e2c28cba42e974bc22568ac999492a34e812",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.23.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"type": "path",

KLR/NRT/Main.lean

@@ -65,13 +65,13 @@ def runNeffCmd := `[Cli|
 
   ARGS:
     neffFile : String; "NEFF file"
-    ...inputFiles : String; "Pairs of names and input files corresponding to the tensor inputs in the NEFF." ++
-                            "For example, run-neff /tmp/foo.neff a_tensor /tmp/a.tensor b_tensor /var/b.tensor" ++
-                            "would map `a_tensor` which is expected by the NEFF to the bytes in `/tmp/a.tensor`, etc." ++
-                            "Currently only files of bytes are supported. NumPy format (.npy) files seem supported by " ++
-                            "the runtime, but we haven't got them to work yet. You can generate bytes from an ndarray by calling " ++
-                            "    with open('a_tensor', 'wb') as f:" ++
-                            "        arr.tofile(f)"
+    ...inputFiles : String; "Pairs of names and input files corresponding to the tensor inputs in the NEFF.
+                             For example, run-neff /tmp/foo.neff a_tensor /tmp/a.tensor b_tensor /var/b.tensor
+                             would map `a_tensor` which is expected by the NEFF to the bytes in `/tmp/a.tensor`, etc.
+                             Currently only files of bytes are supported. NumPy format (.npy) files seem supported by
+                             the runtime, but we haven't got them to work yet. You can generate bytes from an ndarray by calling
+                                 with open('a_tensor', 'wb') as f:
+                                     arr.tofile(f)"
 ]
 
 def runTests (_ : Parsed) : IO UInt32 := do

KLR/NRT/lake-manifest.json

@@ -12,10 +12,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.23.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "NRT",

KLR/NRT/lakefile.lean

@@ -41,6 +41,6 @@ lean_exe nrt where
   root := `Main
 
 require Cli from git
-  "https://github.com/leanprover/lean4-cli.git" @ "v4.21.0"
+  "https://github.com/leanprover/lean4-cli.git" @ "v4.23.0"
 
 require FFIUtil from "../Util/FFIUtil"

KLR/Serde/Basic.lean

@@ -677,7 +677,7 @@ TODO: lift this constraint.
 def cborTag (typeTag valTag len : Nat) : ByteArray :=
   assert! len < 0x18
   let len := 0x80 ||| len
-  .mk #[ 0xd9, typeTag.toUInt8, valTag.toUInt8, len]
+  .mk #[ 0xd9, typeTag.toUInt8, valTag.toUInt8, len.toUInt8]
 
 def parseCBORTag (arr : ByteArray) : Err (Nat × Nat × Nat × ByteArray) := do
   if h:arr.size > 4 then

KLR/Trace/FromNKI.lean

@@ -115,7 +115,7 @@ instance : FromNKI Immediate where
   fromNKI?
     | .bool true => return .int 1
     | .bool false => return .int 0
-    | .int i => return .int i
+    | .int i => return .int i.toInt32
     | .float f => return .float f.toFloat32
     | t => throw s!"expecting int or 'float', got '{Term.kindStr t}'"
 

KLR/Trace/ISA.lean

@@ -831,7 +831,7 @@ nki builtin.isa.sendrecv
       src := .abstract src,
       sendToRank := send_to_rank,
       recvFromRank := recv_from_rank,
-      pipeId := .int pipe_id,
+      pipeId := .int pipe_id.toInt32,
       useGpsimdDma := use_gpsimd_dma
     }) name
     return .none
@@ -851,7 +851,7 @@ nki builtin.isa.sendrecv_cce
       src := <- src.mapM (fun x => return .abstract x),
       sendToRank := send_to_rank,
       recvFromRanks := recv_from_ranks,
-      pipeId := .int pipe_id,
+      pipeId := .int pipe_id.toInt32,
       op := op
     }) name
     return .none

KLR/Trace/Term.lean

@@ -297,8 +297,7 @@ def listAccess (l : List Term) : List Term -> Err Term
       let e := if e < 0 then l.length + e else e
       if start < 0 || start > l.length || e < 0 || e > l.length then
         throw "slice index out of bounds"
-      let sliced := List.range ((e - start + step - 1) / step).toNat |>.map fun i =>
-        l[start.toNat + i * step.toNat]!
+      let sliced := List.range ((e - start + step - 1) / step).toNat |>.map (fun i => l[start.toNat + i * step.toNat]!)
       return .list sliced.toArray
   | e => throw s!"index must be an integer or slice, got {repr e}"
 

KLR/Util/Archive/Main.lean

@@ -83,7 +83,7 @@ def extractCmd : Cmd := `[Cli|
 ]
 
 def archiveCmd : Cmd := `[Cli|
-  archive VIA (fun _ => pure 0); ["0.0.1"]
+  archive NOOP; ["0.0.1"]
   "Work with tar archives"
 
   SUBCOMMANDS:

KLR/Util/Archive/lake-manifest.json

@@ -12,10 +12,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.23.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "Archive",

KLR/Util/Archive/lakefile.lean

@@ -70,6 +70,6 @@ extern_lib liblean_archive pkg := do
   buildStaticLib (pkg.staticLibDir / name) #[ffiO]
 
 require Cli from git
-  "https://github.com/leanprover/lean4-cli.git" @ "v4.21.0"
+  "https://github.com/leanprover/lean4-cli.git" @ "v4.23.0"
 
 require FFIUtil from "../FFIUtil"

KLR/Util/Bstruct.lean

@@ -158,7 +158,7 @@ where
     for item in items do
       match item with
       | `(item| $x:ident : $typ := $v:num) =>
-        fields := fields.push (x.getId, typ.getId, v.getNat)
+        fields := fields.push (x.getId, typ.getId, v.getNat.toUInt8)
         sfields := sfields.push (<- `(structSimpleBinder| $x:ident : $typ))
       | _ => throwError "illegal syntax"
     let cmd <-
@@ -213,9 +213,8 @@ private bstruct Foo where
   x : E := 5
   y : UInt8 := 2
   z : UInt8 := 1
-deriving Repr
 
-#guard ToBytes.toBytes (Foo.mk E.x 3 1) == ByteArray.mk #[ 5 <<< 3 ||| 3 <<< 1 ||| 1 ]
+#guard ToBytes.toBytes (Foo.mk E.x 3 1) == ByteArray.mk #[ (5:UInt8) <<< 3 ||| (3:UInt8) <<< 1 ||| 1 ]
 
 private bstruct Foo0 where
   x : UInt8 := 8
@@ -239,7 +238,7 @@ def roundTrip (n m : UInt4) : Bool :=
   let foo := Foo1.mk n m
   KLR.Util.fromBytes Foo1 (ToBytes.toBytes foo) == .ok (foo, ByteArray.empty)
 
-#guard ToBytes.toBytes (Foo1.mk 3 4) == ⟨ #[ (3 <<< 4) ||| 4 ] ⟩
+#guard ToBytes.toBytes (Foo1.mk 3 4) == ⟨ #[ ((3: UInt8) <<< 4) ||| 4 ] ⟩
 #guard
   let foo := Foo1.mk 10 4
   KLR.Util.fromBytes Foo1 (ToBytes.toBytes foo) == .ok (foo, ByteArray.empty)
@@ -260,7 +259,7 @@ info: Unable to find a counter-example
 warning: declaration uses 'sorry'
 -/
 #guard_msgs in
-  example (n m : UInt4) : ToBytes.toBytes (Foo1.mk m n) == ⟨ #[ m.toNat <<< 4 ||| n.toNat ] ⟩ := by plausible
+  example (n m : UInt4) : ToBytes.toBytes (Foo1.mk m n) == ⟨ #[ m.toNat.toUInt8 <<< 4 ||| n.toNat.toUInt8 ] ⟩ := by plausible
 
 /--
 info: Unable to find a counter-example

KLR/Util/Enum.lean

@@ -229,7 +229,6 @@ private enum Foo where
   | r := 9
   | m := 10
   | n
-deriving Repr
 
 #guard Enum.toUInt8 Foo.x == 0
 #guard Foo.toUInt8 .x == 0