From 51e0b2d4ecb7bee98ad1eb02bfaf47056ad48402 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 10:43:15 +1000 Subject: [PATCH] chore: repoint dependency pins to leanprover The released split libraries moved from kim-em to the leanprover org. Repoint this aggregate's Lake pins and manifest to leanprover (same revisions, which the transfer preserved), so the dependency URLs no longer rely on GitHub's transfer redirect. Co-Authored-By: Claude Opus 4.8 (1M context) --- lake-manifest.json | 26 +++++++++++++------------- lakefile.toml | 12 ++++++------ 2 files changed, 19 insertions(+), 19 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index b1bda66..219a7fa 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,7 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/kim-em/hex-lll-mathlib.git", + [{"url": "https://github.com/leanprover/hex-lll-mathlib.git", "type": "git", "subDir": null, "scope": "", @@ -11,7 +11,7 @@ "inputRev": "f1620294345421743f2a644b429de4ce8370a541", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-lll.git", + {"url": "https://github.com/leanprover/hex-lll.git", "type": "git", "subDir": null, "scope": "", @@ -21,7 +21,7 @@ "inputRev": "72e42ed35d0907301b2a323988944404e5628feb", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/kim-em/hex-gram-schmidt-mathlib.git", + {"url": "https://github.com/leanprover/hex-gram-schmidt-mathlib.git", "type": "git", "subDir": null, "scope": "", @@ -31,7 +31,7 @@ "inputRev": "78cf8d7def9cee8d27c27641fd20059366f9f6b1", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-gram-schmidt.git", + {"url": "https://github.com/leanprover/hex-gram-schmidt.git", "type": "git", "subDir": null, "scope": "", @@ -41,7 +41,7 @@ "inputRev": "9033c5b917e8a7280cb1cd54af0546b64349a4c0", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-matrix-mathlib.git", + {"url": "https://github.com/leanprover/hex-matrix-mathlib.git", "type": "git", "subDir": null, "scope": "", @@ -51,7 +51,7 @@ "inputRev": "ba8b22af8a25fe7fa6db3b3637fdb1dca492c38a", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-matrix.git", + {"url": "https://github.com/leanprover/hex-matrix.git", "type": "git", "subDir": null, "scope": "", @@ -71,7 +71,7 @@ "inputRev": "v4.32.0-rc1-patch1", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/kim-em/hex-bareiss.git", + {"url": "https://github.com/leanprover/hex-bareiss.git", "type": "git", "subDir": null, "scope": "", @@ -81,7 +81,7 @@ "inputRev": "733e2937905ad612423d86a2e39d345fd72ed8ac", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-determinant.git", + {"url": "https://github.com/leanprover/hex-determinant.git", "type": "git", "subDir": null, "scope": "", @@ -91,7 +91,7 @@ "inputRev": "8ce401452f1cfcf714d46887440d7d4341177818", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-row-reduce.git", + {"url": "https://github.com/leanprover/hex-row-reduce.git", "type": "git", "subDir": null, "scope": "", @@ -101,7 +101,7 @@ "inputRev": "48a6d92ac69e1fd6b3b1a86be9cb793a76e000c2", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-bareiss-mathlib.git", + {"url": "https://github.com/leanprover/hex-bareiss-mathlib.git", "type": "git", "subDir": null, "scope": "", @@ -111,7 +111,7 @@ "inputRev": "cd4ad3ecb0f9c8e5317f714edbcb1e748c0e8710", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-determinant-mathlib.git", + {"url": "https://github.com/leanprover/hex-determinant-mathlib.git", "type": "git", "subDir": null, "scope": "", @@ -121,7 +121,7 @@ "inputRev": "ae285cb33473b37a1c868f250aa4c9a3854390f2", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-row-reduce-mathlib.git", + {"url": "https://github.com/leanprover/hex-row-reduce-mathlib.git", "type": "git", "subDir": null, "scope": "", @@ -131,7 +131,7 @@ "inputRev": "4cd50b210b6e972488b790962a8f08e7f666e584", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/hex-basic.git", + {"url": "https://github.com/leanprover/hex-basic.git", "type": "git", "subDir": null, "scope": "", diff --git a/lakefile.toml b/lakefile.toml index 584909f..69739b4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,32 +7,32 @@ defaultTargets = ["HexAll"] [[require]] name = "HexMatrix" -git = "https://github.com/kim-em/hex-matrix.git" +git = "https://github.com/leanprover/hex-matrix.git" rev = "7359d9c53c3d85309b526dd1663a33b28a28bf50" [[require]] name = "HexMatrixMathlib" -git = "https://github.com/kim-em/hex-matrix-mathlib.git" +git = "https://github.com/leanprover/hex-matrix-mathlib.git" rev = "ba8b22af8a25fe7fa6db3b3637fdb1dca492c38a" [[require]] name = "HexGramSchmidt" -git = "https://github.com/kim-em/hex-gram-schmidt.git" +git = "https://github.com/leanprover/hex-gram-schmidt.git" rev = "9033c5b917e8a7280cb1cd54af0546b64349a4c0" [[require]] name = "HexGramSchmidtMathlib" -git = "https://github.com/kim-em/hex-gram-schmidt-mathlib.git" +git = "https://github.com/leanprover/hex-gram-schmidt-mathlib.git" rev = "78cf8d7def9cee8d27c27641fd20059366f9f6b1" [[require]] name = "HexLLL" -git = "https://github.com/kim-em/hex-lll.git" +git = "https://github.com/leanprover/hex-lll.git" rev = "72e42ed35d0907301b2a323988944404e5628feb" [[require]] name = "HexLLLMathlib" -git = "https://github.com/kim-em/hex-lll-mathlib.git" +git = "https://github.com/leanprover/hex-lll-mathlib.git" rev = "f1620294345421743f2a644b429de4ce8370a541" [[lean_lib]]