Merge pull request #18 from dranov/bump-v4.8.0

Bump to v4.8.0

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

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",

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.8.0