From 8c45bbc3bcc5ad951e4561847dafeb277c380cb8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Dec 2024 11:19:35 +1100 Subject: [PATCH] chore: bump toolchain to v4.14.0 --- lake-manifest.json | 18 +++++++++--------- lean-toolchain | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e5fda4d..0cd6f34 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,21 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/acmepjz/md4lean", + [{"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", - "name": "MD4Lean", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014", + "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -31,15 +31,15 @@ "inputRev": "master", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/mhuisi/lean4-cli", + {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, "scope": "", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", - "name": "Cli", + "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "«doc-gen4»", "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index 57a4710..1e70935 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc2 +leanprover/lean4:v4.14.0