From 5f06a60fc40cb76d289053a37e2c73008a272850 Mon Sep 17 00:00:00 2001 From: Sean McLaughlin Date: Thu, 6 Nov 2025 08:56:39 -0800 Subject: [PATCH 1/2] chore: Fix the FromSexp deriving generator It was possible that user-selected field names can shadow builtins in the generated program. In this case, a field named `id` was shadowing the identity function. --- KLR/Util/Sexp.lean | 11 ++++++----- KLR/Util/SexpTest.lean | 16 ++++++++++++++++ 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/KLR/Util/Sexp.lean b/KLR/Util/Sexp.lean index 759ef3c7..44826ea1 100644 --- a/KLR/Util/Sexp.lean +++ b/KLR/Util/Sexp.lean @@ -442,7 +442,8 @@ private def mkFromSexpBodyForStruct (indName : Name) : TermElabM Term := do let getter ← `(doElem| Except.mapError (fun s => (toString $(quote indName)) ++ "." ++ (toString $(quote field)) ++ ": " ++ s) <| $getter) return getter ) - let fields := fields.map mkIdent + let fieldNames := fields.map mkIdent + let fieldValues <- fields.mapM fun f => return mkIdent (<- Lean.Core.mkFreshUserName f) -- mkIdent f.capitalize let name <- Meta.nameToStrLit indName `(do let n <- sexp.length? @@ -453,11 +454,11 @@ private def mkFromSexpBodyForStruct (indName : Name) : TermElabM Term := do | some k => throw s!"No field named {k} in {$name}" | none => pure () try - $[let $fields:ident ← $getNamed]* - return { $[$fields:ident := $(id fields)],* } + $[let $fieldValues:ident ← $getNamed]* + return { $[$fieldNames:ident := $(fieldValues)],* } catch _ => - $[let $fields:ident ← $getPositional]* - return { $[$fields:ident := $(id fields)],* } + $[let $fieldValues:ident ← $getPositional]* + return { $[$fieldNames:ident := $(fieldValues)],* } ) /- diff --git a/KLR/Util/SexpTest.lean b/KLR/Util/SexpTest.lean index e423ed7c..f7d99207 100644 --- a/KLR/Util/SexpTest.lean +++ b/KLR/Util/SexpTest.lean @@ -179,3 +179,19 @@ private structure Default6 where deriving BEq, FromSexp, Repr #guard @fromSexp? Default6 _ (sexp%()) == .ok (Default6.mk) + +structure pseudo_core_barrier where + id : UInt32 + semaphore : UInt32 +deriving FromSexp + +-- Was broken in earlier version. It generated +-- assocWithDefault✝ _ sexp✝ "arg" (id { }) +-- but id was not the identity function, but the projection +private structure IdArg where +deriving FromSexp + +private structure Id where + id : Nat + arg : IdArg := {} +deriving FromSexp From b368e62507b6110b8ffced60d6366f0434ef7138 Mon Sep 17 00:00:00 2001 From: Sean McLaughlin Date: Mon, 29 Sep 2025 12:52:17 -0700 Subject: [PATCH 2/2] chore: Update Lean to 4.23 --- .github/workflows/ci.yml | 134 ---------------------------- KLR.lean | 2 +- KLR/Extract/lake-manifest.json | 38 ++++---- KLR/NRT/Main.lean | 14 +-- KLR/NRT/lake-manifest.json | 4 +- KLR/NRT/lakefile.lean | 2 +- KLR/Serde/Basic.lean | 2 +- KLR/Trace/FromNKI.lean | 2 +- KLR/Trace/ISA.lean | 4 +- KLR/Trace/Term.lean | 3 +- KLR/Util/Archive/Main.lean | 2 +- KLR/Util/Archive/lake-manifest.json | 4 +- KLR/Util/Archive/lakefile.lean | 2 +- KLR/Util/Bstruct.lean | 9 +- KLR/Util/Enum.lean | 1 - KLR/Util/Gzip/lake-manifest.json | 56 +++++------- KLR/Util/Gzip/lakefile.lean | 2 +- KLR/Util/Json.lean | 8 +- KLR/lake-manifest.json | 50 +++-------- KLR/lakefile.lean | 9 +- interop/klr/lean_ast.h | 16 ++-- lake-manifest.json | 50 +++++------ lakefile.lean | 10 ++- lean-toolchain | 2 +- 24 files changed, 129 insertions(+), 297 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9d0153cb..05f2c116 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/KLR.lean b/KLR.lean index 699a3885..a3c0cfd0 100644 --- a/KLR.lean +++ b/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 diff --git a/KLR/Extract/lake-manifest.json b/KLR/Extract/lake-manifest.json index f5fc6bf7..fe388215 100644 --- a/KLR/Extract/lake-manifest.json +++ b/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", diff --git a/KLR/NRT/Main.lean b/KLR/NRT/Main.lean index c9516dfc..654d3c7b 100644 --- a/KLR/NRT/Main.lean +++ b/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 diff --git a/KLR/NRT/lake-manifest.json b/KLR/NRT/lake-manifest.json index 9ef819ad..9a0a366d 100644 --- a/KLR/NRT/lake-manifest.json +++ b/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", diff --git a/KLR/NRT/lakefile.lean b/KLR/NRT/lakefile.lean index 253235d9..051b3fda 100644 --- a/KLR/NRT/lakefile.lean +++ b/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" diff --git a/KLR/Serde/Basic.lean b/KLR/Serde/Basic.lean index 14f88a7c..ab99d0d6 100644 --- a/KLR/Serde/Basic.lean +++ b/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 diff --git a/KLR/Trace/FromNKI.lean b/KLR/Trace/FromNKI.lean index ae20f04b..110018c0 100644 --- a/KLR/Trace/FromNKI.lean +++ b/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}'" diff --git a/KLR/Trace/ISA.lean b/KLR/Trace/ISA.lean index af54416a..d22ab63f 100644 --- a/KLR/Trace/ISA.lean +++ b/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 diff --git a/KLR/Trace/Term.lean b/KLR/Trace/Term.lean index e1df1e1e..0a679ea1 100644 --- a/KLR/Trace/Term.lean +++ b/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}" diff --git a/KLR/Util/Archive/Main.lean b/KLR/Util/Archive/Main.lean index 12611b0f..eed50365 100644 --- a/KLR/Util/Archive/Main.lean +++ b/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: diff --git a/KLR/Util/Archive/lake-manifest.json b/KLR/Util/Archive/lake-manifest.json index eff160cc..628d08a9 100644 --- a/KLR/Util/Archive/lake-manifest.json +++ b/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", diff --git a/KLR/Util/Archive/lakefile.lean b/KLR/Util/Archive/lakefile.lean index 111f365f..c9e8ff1e 100644 --- a/KLR/Util/Archive/lakefile.lean +++ b/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" diff --git a/KLR/Util/Bstruct.lean b/KLR/Util/Bstruct.lean index 8b1e6364..22915767 100644 --- a/KLR/Util/Bstruct.lean +++ b/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 diff --git a/KLR/Util/Enum.lean b/KLR/Util/Enum.lean index 3ae6a093..ab15c867 100644 --- a/KLR/Util/Enum.lean +++ b/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 diff --git a/KLR/Util/Gzip/lake-manifest.json b/KLR/Util/Gzip/lake-manifest.json index 01308411..609d40a5 100644 --- a/KLR/Util/Gzip/lake-manifest.json +++ b/KLR/Util/Gzip/lake-manifest.json @@ -1,17 +1,7 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/SHerLOC.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "c74ae090d4326cca9ff636184c330a67ca039ef6", - "name": "SHerLOC", - "manifestFile": "lake-manifest.json", - "inputRev": "c74ae090d4326cca9ff636184c330a67ca039ef6", - "inherited": false, - "configFile": "lakefile.lean"}, - {"type": "path", + [{"type": "path", "scope": "", "name": "Util", "manifestFile": "lake-manifest.json", @@ -29,61 +19,61 @@ "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"}, + {"url": "https://github.com/leanprover/SHerLOC.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c74ae090d4326cca9ff636184c330a67ca039ef6", + "name": "SHerLOC", + "manifestFile": "lake-manifest.json", + "inputRev": "c74ae090d4326cca9ff636184c330a67ca039ef6", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/TensorLib.git", "type": "git", "subDir": null, "scope": "", - "rev": "98809504392e70fe12a00da7a00d996a8fc29e86", + "rev": "d8137a41053423de98c528d75a5fa1a01fa58567", "name": "TensorLib", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.12", + "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"}, {"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"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "", - "rev": "8ff27701d003456fd59f13a9212431239d902aef", + "rev": "247ff80701c76760523b5d7c180b27b7708faf38", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.21.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", + "inputRev": "v4.23.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "Gzip", - "lakeDir": ".lake"} \ No newline at end of file + "lakeDir": ".lake"} diff --git a/KLR/Util/Gzip/lakefile.lean b/KLR/Util/Gzip/lakefile.lean index a92b3b96..9e69093c 100644 --- a/KLR/Util/Gzip/lakefile.lean +++ b/KLR/Util/Gzip/lakefile.lean @@ -70,7 +70,7 @@ extern_lib liblean_gzip 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" require Util from "../.." diff --git a/KLR/Util/Json.lean b/KLR/Util/Json.lean index faa77668..738cdc27 100644 --- a/KLR/Util/Json.lean +++ b/KLR/Util/Json.lean @@ -50,7 +50,7 @@ instance : FromJson UInt32 where partial def removeNullValues : Json -> Json | .arr a => .arr (a.map removeNullValues) | .obj o => - let pairs := o.fold (init := []) fun ps k v => + let pairs := o.foldl (init := []) fun ps k v => if v.isNull then ps else (k, removeNullValues v) :: ps Json.mkObj pairs | j => j @@ -80,7 +80,7 @@ def jsonRoundTripEq [BEq a] [FromJson a] [ToJson a] (x : a) : Bool := instance HashMapFromJson [FromJson a] : FromJson (HashMap String a) where fromJson? j := do let node <- j.getObj? - node.foldM (fun m k v => do + node.foldlM (fun m k v => do let v <- fromJson? v return m.insert k v ) HashMap.emptyWithCapacity @@ -127,8 +127,8 @@ deriving BEq, FromJson, ToJson def swapKeys (j : Json) (old new : String) : Json := match j.getObj? with | .error _ => j - | .ok obj => match obj.find compare old with + | .ok obj => match obj.get? old with | .none => j - | .some v => (Json.obj (obj.del compare old)).setObjVal! new v + | .some v => (Json.obj (obj.erase old)).setObjVal! new v end KLR.Util.Json diff --git a/KLR/lake-manifest.json b/KLR/lake-manifest.json index 62b44081..2278bed7 100644 --- a/KLR/lake-manifest.json +++ b/KLR/lake-manifest.json @@ -15,40 +15,30 @@ "type": "git", "subDir": null, "scope": "", - "rev": "98809504392e70fe12a00da7a00d996a8fc29e86", + "rev": "d8137a41053423de98c528d75a5fa1a01fa58567", "name": "TensorLib", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.12", + "inputRev": "v0.0.16", "inherited": false, "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": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "8d2067bf518731a70a255d4a61b5c103922c772e", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.21.0", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "", - "rev": "8ff27701d003456fd59f13a9212431239d902aef", - "name": "aesop", + "rev": "d117e2c28cba42e974bc22568ac999492a34e812", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.21.0", + "inputRev": "v4.23.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli.git", @@ -61,35 +51,15 @@ "inputRev": "v4.19.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", - "inherited": true, - "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "", - "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a", + "rev": "247ff80701c76760523b5d7c180b27b7708faf38", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", + "inputRev": "v4.23.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "Util", - "lakeDir": ".lake"} \ No newline at end of file + "lakeDir": ".lake"} diff --git a/KLR/lakefile.lean b/KLR/lakefile.lean index 5a87d88d..99f1dde0 100644 --- a/KLR/lakefile.lean +++ b/KLR/lakefile.lean @@ -22,11 +22,16 @@ package Util @[default_target] lean_lib Util +-- Bug in batteries? It's not getting updated automatically, though +-- we have no references to it directly. +require batteries from git + "https://github.com/leanprover-community/batteries" @ "v4.23.0" + require plausible from git - "https://github.com/leanprover-community/plausible" @ "v4.21.0" + "https://github.com/leanprover-community/plausible" @ "v4.23.0" require TensorLib from git - "https://github.com/leanprover/TensorLib.git" @ "v0.0.12" + "https://github.com/leanprover/TensorLib.git" @ "v0.0.16" require SHerLOC from git "https://github.com/leanprover/SHerLOC.git" @ "c74ae090d4326cca9ff636184c330a67ca039ef6" diff --git a/interop/klr/lean_ast.h b/interop/klr/lean_ast.h index 88e68aaf..99c87cb3 100644 --- a/interop/klr/lean_ast.h +++ b/interop/klr/lean_ast.h @@ -44,14 +44,6 @@ lean_object* Python_Expr_starred(lean_object*,uint8_t); lean_object* Python_Expr_object(lean_object*,lean_object*); lean_object* Python_Expr_format(lean_object*,lean_object*); lean_object* Python_Expr_joined(lean_object*); -extern uint8_t Python_UnaryOp_invert; -extern uint8_t Python_UnaryOp_not; -extern uint8_t Python_UnaryOp_uadd; -extern uint8_t Python_UnaryOp_usub; -lean_object* Python_Fun_mk(lean_object*,lean_object*,lean_object*,lean_object*,lean_object*,lean_object*,lean_object*); -extern uint8_t Python_BoolOp_land; -extern uint8_t Python_BoolOp_lor; -lean_object* Python_Args_mk(lean_object*,lean_object*,lean_object*,lean_object*,lean_object*,lean_object*,lean_object*); lean_object* Python_Stmt_mk(lean_object*,lean_object*); extern uint8_t Python_CmpOp_eq; extern uint8_t Python_CmpOp_ne; @@ -63,6 +55,11 @@ extern uint8_t Python_CmpOp_is; extern uint8_t Python_CmpOp_isNot; extern uint8_t Python_CmpOp_isIn; extern uint8_t Python_CmpOp_notIn; +extern uint8_t Python_UnaryOp_invert; +extern uint8_t Python_UnaryOp_not; +extern uint8_t Python_UnaryOp_uadd; +extern uint8_t Python_UnaryOp_usub; +lean_object* Python_Fun_mk(lean_object*,lean_object*,lean_object*,lean_object*,lean_object*,lean_object*,lean_object*); extern uint8_t Python_BinOp_add; extern uint8_t Python_BinOp_sub; extern uint8_t Python_BinOp_mul; @@ -76,3 +73,6 @@ extern uint8_t Python_BinOp_or; extern uint8_t Python_BinOp_xor; extern uint8_t Python_BinOp_and; extern uint8_t Python_BinOp_floor; +extern uint8_t Python_BoolOp_land; +extern uint8_t Python_BoolOp_lor; +lean_object* Python_Args_mk(lean_object*,lean_object*,lean_object*,lean_object*,lean_object*,lean_object*,lean_object*); diff --git a/lake-manifest.json b/lake-manifest.json index be4bd90e..61dde9ac 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,17 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"type": "path", + [{"url": "https://github.com/markusdemedeiros/iris-lean.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "bad4319b7179ec473716f169a80b78dac32a37bb", + "name": "iris", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.toml"}, + {"type": "path", "scope": "", "name": "Util", "manifestFile": "lake-manifest.json", @@ -22,20 +32,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": false, "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": false, "configFile": "lakefile.toml"}, {"type": "path", @@ -56,10 +66,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"}, {"type": "path", @@ -69,15 +79,15 @@ "inherited": false, "dir": "KLR/Util/Archive", "configFile": "lakefile.lean"}, - {"url": "https://github.com/markusdemedeiros/iris-lean.git", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "", - "rev": "bad4319b7179ec473716f169a80b78dac32a37bb", - "name": "iris", + "rev": "247ff80701c76760523b5d7c180b27b7708faf38", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": true, + "inputRev": "v4.23.0", + "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", @@ -89,24 +99,14 @@ "inputRev": "stable", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "", - "rev": "8ff27701d003456fd59f13a9212431239d902aef", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.21.0", - "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", diff --git a/lakefile.lean b/lakefile.lean index ea740312..42e978e7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -43,20 +43,24 @@ lean_exe "klr" where moreLinkArgs := moreLinkArgs supportInterpreter := true +-- FIXME: Without this, aesop version 4.20 is included, and the build fails. I can't figure out why. +require aesop from git + "https://github.com/leanprover-community/aesop" @ "v4.23.0" + require Archive from "KLR/Util/Archive" 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 Gzip from "KLR/Util/Gzip" require NRT from "KLR/NRT" require plausible from git - "https://github.com/leanprover-community/plausible" @ "v4.21.0" + "https://github.com/leanprover-community/plausible" @ "v4.23.0" require TensorLib from git - "https://github.com/leanprover/TensorLib.git" @ "v0.0.15" + "https://github.com/leanprover/TensorLib.git" @ "v0.0.16" require SHerLOC from git "https://github.com/leanprover/SHerLOC.git" @ "c74ae090d4326cca9ff636184c330a67ca039ef6" diff --git a/lean-toolchain b/lean-toolchain index b9f9eea1..7f254a98 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.21.0 \ No newline at end of file +leanprover/lean4:v4.23.0