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.

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

Jump to bottom

Stop automatically using assumption in replace by tac #17964

Merged
merged 1 commit into from Sep 22, 2023
Merged

Stop automatically using assumption in replace by tac #17964

merged 1 commit into from Sep 22, 2023

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Aug 17, 2023 •
edited

@SkySkimmer SkySkimmer requested review from a team as code owners August 17, 2023 08:15
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 17, 2023
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 17, 2023
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Aug 17, 2023
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 17, 2023
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 17, 2023
@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Aug 17, 2023
@ppedrot
Copy link
Member

ppedrot commented Aug 17, 2023

This looks quite non-backwards compatible... Is it worth it? The original bug could be solved much more simply as you commented there.

@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 4, 2023
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels Sep 6, 2023
@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. request: full CI Use this label when you want your next push to trigger a full CI. labels Sep 6, 2023
@SkySkimmer SkySkimmer changed the title Stop automatically using assumption in replace Stop automatically using assumption in replace by tac Sep 6, 2023
@SkySkimmer
Copy link
Contributor Author

OK let's keep the auto assumption when there's no by tac

@SkySkimmer SkySkimmer added the kind: fix This fixes a bug or incorrect documentation. label Sep 6, 2023
@SkySkimmer SkySkimmer added this to the 8.19+rc1 milestone Sep 6, 2023
@ppedrot
Copy link
Member

ppedrot commented Sep 6, 2023

I was more on the line of using tclORELSE0 but if this version of the PR is backwards compatible enough it's also fine.

@Zimmi48 Zimmi48 removed request for a team September 6, 2023 11:50
@ppedrot ppedrot self-assigned this Sep 6, 2023
@SkySkimmer SkySkimmer added needs: overlay This is breaking external developments we track in CI. request: full CI Use this label when you want your next push to trigger a full CI. labels Sep 8, 2023
SkySkimmer added a commit to SkySkimmer/coqutil that referenced this pull request Sep 8, 2023
@SkySkimmer
Stop relying on replace by automatic assumption-based solving
1b632be 
Before coq/coq#17964 `replace foo with bar by tac` actually means
`replace foo with bar by first [assumption | symmetry; assumption | tac]`.
@SkySkimmer SkySkimmer mentioned this pull request Sep 8, 2023
Merged
SkySkimmer added a commit to SkySkimmer/bedrock2 that referenced this pull request Sep 8, 2023
@SkySkimmer
Update coqutil for coq/coq#17964
3c73ba1
SkySkimmer added a commit to SkySkimmer/bignums that referenced this pull request Sep 8, 2023
@SkySkimmer
Stop relying on replace by automatic assumption-based solving
f34bf04 
Before coq/coq#17964 `replace foo with bar by tac` actually means
`replace foo with bar by first [assumption | symmetry; assumption | tac]`.
@SkySkimmer SkySkimmer mentioned this pull request Sep 8, 2023
Merged
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 8, 2023
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 8, 2023
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 8, 2023
SkySkimmer added a commit to coq-community/bignums that referenced this pull request Sep 8, 2023
@SkySkimmer
Better fix for coq/coq#17964: use correct direction of assumption
e78b257 
instead of automatically generated name
proux01 added a commit to coq-community/bignums that referenced this pull request Sep 8, 2023
@proux01
Merge pull request #80 from SkySkimmer/replace
9b7f830 
Better fix for coq/coq#17964: use correct direction of assumption
SkySkimmer added a commit to SkySkimmer/bedrock2 that referenced this pull request Sep 8, 2023
@SkySkimmer
Stop relying on replace by automatic assumption-based solving
27cdf79 
Before coq/coq#17964 `replace foo with bar by tac` actually means
`replace foo with bar by first [assumption | symmetry; assumption | tac]`.
This was referenced Sep 8, 2023
Merged
Merged
SkySkimmer added a commit to SkySkimmer/fiat-crypto that referenced this pull request Sep 11, 2023
@SkySkimmer
Stop relying on replace by automatic assumption-based solving
0b00572 
Before coq/coq#17964 `replace foo with bar by tac` actually means
`replace foo with bar by first [assumption | symmetry; assumption | tac]`.
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 11, 2023
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 11, 2023
@SkySkimmer SkySkimmer removed the needs: overlay This is breaking external developments we track in CI. label Sep 11, 2023
JasonGross pushed a commit to mit-plv/fiat-crypto that referenced this pull request Sep 11, 2023
@SkySkimmer
Stop relying on replace by automatic assumption-based solving (#1657
4bd2596 
)

Before coq/coq#17964 `replace foo with bar by tac` actually means
`replace foo with bar by first [assumption | symmetry; assumption | tac]`.
@ppedrot
Copy link
Member

ppedrot commented Sep 22, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 8ff316d into coq:master Sep 22, 2023
8 checks passed
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 22, 2023

@ppedrot: Please take care of the following overlays:

  • 17964-SkySkimmer-replace-assum.sh

@SkySkimmer SkySkimmer deleted the replace-assum branch September 22, 2023 14:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Zimmi48 approved these changes

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

replace by tac should not mask tac's failure message
3 participants
@SkySkimmer @ppedrot @Zimmi48