From 3b1d095983ae2a26f07789bc38e59b6c0f94171d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 26 Jun 2026 16:00:49 +1000 Subject: [PATCH 1/2] feat: migrate hex aggregator to the module system module + public import in HexAll.lean; bump all six hex-* library pins to their module-migration revs. Co-Authored-By: Claude Opus 4.8 (1M context) --- HexAll.lean | 16 ++++++++++------ lake-manifest.json | 12 ++++++------ lakefile.toml | 12 ++++++------ 3 files changed, 22 insertions(+), 18 deletions(-) diff --git a/HexAll.lean b/HexAll.lean index 63b1554..fd9914b 100644 --- a/HexAll.lean +++ b/HexAll.lean @@ -1,9 +1,13 @@ -import HexMatrix -import HexMatrixMathlib -import HexGramSchmidt -import HexGramSchmidtMathlib -import HexLLL -import HexLLLMathlib +module + +public import HexMatrix +public import HexMatrixMathlib +public import HexGramSchmidt +public import HexGramSchmidtMathlib +public import HexLLL +public import HexLLLMathlib + +public section /-! `hex` — convenience aggregator for the released hex libraries. diff --git a/lake-manifest.json b/lake-manifest.json index 187dc8d..9f3c97e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e4554e109e1cd93547572819499c33db769300af", + "rev": "a2cded1f8addfe4cdcae691d879ff79fbed8716f", "name": "HexLLLMathlib", "manifestFile": "lake-manifest.json", "inputRev": "e4554e109e1cd93547572819499c33db769300af", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ff9729a08b65fda89f391eca5ce5b4497711f815", + "rev": "a9c3ba5732db36f9303d8a8389ffc85b327892b7", "name": "HexLLL", "manifestFile": "lake-manifest.json", "inputRev": "ff9729a08b65fda89f391eca5ce5b4497711f815", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "29404cfe535ec3dc53a6a174235e69fbf0c3c7e8", + "rev": "2e1dec9bd238bb1a43b79b4160af952002caa25c", "name": "HexGramSchmidtMathlib", "manifestFile": "lake-manifest.json", "inputRev": "29404cfe535ec3dc53a6a174235e69fbf0c3c7e8", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d9ffab41cd4b400bc05eb69eb1724484d43017e3", + "rev": "ee2a2896077eff44852e3e8a28e17d2208376e7a", "name": "HexGramSchmidt", "manifestFile": "lake-manifest.json", "inputRev": "d9ffab41cd4b400bc05eb69eb1724484d43017e3", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7e2eed8ae6d962d11e65d5763ce93439ce3fcb72", + "rev": "96e1a0907b76aa648caaa984b26e2c4ed98912f9", "name": "HexMatrixMathlib", "manifestFile": "lake-manifest.json", "inputRev": "7e2eed8ae6d962d11e65d5763ce93439ce3fcb72", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "20e4c73f958cf7996199972a45e538d06121f91f", + "rev": "9e3d029b1d95426d04b132b37ff3a1f1790f6e25", "name": "HexMatrix", "manifestFile": "lake-manifest.json", "inputRev": "20e4c73f958cf7996199972a45e538d06121f91f", diff --git a/lakefile.toml b/lakefile.toml index 7cce97c..2cb15a6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -8,32 +8,32 @@ defaultTargets = ["HexAll"] [[require]] name = "HexMatrix" git = "https://github.com/kim-em/hex-matrix.git" -rev = "20e4c73f958cf7996199972a45e538d06121f91f" +rev = "9e3d029b1d95426d04b132b37ff3a1f1790f6e25" [[require]] name = "HexMatrixMathlib" git = "https://github.com/kim-em/hex-matrix-mathlib.git" -rev = "7e2eed8ae6d962d11e65d5763ce93439ce3fcb72" +rev = "96e1a0907b76aa648caaa984b26e2c4ed98912f9" [[require]] name = "HexGramSchmidt" git = "https://github.com/kim-em/hex-gram-schmidt.git" -rev = "d9ffab41cd4b400bc05eb69eb1724484d43017e3" +rev = "ee2a2896077eff44852e3e8a28e17d2208376e7a" [[require]] name = "HexGramSchmidtMathlib" git = "https://github.com/kim-em/hex-gram-schmidt-mathlib.git" -rev = "29404cfe535ec3dc53a6a174235e69fbf0c3c7e8" +rev = "2e1dec9bd238bb1a43b79b4160af952002caa25c" [[require]] name = "HexLLL" git = "https://github.com/kim-em/hex-lll.git" -rev = "ff9729a08b65fda89f391eca5ce5b4497711f815" +rev = "a9c3ba5732db36f9303d8a8389ffc85b327892b7" [[require]] name = "HexLLLMathlib" git = "https://github.com/kim-em/hex-lll-mathlib.git" -rev = "e4554e109e1cd93547572819499c33db769300af" +rev = "a2cded1f8addfe4cdcae691d879ff79fbed8716f" [[lean_lib]] name = "HexAll" From 8f3826ae5c64d235192efe93fd618c770e02023b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 26 Jun 2026 20:22:34 +1000 Subject: [PATCH 2/2] chore: re-pin all hex-* deps to canonical module-migration mains Co-Authored-By: Claude Opus 4.8 (1M context) --- lake-manifest.json | 12 ++++++------ lakefile.toml | 12 ++++++------ 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 9f3c97e..dc6443b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a2cded1f8addfe4cdcae691d879ff79fbed8716f", + "rev": "c73b5db35df9775eee9601ff629133e75085eb37", "name": "HexLLLMathlib", "manifestFile": "lake-manifest.json", "inputRev": "e4554e109e1cd93547572819499c33db769300af", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a9c3ba5732db36f9303d8a8389ffc85b327892b7", + "rev": "4c5774effb54cb1107a456287ccca3053438e756", "name": "HexLLL", "manifestFile": "lake-manifest.json", "inputRev": "ff9729a08b65fda89f391eca5ce5b4497711f815", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2e1dec9bd238bb1a43b79b4160af952002caa25c", + "rev": "ddf7de1193033da3480b1ae595c8a8adc4ec1e9b", "name": "HexGramSchmidtMathlib", "manifestFile": "lake-manifest.json", "inputRev": "29404cfe535ec3dc53a6a174235e69fbf0c3c7e8", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ee2a2896077eff44852e3e8a28e17d2208376e7a", + "rev": "9e91dd73311bc2739ca0740ba815a58453008666", "name": "HexGramSchmidt", "manifestFile": "lake-manifest.json", "inputRev": "d9ffab41cd4b400bc05eb69eb1724484d43017e3", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "96e1a0907b76aa648caaa984b26e2c4ed98912f9", + "rev": "bbdbd6f2b4b3ed8dcd95abb170d9186ceb88e3a1", "name": "HexMatrixMathlib", "manifestFile": "lake-manifest.json", "inputRev": "7e2eed8ae6d962d11e65d5763ce93439ce3fcb72", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9e3d029b1d95426d04b132b37ff3a1f1790f6e25", + "rev": "863836597fb000c6263042ce023a9375db33cb1f", "name": "HexMatrix", "manifestFile": "lake-manifest.json", "inputRev": "20e4c73f958cf7996199972a45e538d06121f91f", diff --git a/lakefile.toml b/lakefile.toml index 2cb15a6..f894007 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -8,32 +8,32 @@ defaultTargets = ["HexAll"] [[require]] name = "HexMatrix" git = "https://github.com/kim-em/hex-matrix.git" -rev = "9e3d029b1d95426d04b132b37ff3a1f1790f6e25" +rev = "863836597fb000c6263042ce023a9375db33cb1f" [[require]] name = "HexMatrixMathlib" git = "https://github.com/kim-em/hex-matrix-mathlib.git" -rev = "96e1a0907b76aa648caaa984b26e2c4ed98912f9" +rev = "bbdbd6f2b4b3ed8dcd95abb170d9186ceb88e3a1" [[require]] name = "HexGramSchmidt" git = "https://github.com/kim-em/hex-gram-schmidt.git" -rev = "ee2a2896077eff44852e3e8a28e17d2208376e7a" +rev = "9e91dd73311bc2739ca0740ba815a58453008666" [[require]] name = "HexGramSchmidtMathlib" git = "https://github.com/kim-em/hex-gram-schmidt-mathlib.git" -rev = "2e1dec9bd238bb1a43b79b4160af952002caa25c" +rev = "ddf7de1193033da3480b1ae595c8a8adc4ec1e9b" [[require]] name = "HexLLL" git = "https://github.com/kim-em/hex-lll.git" -rev = "a9c3ba5732db36f9303d8a8389ffc85b327892b7" +rev = "4c5774effb54cb1107a456287ccca3053438e756" [[require]] name = "HexLLLMathlib" git = "https://github.com/kim-em/hex-lll-mathlib.git" -rev = "a2cded1f8addfe4cdcae691d879ff79fbed8716f" +rev = "c73b5db35df9775eee9601ff629133e75085eb37" [[lean_lib]] name = "HexAll"