Fix Kani version parsing in install script

.github/workflows/test-action.yml

@@ -40,7 +40,13 @@ jobs:
 
       - name: Test "Run Kani with older version"
         run: |
-          installed_version=$(kani --version | awk '{print $2}')
+          # Kani 0.67.0 and earlier print `kani <version>`; 0.68.0 and later
+          # print `Kani Rust Verifier <version> (<invocation>)` plus a CBMC line.
+          installed_version=$(
+            kani --version |
+              sed -nE 's/^(Kani Rust Verifier|kani) ([^[:space:]]+).*/\2/p' |
+              head -1
+          )
           expected_version='0.33.0'
 
           if [[ "$installed_version" == "$expected_version" ]]; then
@@ -57,19 +63,18 @@ jobs:
 
       - name: Test "Run Kani with latest version"
         run: |
-          installed_version=$(kani --version | awk '{print $2}')
-          expected_version=$(cargo search kani-verifier | grep -m 1 "kani" | awk '{print $3}' | sed 's/"//g')
+          installed_version=$(
+            kani --version |
+              sed -nE 's/^(Kani Rust Verifier|kani) ([^[:space:]]+).*/\2/p' |
+              head -1
+          )
+          # CARGO_TERM_COLOR=always leaks in from the Rust toolchain action, and
+          # its escape codes would defeat the anchor below.
+          expected_version=$(CARGO_TERM_COLOR=never cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}' | sed 's/"//g')
 
           if [[ "$installed_version" == "$expected_version" ]]; then
             echo "The installed version ($installed_version) matches the latest version ($expected_version)"
           else
             echo "::error::The installed version ($installed_version) does not match the latest version ($expected_version)."
             exit 1
           fi
-
-      - name: Test ProfProof within Kani Action
-        uses: ./
-        with:
-          working-directory: tests/cargo-kani/proptest-lib
-          args: --tests
-          enable-propproof: true

README.md

@@ -33,12 +33,6 @@ If omitted, the latest version of `Kani` hosted on [`Kani's crates.io page`](htt
 - **Default**: `''`
 - **Usage**: These arguments or subcommands will be appended to the Kani command.
 
-`enable-propproof`
-
-- **Description**: Experimental feature that allows Kani to verify [proptest harnesses](https://proptest-rs.github.io/proptest/proptest/index.html) using the PropProof feature.
-- **Default**: `false`
-- **Usage**: If set to `true`, Kani will enable the experimental PropProof feature for verifying proptest harnesses.
-
 ## Example usage in a workflow YAML file:
 
 Here are a few examples of workflow YAML files for the Kani Github Action:
@@ -75,7 +69,7 @@ jobs:
 
 #### Example 3: Run Kani with args
 
-Use latest version of Kani, to run `cargo-kani --tests` on a project with `propproof` harnesses.
+Use latest version of Kani, to run `cargo-kani --tests` on a project.
 
 ```yaml
 jobs:
@@ -86,7 +80,6 @@ jobs:
         uses: model-checking/kani-github-action@v1
         with:
           args: '--tests'
-          enable-propproof: true
 ```
 
 ## Security

action.yml

@@ -26,10 +26,6 @@ inputs:
     description: 'Arguments to pass to kani.'
     required: false
     default: ''
-  enable-propproof:
-    description: 'Experimental: Allow Kani to verify proptest harnesses using the PropProof feature'
-    required: false
-    default: false
 
 runs:
   using: "composite"
@@ -41,21 +37,6 @@ runs:
       run: ${{ github.action_path }}/src/install-kani.sh ${{ inputs.kani-version }}
       shell: bash
 
-    - name: Install PropProof
-      if: ${{ inputs.enable-propproof == 'true' }}
-      uses: actions/checkout@v3
-      with:
-        repository: model-checking/kani
-        ref: features/proptest
-        path: propproof
-        submodules: true
-
-    - name: Add PropProof to config
-      if: ${{ inputs.enable-propproof == 'true' }}
-      shell: bash
-      run: |
-        echo "paths = [\"$GITHUB_WORKSPACE/propproof\"]" > $HOME/.cargo/config.toml
-
     - name: Run Kani
       shell: bash
       run: |

src/install-kani.sh

@@ -12,7 +12,7 @@ fi
 
 # Check exit status for error handling
 if [ $? -eq 0 ]; then
-    echo "Installed Kani $VERSION successfully"
+    echo "Installed Kani $1 successfully"
 else
     echo "::error::Could not install Kani. Please check if the provided version is correct"
     exit 1
@@ -21,19 +21,37 @@ fi
 # Setup kani in ci
 cargo-kani setup;
 
-# Get the current installed version of kani and check it against the latest version
-installed_version=$(kani --version | awk '{print $2}')
+# Get the current installed version of kani and check it against the latest version.
+# Two output formats have to be supported, since this action can install any
+# published version:
+#   - Kani 0.68.0 and later print `Kani Rust Verifier <version> (<invocation>)`,
+#     followed by a `CBMC <version>` line.
+#   - Kani 0.67.0 and earlier used clap's default flag, printing `kani <version>`.
+installed_version=$(
+    kani --version |
+        sed -nE 's/^(Kani Rust Verifier|kani) ([^[:space:]]+).*/\2/p' |
+        head -1
+)
 
-if [ $? -eq 0 ]; then
-    if [ "$1" == "latest" ]; then
-        # Cargo search returns version number as string
-        requested_version=$(cargo search kani-verifier | grep -m 1 "kani-verifier" | awk '{print $3}' | tr -d '"')
-    else
-        requested_version=$1
-    fi
+if [ -z "$installed_version" ]; then
+    echo "::error::Could not determine installed Kani version from \`kani --version\`"
+    exit 1
+fi
 
-    if [ "$installed_version" != "$requested_version" ]; then
-        echo "::error::The version of Kani installed was different than the one requested"
+if [ "$1" == "latest" ]; then
+    # Cargo search returns version number as string. Force color off: the Rust
+    # toolchain action exports CARGO_TERM_COLOR=always, and the escape codes it
+    # adds would otherwise defeat the anchor below.
+    requested_version=$(CARGO_TERM_COLOR=never cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}' | tr -d '"')
+    if [ -z "$requested_version" ]; then
+        echo "::error::Could not determine the latest Kani version from \`cargo search\`"
         exit 1
     fi
+else
+    requested_version=$1
+fi
+
+if [ "$installed_version" != "$requested_version" ]; then
+    echo "::error::The version of Kani installed ($installed_version) was different than the one requested ($requested_version)"
+    exit 1
 fi