From 3e56459ec9cc7a1b2f6465f5a4208564f9d9d9c3 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 26 May 2026 14:24:44 -0400 Subject: [PATCH] Update README --- README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 659a2d0..ca206e4 100644 --- a/README.md +++ b/README.md @@ -4,23 +4,23 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle ## Adding Duper to an existing project -To add Duper for `v4.29.0` to an existing project with a `lakefile.toml` file, add the following dependency: +To add Duper for `v4.30.0` to an existing project with a `lakefile.toml` file, add the following dependency: ```toml [[require]] name = "Duper" git = "https://github.com/leanprover-community/duper.git" -rev = "v4.29.0" +rev = "v4.30.0" ``` The file `lean-toolchain` should contain the following: ``` -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.30.0 ``` If you have a project with a `lakefile.lean` instead of `lakefile.toml`, you can use this instead: ```lean -require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.29.0" +require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.30.0" ``` 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.