Implement GH action script.

.github/workflows/release.yml

@@ -36,6 +36,11 @@ jobs:
             echo "Git tag ${{env.TAG_VERSION}} did not match crate version ${{env.CRATE_VERSION}}"
             exit 1
           fi
+          # Check the action script's tag.
+          if ! grep "image: docker://ghcr.io/model-checking/kani.*:${{ env.TAG_VERSION }}" action.yml; then
+            echo "Git tag ${{env.TAG_VERSION}} did not match version in action.yml"
+            exit 1;
+          fi
 
       - name: Create release
         id: create_release

action.yml

@@ -0,0 +1,19 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+name: 'Kani Model Checker'
+description: 'Run the Kani Model Checker on a Cargo Crate'
+author: 'Kani Contributors'
+
+branding:
+  icon: 'cloud'
+  color: 'orange'
+
+runs:
+  using: 'docker'
+  image: docker://ghcr.io/model-checking/kani-ubuntu-20.04:0.9.0
+  args:
+    - bash
+    - '-c'
+    - 'PATH="/root/.cargo/bin:${PATH}"; cargo kani'
+

docs/src/SUMMARY.md

@@ -3,6 +3,7 @@
 - [Getting started](./getting-started.md)
   - [Installation](./install-guide.md)
     - [Building from source](./build-from-source.md)
+    - [GitHub CI Action](./install-github-ci.md)
   - [Using Kani](./usage.md)
   - [Verification results](./verification-results.md)
   - [Debugging verification failures](./debugging-verification-failures.md)

docs/src/install-github-ci.md

@@ -0,0 +1,37 @@
+# GitHub CI Action
+
+Kani offers a GitHub action for running Kani in the CI. As of now,
+only Ubuntu 20.04 wtih `x86_64-unknown-linux-gnu` is supported for
+Kani in the CI.
+
+## Using Kani in Your GitHub Workflow.
+Our GitHub CI Action is available in the GitHub Marketspace with the
+name `model-checking/kani`
+
+The following workflow snippet will checkout your repository and run
+`cargo kani` on it whenever a push or pull request occurs. Replace
+`VER.SION` with the version of Kani you want to run with.
+
+```yaml
+name: Kani CI
+on:
+  pull_request:
+  push:
+jobs:
+  run-kani:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: 'Checkout your code.'
+        uses: actions/checkout@v2
+
+      - name: 'Run Kani on your code.'
+        uses: model-checking/kani@vVER.SION
+```
+
+
+## Configuring Kani with Flags
+
+The github action itself does not take any flags that `cargo kani`
+would take. Instead, they should be configured in `Cargo.toml`. See
+["Configuration in Cargo.toml"](usage.md#configuration-in-cargotoml)
+for details.

docs/src/install-guide.md

@@ -5,7 +5,9 @@ Kani offers an easy installation option on two platforms:
 * `x86_64-unknown-linux-gnu` (Most Linux distributions)
 * `x86_64-apple-darwin` (Intel Mac OS)
 
-Other platforms are either not yet supported or require instead that you [build from source](build-from-source.md).
+Other platforms are either not yet supported or require instead that
+you [build from source](build-from-source.md). To use Kani in in your
+GitHub CI workflows, see [GitHub CI Action](./install-github-ci.md).
 
 ## Dependencies