Skip to content

chore(verfication): remove {:only} #517

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

Merged
merged 11 commits into from
Jul 16, 2024
Merged

chore(verfication): remove {:only} #517

merged 11 commits into from
Jul 16, 2024

Conversation

josecorella
Copy link
Contributor

Issue #, if available:

Description of changes:

Squash/merge commit message, if applicable:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

Copy link

It looks like you are adding or removing the dafny keyword {:only}.
Is this intended?

@josecorella josecorella marked this pull request as ready for review July 16, 2024 00:20
@josecorella josecorella requested a review from a team as a code owner July 16, 2024 00:20
Copy link

It looks like you are adding or removing the dafny keyword {:only}.
Is this intended?

Comment on lines +29 to +37
- name: Check if ONLY_KEYWORD is not empty
id: comment
env:
PR_NUMBER: ${{ github.event.number }}
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
ONLY_KEYWORD: ${{ steps.only-keyword.outputs.ONLY_KEYWORD }}
if: ${{env.ONLY_KEYWORD != ''}}
run: |
COMMENT="It looks like you are adding or removing the dafny keyword {:only}.\nIs this intended?"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not just have this action fail? If I'm working on a PR and it does not pass for this reason, that feels like a good thing?

Copy link

It looks like you are adding or removing the dafny keyword {:only}.
Is this intended?

Copy link
Contributor

@seebees seebees left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@josecorella
Copy link
Contributor Author

Although the action, Check {:only} decorator presence / grep-only-verification-keyword is failing it is safe to merge in this instance since we are removing it. The action we have set up is very basic and is made to ensure we fail if we either add it or remove it from code. Since this is the only occurrence of {:only} in the code, the action will never get triggered for removing it, only if we add it. I will merge this as is and make it a required action in the branch protection settings.

@josecorella josecorella merged commit 99072ae into main Jul 16, 2024
57 of 58 checks passed
@josecorella josecorella deleted the jocorell/remove-only branch July 16, 2024 04:02
lucasmcdonald3 pushed a commit to lucasmcdonald3/aws-cryptographic-material-providers-library that referenced this pull request Sep 26, 2024
lucasmcdonald3 pushed a commit to lucasmcdonald3/aws-cryptographic-material-providers-library that referenced this pull request Oct 1, 2024
seebees added a commit that referenced this pull request Oct 17, 2024
* chore: Remove Dafny warnings

Remove all Dafny warnings and set warnings to error.
By removing all the errors, --allow-warnings can be removed from verification. This means that any verification warning will now fail the build. This is especially relevant if {:only} is ever committed. See #517. This would now cause CI verification to fail.
seebees added a commit to aws/aws-database-encryption-sdk-dynamodb that referenced this pull request Mar 20, 2025
Remove all Dafny warnings and set warnings to error.
By removing all the errors,
--allow-warnings can be removed from verification.
This means that any verification warning will now fail the build.
This is especially relevant if {:only} is ever committed.
See aws/aws-cryptographic-material-providers-library#517.
This would now cause CI verification to fail.
seebees added a commit to aws/aws-database-encryption-sdk-dynamodb that referenced this pull request Mar 24, 2025
Remove all Dafny warnings and set warnings to error.
By removing all the errors,
--allow-warnings can be removed from verification.
This means that any verification warning will now fail the build.
This is especially relevant if {:only} is ever committed.
See aws/aws-cryptographic-material-providers-library#517.
This would now cause CI verification to fail.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants