From 12163797e296c65e689ce98b09bd4ab807d01120 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 29 Jun 2026 23:47:31 +1000 Subject: [PATCH] chore: bump toolchain to v4.32.0-rc1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 🤖 Prepared with Claude Code --- conformance/lake-manifest.json | 43 +++++++++++++++++++++++++ conformance/lakefile.toml | 2 +- conformance/lean-toolchain | 1 + lake-manifest.json | 59 +++++++++++++++------------------- lakefile.toml | 5 --- lean-toolchain | 2 +- 6 files changed, 72 insertions(+), 40 deletions(-) create mode 100644 conformance/lake-manifest.json create mode 100644 conformance/lean-toolchain diff --git a/conformance/lake-manifest.json b/conformance/lake-manifest.json new file mode 100644 index 0000000..5e1c473 --- /dev/null +++ b/conformance/lake-manifest.json @@ -0,0 +1,43 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/kim-em/hex-test-kit.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "af49dc8131395afd44cb19297a55884882397c1b", + "name": "«hex-test-kit»", + "manifestFile": "lake-manifest.json", + "inputRev": "af49dc8131395afd44cb19297a55884882397c1b", + "inherited": false, + "configFile": "lakefile.toml"}, + {"type": "path", + "scope": "", + "name": "HexRowReduce", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "..", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/kim-em/hex-matrix.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3de422434b4565933a0315338e714f303bb6442f", + "name": "HexMatrix", + "manifestFile": "lake-manifest.json", + "inputRev": "3de422434b4565933a0315338e714f303bb6442f", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "«hex-row-reduce-conformance»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/conformance/lakefile.toml b/conformance/lakefile.toml index 0eb9875..1bd2bbf 100644 --- a/conformance/lakefile.toml +++ b/conformance/lakefile.toml @@ -8,7 +8,7 @@ path = ".." [[require]] name = "hex-test-kit" git = "https://github.com/kim-em/hex-test-kit.git" -rev = "a3355fd337e13fba815e22d55c1b21060ee4bbd1" +rev = "af49dc8131395afd44cb19297a55884882397c1b" [[lean_lib]] name = "HexRowReduceConformance" diff --git a/conformance/lean-toolchain b/conformance/lean-toolchain new file mode 100644 index 0000000..63f51ea --- /dev/null +++ b/conformance/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.0-rc1 \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index 197005d..7a0e182 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,33 +1,26 @@ -{ - "version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": [ - { - "url": "https://github.com/kim-em/hex-matrix.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "3de422434b4565933a0315338e714f303bb6442f", - "name": "HexMatrix", - "manifestFile": "lake-manifest.json", - "inputRev": "3de422434b4565933a0315338e714f303bb6442f", - "inherited": false, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/batteries.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", - "inherited": false, - "configFile": "lakefile.toml" - } - ], - "name": "\u00abhex-row-reduce\u00bb", - "lakeDir": ".lake", - "fixedToolchain": false -} +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/kim-em/hex-matrix.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3de422434b4565933a0315338e714f303bb6442f", + "name": "HexMatrix", + "manifestFile": "lake-manifest.json", + "inputRev": "3de422434b4565933a0315338e714f303bb6442f", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "«hex-row-reduce»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index 18f0976..70f6400 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,11 +1,6 @@ name = "hex-row-reduce" defaultTargets = ["HexRowReduce"] -[[require]] -name = "batteries" -git = "https://github.com/leanprover-community/batteries.git" -rev = "v4.30.0-rc2" - [[require]] name = "HexMatrix" git = "https://github.com/kim-em/hex-matrix.git" diff --git a/lean-toolchain b/lean-toolchain index 6c7e31f..2694eb7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc2 +leanprover/lean4:v4.32.0-rc1