diff --git a/lake-manifest.json b/lake-manifest.json index a0b4902f..59f3c2c4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e", + "rev": "b3debfe6b629192033ef87257e1c60201881646f", "name": "illuminate", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f3f26cc72646205ca167117487c008ee1dafe816", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041", + "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 2694eb76..94b9f495 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0-rc1 +leanprover/lean4:v4.32.0 diff --git a/test-projects/anchor-examples/lake-manifest.json b/test-projects/anchor-examples/lake-manifest.json index 2fe524ce..18e8ebcd 100644 --- a/test-projects/anchor-examples/lake-manifest.json +++ b/test-projects/anchor-examples/lake-manifest.json @@ -1,16 +1,21 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}], - "name": "examples", - "lakeDir": ".lake", - "fixedToolchain": false} +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "efa6467799f50bb896318ef12a1337c14eb3d323", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean" + } + ], + "name": "examples", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/test-projects/documented-package/lake-manifest.json b/test-projects/documented-package/lake-manifest.json index 4fa83e23..4dd88bae 100644 --- a/test-projects/documented-package/lake-manifest.json +++ b/test-projects/documented-package/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b899742d040e9eb946daec33c4d129a73537ae6c", + "rev": "efa6467799f50bb896318ef12a1337c14eb3d323", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/test-projects/literate-config/lake-manifest.json b/test-projects/literate-config/lake-manifest.json index ee111be7..56772caf 100644 --- a/test-projects/literate-config/lake-manifest.json +++ b/test-projects/literate-config/lake-manifest.json @@ -1,53 +1,66 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"type": "path", - "scope": "", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../..", - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "f3f26cc72646205ca167117487c008ee1dafe816", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "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"}, - {"url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}], - "name": "«literate-config-test»", - "lakeDir": ".lake", - "fixedToolchain": false} +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "type": "path", + "scope": "", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../..", + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f3f26cc72646205ca167117487c008ee1dafe816", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "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" + }, + { + "url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + } + ], + "name": "«literate-config-test»", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/test-projects/literate-config/lean-toolchain b/test-projects/literate-config/lean-toolchain index 2694eb76..94b9f495 100644 --- a/test-projects/literate-config/lean-toolchain +++ b/test-projects/literate-config/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0-rc1 +leanprover/lean4:v4.32.0 diff --git a/test-projects/literate-multi-root/lake-manifest.json b/test-projects/literate-multi-root/lake-manifest.json index 978f71a2..50bb46de 100644 --- a/test-projects/literate-multi-root/lake-manifest.json +++ b/test-projects/literate-multi-root/lake-manifest.json @@ -1,53 +1,66 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"type": "path", - "scope": "", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../..", - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "f3f26cc72646205ca167117487c008ee1dafe816", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "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"}, - {"url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}], - "name": "«literate-multi-root-test»", - "lakeDir": ".lake", - "fixedToolchain": false} +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "type": "path", + "scope": "", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../..", + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f3f26cc72646205ca167117487c008ee1dafe816", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "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" + }, + { + "url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + } + ], + "name": "«literate-multi-root-test»", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/test-projects/literate-multi-root/lean-toolchain b/test-projects/literate-multi-root/lean-toolchain index 2694eb76..94b9f495 100644 --- a/test-projects/literate-multi-root/lean-toolchain +++ b/test-projects/literate-multi-root/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0-rc1 +leanprover/lean4:v4.32.0 diff --git a/test-projects/website-examples/lake-manifest.json b/test-projects/website-examples/lake-manifest.json index 1eaf5b07..4c87a293 100644 --- a/test-projects/website-examples/lake-manifest.json +++ b/test-projects/website-examples/lake-manifest.json @@ -6,7 +6,7 @@ "url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, - "rev": "b899742d040e9eb946daec33c4d129a73537ae6c", + "rev": "efa6467799f50bb896318ef12a1337c14eb3d323", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/test-projects/website-literate/lake-manifest.json b/test-projects/website-literate/lake-manifest.json index 4a05c20b..0416fd3b 100644 --- a/test-projects/website-literate/lake-manifest.json +++ b/test-projects/website-literate/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b899742d040e9eb946daec33c4d129a73537ae6c", + "rev": "efa6467799f50bb896318ef12a1337c14eb3d323", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main",