leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.82k stars 325 forks source link

fix: bug in reduceLeDiff simproc proof term #4065

Closed digama0 closed 2 weeks ago

digama0 commented 2 weeks ago

As reported on Zulip.

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

github-actions[bot] commented 2 weeks ago

The backport to releases/v4.8.0 failed:

The process '/usr/bin/git' failed with exit code 1

To backport manually, run these commands in your terminal:

# Fetch latest updates from GitHub
git fetch
# Create a new working tree
git worktree add .worktrees/backport-releases/v4.8.0 releases/v4.8.0
# Navigate to the new working tree
cd .worktrees/backport-releases/v4.8.0
# Create a new branch
git switch --create backport-4065-to-releases/v4.8.0
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 93d7afb00a9acb6ef0648cc2aeef798ca08d6ea9
# Push it to GitHub
git push --set-upstream origin backport-4065-to-releases/v4.8.0
# Go back to the original working tree
cd ../..
# Delete the working tree
git worktree remove .worktrees/backport-releases/v4.8.0

Then, create a pull request where the base branch is releases/v4.8.0 and the compare/head branch is backport-4065-to-releases/v4.8.0.