kani
kani copied to clipboard
model-checking
Possibly create Kani Github Action
It might make things easier for customers if they can simply make use of a github action to run Kani on their code. Ideally this would be as simple as (for example) how we publish our ghpages:
- name: Run proofs
uses: model-checking/kani-github-action@v1
Just heard about a project that would be interested in using an action like this.
By default, it should run cargo kani. But we should also provide the option to call a set of proofs, or exclude some proofs from executing (this is desirable if some proofs are failing, since we don't have the "expect-fail" annotation yet).
Another thing to take into account is that some proofs may need to enable flags. Do we want an annotation for extra flags?
Yeah, I think the idea is for annotations to do that work. I'm not sure if they could be arbitrary flags (easily, that is, it'd take some work to restructure how we do things...)
+1 for this feature. We had potential customers at my mid-internship talk who would be interested in using it in CI. Implementing it would go a long ways in terms of easing adoption.
https://github.com/tokio-rs/prost.git
There are some docker files that already exist for testing the Kani install procedure on different OSes that might serve as a starting point. For instance here is the ubuntu-latest one: https://github.com/model-checking/kani/blob/main/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04
More details in #1587, but I think it would be better experience customer-side if the actions uses a pre-built docker image that is stored on GHCR/ECR. That's how it's done for codeguru etc.
I'll PR the action.yml and test by hosting the image on my fork with GHCR, but I would like a discussion WRT to the permanent solution.
