From 73e88cbcca87b185f82843faad2986ce343f7bd1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?George=20P=C3=AErlea?= Date: Tue, 25 Jun 2024 11:35:04 +0800 Subject: [PATCH 1/2] Update to lean v4.8.0 --- lake-manifest.json | 8 ++++---- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 31d5b02..1ce420d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,19 +4,19 @@ [{"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "91cd0e81ec8bd16baa2c08e3d00a7f8e473477b4", + "rev": "0f5f39a0336e36ae4ba8ab45b27865ebd9f8f025", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "91cd0e81ec8bd16baa2c08e3d00a7f8e473477b4", + "inputRev": "0f5f39a0336e36ae4ba8ab45b27865ebd9f8f025", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06", + "rev": "51e6e0d24db9341fb031288c298b7e6b56102253", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.8.0-rc2", + "inputRev": "v4.8.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index 51bbe9e..c966e14 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,8 +2,8 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"91cd0e81ec8bd16baa2c08e3d00a7f8e473477b4" -require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.8.0-rc2" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"0f5f39a0336e36ae4ba8ab45b27865ebd9f8f025" +require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.8.0" package Duper { precompileModules := true diff --git a/lean-toolchain b/lean-toolchain index 78f39e2..ef1f67e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc2 +leanprover/lean4:v4.8.0 From 64441b020a41cf6c17288b830d1a685fe1fec44c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?George=20P=C3=AErlea?= Date: Tue, 25 Jun 2024 11:41:23 +0800 Subject: [PATCH 2/2] Update README now that Auto no longer depends on Std --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 2909e10..0d9c979 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ To use Duper in an existing Lean 4 project, first add this package as a dependen require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.13" ``` -Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [std4](https://github.com/leanprover/std4.git), then it uses the same version of std4 as the Duper branch of [Auto](https://github.com/leanprover-community/lean-auto.git). This step is necessary because Duper depends on Auto which depends on std4, so errors can arise if your project attempts to import a version of std4 different from the one imported by Duper. +Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [batteries](https://github.com/leanprover-community/batteries), then it uses the same version of batteries as Duper. This step is necessary because Duper depends on batteries, so errors can arise if your project attempts to import a version of batteries different from the one imported by Duper. After these steps are taken, add the following code to a Lean file that your project's root (usually Main.lean) depends on. ```lean