Skip to content

Install Kani into the action, instead of using a docker#1724

Closed
danielsn wants to merge 7 commits intomodel-checking:mainfrom
danielsn:test-action
Closed

Install Kani into the action, instead of using a docker#1724
danielsn wants to merge 7 commits intomodel-checking:mainfrom
danielsn:test-action

Conversation

@danielsn
Copy link
Copy Markdown
Contributor

@danielsn danielsn commented Sep 27, 2022

Description of changes:

Currently, the action requires a docker, which is not yet published. Instead, as a temporary solution, just install the dependencies every time.

Resolved issues:

Resolves #1589

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

  • Installing the dependencies takes about 1-1.5 minutes according to some initial testing.

Testing:

  • How is this change tested? Made a repo with Kani proofs, ran this action on it.

  • 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.

@danielsn danielsn requested a review from a team as a code owner September 27, 2022 20:42
Comment thread action.yml Outdated
Copy link
Copy Markdown
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.

I do have one concern regarding how we are using our repository. I was puzzled about having the action.yml in the root of the repository. So I decided to read a bit more about actions. This is basically the first thing in their documentation:

When you plan to publish your action to GitHub Marketplace, you'll need ensure that the repository only includes the metadata file, code, and files necessary for the action.

https://docs.github.com/en/actions/creating-actions/publishing-actions-in-github-marketplace

# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
name: Kani Action Check
on: pull_request
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

why not push?

@tedinski
Copy link
Copy Markdown
Contributor

That's a pretty good point. We should have a kani-action repo or something?

Comment thread action.yml
- name: Install Kani
shell: bash
run: |
export KANI_VERSION="0.11.0"; \
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Should we retrieve the version from the repository instead? I was also wondering if we should allow users to choose the version they want to use so they can control when to update Kani.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

My thought was action version matches kani-version. So we have kani-action@0.11 matches kani 0.11

@celinval
Copy link
Copy Markdown
Contributor

@danielsn Can we close this PR since we have published the Action in a different repo?

@celinval celinval closed this Nov 15, 2022
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.

3 participants