From 2809a459da522b8e80910612a902ce527082922f Mon Sep 17 00:00:00 2001 From: justincasher Date: Sun, 19 Apr 2026 10:51:17 -0400 Subject: [PATCH] Bump extractor workspaces for doc-gen4 SQLite support Updates lakefile.lean, lean-toolchain, and lake-manifest.json across the cslib, flt, formal-conjectures, mathlib, and physlean extractor workspaces to the latest toolchain (v4.30.0-rc2) and reorders the doc-gen4 require before the main package dependency to avoid transitive conflicts. Four workspaces pin doc-gen4 @ "main" for access to the new SQLite api-docs.db output. PhysLean remains pinned to v4.29.0 to match its Lean toolchain. PhysExtract.lean is updated to import Physlib and QuantumInfo, the post-rename library targets. Manifests regenerated via `lake update` in each workspace. --- lean/cslib/lake-manifest.json | 133 +++++++++++--------- lean/cslib/lakefile.lean | 6 +- lean/cslib/lean-toolchain | 2 +- lean/flt/lake-manifest.json | 131 ++++++++++--------- lean/flt/lakefile.lean | 6 +- lean/flt/lean-toolchain | 2 +- lean/formal-conjectures/lake-manifest.json | 139 +++++++++++---------- lean/formal-conjectures/lakefile.lean | 6 +- lean/formal-conjectures/lean-toolchain | 2 +- lean/mathlib/lake-manifest.json | 129 ++++++++++--------- lean/mathlib/lakefile.lean | 6 +- lean/mathlib/lean-toolchain | 2 +- lean/physlean/PhysExtract.lean | 3 +- lean/physlean/lake-manifest.json | 131 ++++++++++--------- lean/physlean/lakefile.lean | 7 +- lean/physlean/lean-toolchain | 2 +- 16 files changed, 382 insertions(+), 325 deletions(-) diff --git a/lean/cslib/lake-manifest.json b/lean/cslib/lake-manifest.json index 76ba7e0..6e4850f 100644 --- a/lean/cslib/lake-manifest.json +++ b/lean/cslib/lake-manifest.json @@ -1,81 +1,41 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/leanprover/cslib", "type": "git", "subDir": null, "scope": "", - "rev": "7be6082d00bb0cfc1e136505dba7718cd5fcaa84", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0-rc1", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/cslib", - "type": "git", - "subDir": null, - "scope": "", - "rev": "00d68a39497c0954bd52ca5237eea2aa152a5387", + "rev": "95fdc7dc863ff83e9d6c3a68fcb2505540462a4d", "name": "Cslib", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "28e0856d4424863a85b18f38868c5420c55f9bae", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "1c5c543d2637aebf90c80aead2d401ae88db13cc", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", - "name": "MD4Lean", + "rev": "799154a6ee3cefd3c0c89a68a81911fb83b7755c", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": true, + "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5352afccd6866369be9de43f5b7ec47203555f44", + "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0-rc1", + "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7311586e1a56af887b1081d05e80c11b6c41d212", + "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60", + "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,41 +65,92 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294", + "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.86", + "inputRev": "v0.0.98", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0", + "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "23324752757bf28124a518ec284044c8db79fee5", + "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", "name": "batteries", "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c7326b06de365308e008bdfe379909e44334a2e2", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "05954ce1797e6bd6b414c916499fe6dda4a11702", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "«cslib-extractor»", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/cslib/lakefile.lean b/lean/cslib/lakefile.lean index e48cda9..3f04e15 100644 --- a/lean/cslib/lakefile.lean +++ b/lean/cslib/lakefile.lean @@ -7,8 +7,8 @@ package «cslib-extractor» where lean_lib «CslibExtract» where roots := #[`CslibExtract] +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main" + require Cslib from git "https://github.com/leanprover/cslib" @ "main" - -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "v4.28.0-rc1" diff --git a/lean/cslib/lean-toolchain b/lean/cslib/lean-toolchain index 4bafde2..635bb95 100644 --- a/lean/cslib/lean-toolchain +++ b/lean/cslib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0-rc1 +leanprover/lean4:v4.30.0-rc2 \ No newline at end of file diff --git a/lean/flt/lake-manifest.json b/lean/flt/lake-manifest.json index 0faeab2..8695c3d 100644 --- a/lean/flt/lake-manifest.json +++ b/lean/flt/lake-manifest.json @@ -1,65 +1,25 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/ImperialCollegeLondon/FLT", "type": "git", "subDir": null, "scope": "", - "rev": "01e143329f2f79abbb8559344e836c221ae84cfd", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/ImperialCollegeLondon/FLT", - "type": "git", - "subDir": null, - "scope": "", - "rev": "782d8b962dd96be0c767b7b99e390e32c52ea583", + "rev": "e8c35753f741cf30ffc59dcec88b5ce4e36f37b7", "name": "FLT", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "b09d573cbacf5a8e767292e0edeec787a81689ce", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "c8a6a4dae7c7f42949a1058427a75c20447e990f", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", - "name": "MD4Lean", + "rev": "799154a6ee3cefd3c0c89a68a81911fb83b7755c", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": true, + "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", @@ -75,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", + "rev": "8e3c989104daaa052921bf43de9eef0e1ac9fbf5", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -85,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f", + "rev": "264309b5c0c10e569025a53ab6440a45c03133e4", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", + "rev": "4411c5f89c797401c609b3a946c8874569e69731", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,41 +75,92 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c04225ee7c0585effbd933662b3151f01b600e40", + "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.85", + "inputRev": "v0.0.97", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", + "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", + "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", + "rev": "bf597c77bf9b8e66720d724928207f5911533113", "name": "batteries", "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c7326b06de365308e008bdfe379909e44334a2e2", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "05954ce1797e6bd6b414c916499fe6dda4a11702", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "«flt-extractor»", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/flt/lakefile.lean b/lean/flt/lakefile.lean index 412308c..f21999c 100644 --- a/lean/flt/lakefile.lean +++ b/lean/flt/lakefile.lean @@ -7,8 +7,8 @@ package «flt-extractor» where lean_lib «FLTExtract» where roots := #[`FLTExtract] +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main" + require FLT from git "https://github.com/ImperialCollegeLondon/FLT" @ "main" - -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "v4.27.0" diff --git a/lean/flt/lean-toolchain b/lean/flt/lean-toolchain index 5249182..635bb95 100644 --- a/lean/flt/lean-toolchain +++ b/lean/flt/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0 +leanprover/lean4:v4.30.0-rc2 \ No newline at end of file diff --git a/lean/formal-conjectures/lake-manifest.json b/lean/formal-conjectures/lake-manifest.json index 3f35390..3f73c23 100644 --- a/lean/formal-conjectures/lake-manifest.json +++ b/lean/formal-conjectures/lake-manifest.json @@ -1,91 +1,51 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/google-deepmind/formal-conjectures", "type": "git", "subDir": null, "scope": "", - "rev": "58b48e75bd19f785927e06912dea610e5e48f1fa", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/google-deepmind/formal-conjectures", - "type": "git", - "subDir": null, - "scope": "", - "rev": "f01550cf4f910c7018f593f47979ab1cc9e8c70e", + "rev": "e6ccabe7bbeecc5c51c5e93152ad2c4acfbff039", "name": "formal_conjectures", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/mhuisi/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "6667b921594697980586296511fab6a359e802d1", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "d3195374a885cf2b0bfa66063deb493686029f95", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", + {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "feac4e0c356b0928657bf3b54fa83ae952f53257", - "name": "MD4Lean", + "rev": "799154a6ee3cefd3c0c89a68a81911fb83b7755c", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": true, + "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca", + "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "v4.27.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f", + "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,51 +55,102 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "eb164a46de87078f27640ee71e6c3841defc2484", + "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407", + "rev": "c04225ee7c0585effbd933662b3151f01b600e40", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.68", + "inputRev": "v0.0.85", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c", + "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3", + "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "240676e9568c254a69be94801889d4b13f3b249f", + "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c7326b06de365308e008bdfe379909e44334a2e2", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "05954ce1797e6bd6b414c916499fe6dda4a11702", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "«formal-conjectures-extractor»", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/formal-conjectures/lakefile.lean b/lean/formal-conjectures/lakefile.lean index 032c248..d136505 100644 --- a/lean/formal-conjectures/lakefile.lean +++ b/lean/formal-conjectures/lakefile.lean @@ -4,8 +4,8 @@ open Lake DSL package «formal-conjectures-extractor» where -- Workspace for extracting formal-conjectures documentation +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main" + require «formal_conjectures» from git "https://github.com/google-deepmind/formal-conjectures" @ "main" - -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "v4.22.0" diff --git a/lean/formal-conjectures/lean-toolchain b/lean/formal-conjectures/lean-toolchain index 6ac6d4c..635bb95 100644 --- a/lean/formal-conjectures/lean-toolchain +++ b/lean/formal-conjectures/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.22.0 +leanprover/lean4:v4.30.0-rc2 \ No newline at end of file diff --git a/lean/mathlib/lake-manifest.json b/lean/mathlib/lake-manifest.json index 68cc3c8..de18ec4 100644 --- a/lean/mathlib/lake-manifest.json +++ b/lean/mathlib/lake-manifest.json @@ -1,71 +1,31 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "7be6082d00bb0cfc1e136505dba7718cd5fcaa84", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0-rc1", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0e16bffea0a1b2664111fb1cfeb46c94e4a92604", + "rev": "700fcd702faa706903e2cde26901b1732c36e951", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "28e0856d4424863a85b18f38868c5420c55f9bae", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "1c5c543d2637aebf90c80aead2d401ae88db13cc", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", - "name": "MD4Lean", + "rev": "799154a6ee3cefd3c0c89a68a81911fb83b7755c", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": true, + "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7311586e1a56af887b1081d05e80c11b6c41d212", + "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60", + "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,41 +55,92 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294", + "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.86", + "inputRev": "v0.0.98", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0", + "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "23324752757bf28124a518ec284044c8db79fee5", + "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", "name": "batteries", "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c7326b06de365308e008bdfe379909e44334a2e2", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "05954ce1797e6bd6b414c916499fe6dda4a11702", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "«mathlib-extractor»", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/mathlib/lakefile.lean b/lean/mathlib/lakefile.lean index f6d3ba3..f2b6f63 100644 --- a/lean/mathlib/lakefile.lean +++ b/lean/mathlib/lakefile.lean @@ -7,8 +7,8 @@ package «mathlib-extractor» where lean_lib «MathExtract» where roots := #[`MathExtract] +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main" + require mathlib from git "https://github.com/leanprover-community/mathlib4.git" - -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "v4.28.0-rc1" diff --git a/lean/mathlib/lean-toolchain b/lean/mathlib/lean-toolchain index 4bafde2..635bb95 100644 --- a/lean/mathlib/lean-toolchain +++ b/lean/mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0-rc1 +leanprover/lean4:v4.30.0-rc2 \ No newline at end of file diff --git a/lean/physlean/PhysExtract.lean b/lean/physlean/PhysExtract.lean index bbfe63d..cbfc3a6 100644 --- a/lean/physlean/PhysExtract.lean +++ b/lean/physlean/PhysExtract.lean @@ -1 +1,2 @@ -import PhysLean +import Physlib +import QuantumInfo diff --git a/lean/physlean/lake-manifest.json b/lean/physlean/lake-manifest.json index e0230f9..f9f03ae 100644 --- a/lean/physlean/lake-manifest.json +++ b/lean/physlean/lake-manifest.json @@ -1,81 +1,41 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/HEPLean/PhysLean", "type": "git", "subDir": null, "scope": "", - "rev": "77ef3eb515ad6bd125c596f0b164349d4a7d5bf5", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/HEPLean/PhysLean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "7ba876c3f5fcd9f67fa2ee9326dd5d0b1e70079a", + "rev": "5b4db3a0254fc18b9af5bcd1f5f7b0ff70e437da", "name": "PhysLean", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "933fce7e893f65969714c60cdb4bd8376786044e", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "84b88f7ac9adf382b9668f852cee82487d616792", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "3ab4379b2b92448717de66b7d3e254ac1487aede", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", + {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", - "name": "MD4Lean", + "rev": "aa4c3e4e14f5b31495b7c7238762ecceddd9f52c", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, + "inputRev": "v4.29.0", + "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67", + "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0", + "inputRev": "v4.29.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11", + "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2", + "rev": "48d5698bc464786347c1b0d859b18f938420f060", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,17 +65,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192", + "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.83", + "inputRev": "v0.0.95", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931", + "rev": "7152850e7b216a0d409701617721b6e469d34bf6", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9312503909aa8e8bb392530145cc1677a6298574", + "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -135,11 +95,62 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3", + "rev": "756e3321fd3b02a85ffda19fef789916223e578c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.29.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/kim-em/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d14544c72b593af6a66131bc34cdab16bf7c0940", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "suppress-reducibility-warning", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9539e34e5cb2d52a6454d9b6218f6b6835cad071", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}], "name": "«physlean-extractor»", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/physlean/lakefile.lean b/lean/physlean/lakefile.lean index b6bbade..b819436 100644 --- a/lean/physlean/lakefile.lean +++ b/lean/physlean/lakefile.lean @@ -4,11 +4,12 @@ open Lake DSL package «physlean-extractor» where -- Workspace for extracting PhysLean documentation +@[default_target] lean_lib «PhysExtract» where roots := #[`PhysExtract] +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "v4.29.0" + require PhysLean from git "https://github.com/HEPLean/PhysLean" - -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "v4.26.0" diff --git a/lean/physlean/lean-toolchain b/lean/physlean/lean-toolchain index e59446d..79ac861 100644 --- a/lean/physlean/lean-toolchain +++ b/lean/physlean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.30.0-rc1 \ No newline at end of file