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

Ltac2: support "head" reduction flag #18273

Merged
merged 1 commit into from Nov 15, 2023
Merged

Ltac2: support "head" reduction flag #18273

merged 1 commit into from Nov 15, 2023

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Nov 7, 2023 •
edited

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 7, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner November 7, 2023 16:23
@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 Nov 7, 2023
@SkySkimmer SkySkimmer added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: changelog entry This should be documented in doc/changelog. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. needs: test-suite update Test case should be added to / updated in the test-suite. and removed needs: changelog entry This should be documented in doc/changelog. labels Nov 7, 2023
@ppedrot ppedrot self-assigned this Nov 7, 2023
@ppedrot ppedrot added this to the 8.19+rc1 milestone Nov 8, 2023
SkySkimmer added a commit to SkySkimmer/coqutil that referenced this pull request Nov 8, 2023
@SkySkimmer
Adapt to coq/coq#18273 (Ltac2 supports head reduction)
579b902
@SkySkimmer SkySkimmer requested a review from a team as a code owner November 8, 2023 12:55
@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 Nov 8, 2023
@SkySkimmer SkySkimmer added needs: overlay This is breaking external developments we track in CI. and removed needs: test-suite update Test case should be added to / updated in the test-suite. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Nov 8, 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 Nov 8, 2023
@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label Nov 8, 2023
samuelgruetter pushed a commit to SkySkimmer/coqutil that referenced this pull request Nov 8, 2023
@SkySkimmer @samuelgruetter
Adapt to coq/coq#18273 (Ltac2 supports head reduction)
f664c81
samuelgruetter pushed a commit to mit-plv/coqutil that referenced this pull request Nov 8, 2023
@SkySkimmer
Adapt to coq/coq#18273 (Ltac2 supports head reduction) (#102)
a80d8c2
@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Nov 9, 2023
@SkySkimmer SkySkimmer removed the needs: overlay This is breaking external developments we track in CI. label Nov 9, 2023
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Nov 9, 2023

🔴 CI failure at commit 33b30c9 without any failure in the test-suite

✔️ Corresponding job for the base commit 1d1cbfe succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-bedrock2
  • You can also pass me a specific list of targets to minimize as arguments.

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Nov 10, 2023
@SkySkimmer SkySkimmer removed the needs: overlay This is breaking external developments we track in CI. label Nov 10, 2023
JasonGross pushed a commit to SkySkimmer/fiat-crypto that referenced this pull request Nov 13, 2023
@SkySkimmer @JasonGross
Adapt to coq/coq#18273 (Ltac2 supports head reduction)
fd25e82
JasonGross pushed a commit to mit-plv/fiat-crypto that referenced this pull request Nov 14, 2023
@SkySkimmer
Adapt to coq/coq#18273 (Ltac2 supports head reduction) (#1725)
6551f87
@SkySkimmer
Copy link
Contributor Author

We need to rerun bedrock2 to get the update fiat crypto commit

@ppedrot
Copy link
Member

ppedrot commented Nov 15, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d342a02 into coq:master Nov 15, 2023
34 checks passed
@SkySkimmer SkySkimmer deleted the ltac2-head-red branch November 16, 2023 08:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

Ltac2 should support weak reduction flag
2 participants
@SkySkimmer @ppedrot