From 799198601969e7b78fdb7fb04a7cd1e0931eee90 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 3 Feb 2026 13:21:47 -0500 Subject: [PATCH] Update README to include instructions for projects using .toml files --- README.md | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 50f8f59..39f8724 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,20 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle ## Adding Duper to an existing project -To use Duper in an existing Lean 4 project, first add this package as a dependency. In your lakefile.lean, add: +To add Duper for `v4.27.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.27.0" +``` +The file `lean-toolchain` should contain the following: +``` +leanprover/lean4:v4.27.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.27.0"