Skip to content
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.

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

fix: calculate error suppression per snapshot #4657

Merged
merged 1 commit into from
Jul 8, 2024

Conversation

Kha
Copy link
Member

@Kha Kha commented Jul 5, 2024

Generalizes #3556 to not suppressing errors in tactic steps either when the parse error is in a later step, as otherwise changes to the end of a proof would affect (correctness or effectiveness of) incrementality of preceding steps.

Fixes #4623, in combination with #4643

@Kha Kha requested a review from kim-em as a code owner July 5, 2024 08:33
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 5, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-07-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-07-05 08:49:58)

@Kha Kha added this pull request to the merge queue Jul 8, 2024
Merged via the queue into leanprover:master with commit 4d2f2d7 Jul 8, 2024
16 checks passed
Copy link
Contributor

github-actions bot commented Jul 8, 2024

The backport to releases/v4.9.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.9.0 releases/v4.9.0
# Navigate to the new working tree
cd .worktrees/backport-releases/v4.9.0
# Create a new branch
git switch --create backport-4657-to-releases/v4.9.0
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 4d2f2d7cc59f1df0417f7b58329cbd3fbd2f0906
# Push it to GitHub
git push --set-upstream origin backport-4657-to-releases/v4.9.0
# Go back to the original working tree
cd ../..
# Delete the working tree
git worktree remove .worktrees/backport-releases/v4.9.0

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

Copy link
Contributor

github-actions bot commented Jul 8, 2024

The backport to releases/v4.10.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.10.0 releases/v4.10.0
# Navigate to the new working tree
cd .worktrees/backport-releases/v4.10.0
# Create a new branch
git switch --create backport-4657-to-releases/v4.10.0
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 4d2f2d7cc59f1df0417f7b58329cbd3fbd2f0906
# Push it to GitHub
git push --set-upstream origin backport-4657-to-releases/v4.10.0
# Go back to the original working tree
cd ../..
# Delete the working tree
git worktree remove .worktrees/backport-releases/v4.10.0

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

Kha added a commit that referenced this pull request Jul 9, 2024
Generalizes #3556 to not suppressing errors in tactic steps either when
the parse error is in a later step, as otherwise changes to the end of a
proof would affect (correctness or effectiveness of) incrementality of
preceding steps.

Fixes #4623, in combination with #4643
Kha added a commit that referenced this pull request Jul 9, 2024
Generalizes #3556 to not suppressing errors in tactic steps either when
the parse error is in a later step, as otherwise changes to the end of a
proof would affect (correctness or effectiveness of) incrementality of
preceding steps.

Fixes #4623, in combination with #4643
Kha added a commit to Kha/lean4 that referenced this pull request Jul 9, 2024
Generalizes leanprover#3556 to not suppressing errors in tactic steps either when
the parse error is in a later step, as otherwise changes to the end of a
proof would affect (correctness or effectiveness of) incrementality of
preceding steps.

Fixes leanprover#4623, in combination with leanprover#4643
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backport releases/v4.9.0 backport releases/v4.10.0 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Incremental tactics leading to errors disappearing in proof
2 participants