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

Decouple kani version from kani-github-action version #45

Merged
merged 32 commits into from
Sep 27, 2023

Conversation

jaisnan
Copy link
Contributor

@jaisnan jaisnan commented Sep 6, 2023

Description of changes:

This PR updates the action to add the parameter for kani-version which defaults to the value latest.
The default value latest uses the latest version of Kani that is uploaded on crates.io unless a specific version is provided by the user, in which case that specific version of Kani will be used in the CI.

Documentation changes rendered here.

The changes were tested in a local setting and a test project here:

  1. Test for using "latest" by default. Related kani-github-action job here.
  2. Test for using pinned kani version. Related kani-github-action job here.

Resolves: #46

Call-outs:

This would update the action to pull in the latest version by default. Users who don't provide a value for the kani-version parameter would have to set it to pin the kani version that they want to use.

Testing:

  • How is this change tested? Tested locally, Added a CI check for the kani-version parameter, and ran the feature branch of the action on a test github project.

Test for using "latest" by default. Related kani-action here.
Test for using pinned kani version. Related kani-action here.

  • Is this a refactor change? No

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Can you please document in the README.md the inputs the action takes and highlight that if the user doesn't provide the version, the action will install the latest?

Can you also please add tests that give an invalid version and a check that running the action without a version will install the latest version available on crates.io?

.github/workflows/test-action.yml Show resolved Hide resolved
src/install-kani.sh Outdated Show resolved Hide resolved
@jaisnan
Copy link
Contributor Author

jaisnan commented Sep 15, 2023

Update: I've updated documentation with the features and a test for when an invalid version is passed (like 0.47.0 for example). I've also added checks for the version number to ensure that the latest version is installed by default. But I could not automate parsing the error message that appears when an invalid version is passed in subsequent steps.

Rendered documentation here.

Added test here

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Everything looks good, but I would prefer if we can test things a bit better. I'm OK with a follow up PR as long as you manually inspected that the scenarios below work. Thus, I'm approving this one.

Here are the scenarios that I believe should be tested:

  • The default version works and (preferably, check that it is the latest)
  • A specific version works and it matches the requested version
  • An invalid version triggers an error
    • You can use the outcome field of the step context.
    • Note that continue-on-error will continue no matter what, including if the step succeeds.

BTW, I would be OK with testing the installation script separately or test it via github workflow. I prefer the latter though.

.github/workflows/test-action.yml Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Looks good! Thanks @jaisnan! @adpaco-aws do you mind doing a pass on nice the documentation that Jai added please?

One more thing, should we push this to a branch named v1?

README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

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

Documentation looks good to me.

Still think it's a good idea to link mentions of the PropProof feature to our documentation, otherwise they can be confusing.

@jaisnan jaisnan changed the base branch from main to v1 September 27, 2023 17:30
@jaisnan jaisnan merged commit e621a98 into model-checking:v1 Sep 27, 2023
2 checks passed
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.

Decouple Kani-github-action version from Kani
3 participants