chore: Update Lean to 4.23

Author: seanmcl

.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/Core/Indexing.lean

@@ -451,7 +451,7 @@ structure FreeSpans (d : Nat) where
 
 def FreeSpans.get! {d : Nat} (f : FreeSpans d) (c : Coord d) : Coord d where
   coords := List.zipWith (IndexSpan.get! · ·) f.spans c.coords
-  coords_dim := by simp [FreeSpans.spans_dim, Coord.coords_dim, Nat.min_self]
+  coords_dim := by simp [FreeSpans.spans_dim, Coord.coords_dim]
 
 /- ## Composition -/
 
@@ -470,7 +470,7 @@ def comp {d} (f : FreeSpans d) (l : Layout d) : Layout d where
   offset := Int.toNat <| offset f l
   steps := steps f l
   nums  := l.nums
-  steps_dim := by simp [FreeSpans.spans_dim, Layout.steps_dim, Nat.min_self, steps]
+  steps_dim := by simp [FreeSpans.spans_dim, Layout.steps_dim, steps]
   nums_dim := l.nums_dim
 
 end lcomp

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

@@ -106,7 +106,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

@@ -805,7 +805,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
@@ -825,7 +825,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

@@ -308,7 +308,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.get! (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}"