Skip to content

Update dev to match main #75

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
JOSHCLUNE merged 3 commits into from
Mar 28, 2026
Merged

Update dev to match main #75

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4aa43d4
Merge pull request #73 from leanprover-community/dev
JOSHCLUNE Feb 19, 2026
8c18127
Merge pull request #74 from leanprover-community/dev
JOSHCLUNE Mar 28, 2026
301f202
Update README
JOSHCLUNE Mar 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.28.0` to an existing project with a `lakefile.toml` file, add the following dependency:
To add Duper for `v4.29.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.28.0"
rev = "v4.29.0"
```
The file `lean-toolchain` should contain the following:
```
leanprover/lean4:v4.28.0
leanprover/lean4:v4.29.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.28.0"
require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.29.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.
Expand Down
Loading