From a45ae63747140c1b2cbad9d46f518015c047047a Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 4 Apr 2024 08:32:09 +0000 Subject: [PATCH] chore: bump toolchain to v4.7.0 (#11864) Co-authored-by: Sebastian Ullrich --- .github/workflows/bors.yml | 2 +- .github/workflows/build.yml | 2 +- .github/workflows/build.yml.in | 2 +- .github/workflows/build_fork.yml | 2 +- lake-manifest.json | 6 +++--- lean-toolchain | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index 4c49350abc..f55d01e9e9 100644 --- a/.github/workflows/bors.yml +++ b/.github/workflows/bors.yml @@ -300,7 +300,7 @@ jobs: run: | git clone https://github.com/leanprover/lean4checker cd lean4checker - git checkout toolchain/v4.7.0-rc1 + git checkout toolchain/v4.7.0 # Now that the git hash is embedded in each olean, # we need to compile lean4checker on the same toolchain cp ../lean-toolchain . diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index a94777b4ec..03356d415e 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -307,7 +307,7 @@ jobs: run: | git clone https://github.com/leanprover/lean4checker cd lean4checker - git checkout toolchain/v4.7.0-rc1 + git checkout toolchain/v4.7.0 # Now that the git hash is embedded in each olean, # we need to compile lean4checker on the same toolchain cp ../lean-toolchain . diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in index 46ee546b5e..e1d777edaa 100644 --- a/.github/workflows/build.yml.in +++ b/.github/workflows/build.yml.in @@ -286,7 +286,7 @@ jobs: run: | git clone https://github.com/leanprover/lean4checker cd lean4checker - git checkout toolchain/v4.7.0-rc1 + git checkout toolchain/v4.7.0 # Now that the git hash is embedded in each olean, # we need to compile lean4checker on the same toolchain cp ../lean-toolchain . diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index 2cc6ebff60..8b80c1aa48 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -304,7 +304,7 @@ jobs: run: | git clone https://github.com/leanprover/lean4checker cd lean4checker - git checkout toolchain/v4.7.0-rc1 + git checkout toolchain/v4.7.0 # Now that the git hash is embedded in each olean, # we need to compile lean4checker on the same toolchain cp ../lean-toolchain . diff --git a/lake-manifest.json b/lake-manifest.json index 3311107301..a6622a9422 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "d4161291e2a4c1c92d710bf670570aa79bf0d6ef", + "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "fd760831487e6835944e7eeed505522c9dd47563", + "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9", + "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lean-toolchain b/lean-toolchain index e35881ce7c..9ad304042c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0-rc2 +leanprover/lean4:v4.7.0