Unify Kani bundle CI jobs (rust-lang#2841)

We have two different ways today of building release bundles, one in
`kani.yml` and another one in `release.yml`, and only the `kani.yml`
actually run tests. This is error prone, since the release workflow only
runs during a release without validation tests, and the build can
diverge from what's being tested in CI.

Instead, we will always run the same workflow, except for the steps that
create the release.

Resolves rust-lang#2703

Co-authored-by: Zyad Hassan <[email protected]>

Author: celinval

.github/actions/build-bundle/action.yml

@@ -0,0 +1,92 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Build bundle
+description: "Build the Kani bundle for the current architecture and OS. The inputs must match the worker architecture."
+inputs:
+  arch:
+    description: "Current architecture tuple"
+  os:
+    description: "Current operating system"
+outputs:
+  version:
+    description: "The bundle version (latest or =crate_version)"
+    value: ${{ steps.set_output.outputs.version }}
+  crate_version:
+    description: "The current crate version"
+    value: ${{ steps.set_output.outputs.crate_version }}
+  bundle:
+    description: "The bundle file name"
+    value: ${{ steps.set_output.outputs.bundle }}
+  package:
+    description: "The package file name"
+    value: ${{ steps.set_output.outputs.package }}
+runs:
+  using: composite
+  steps:
+    - name: Export crate version
+      shell: bash
+      run: |
+        echo "CRATE_VERSION=$(cargo pkgid | cut -d@ -f2)" >> $GITHUB_ENV
+
+    - name: Export tag version
+      shell: bash
+      if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }}
+      run: |
+        # GITHUB_REF is refs/tags/kani-0.1.0
+        echo "VERSION=$(echo ${{ github.ref }} | cut -d "-" -f 2)" >> $GITHUB_ENV
+
+    - name: Check Version
+      shell: bash
+      if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }}
+      run: |
+        # Validate git tag & Cargo.toml are in sync on version number
+        if [[ ${{ env.CRATE_VERSION }} != ${{ env.VERSION }} ]]; then
+          echo "Git tag ${{env.VERSION}} did not match crate version ${{env.CRATE_VERSION}}"
+          exit 1
+        fi
+
+    - name: Export latest version
+      shell: bash
+      if: ${{ !startsWith(github.ref, 'refs/tags/kani-') }}
+      run: |
+        echo "VERSION=latest" >> $GITHUB_ENV
+
+    - name: Build bundle
+      shell: bash
+      run: |
+        cargo bundle -- ${{ env.VERSION }}
+        echo "BUNDLE=kani-${{ env.VERSION }}-${{ inputs.arch }}.tar.gz" >> $GITHUB_ENV
+
+    - name: Build package
+      shell: bash
+      run: |
+        cargo package -p kani-verifier
+        mv target/package/kani-verifier-${{ env.CRATE_VERSION }}.crate ${{ inputs.os }}-kani-verifier.crate
+        echo "PKG=${{ inputs.os }}-kani-verifier.crate" >> $GITHUB_ENV
+
+    - name: Upload bundle
+      uses: actions/upload-artifact@v3
+      with:
+        name: ${{ env.BUNDLE }}
+        path: ${{ env.BUNDLE }}
+        if-no-files-found: error
+        # Aggressively short retention: we don't really need these
+        retention-days: 3
+
+    - name: Upload kani-verifier pkg
+      uses: actions/upload-artifact@v3
+      with:
+        name: ${{ env.PKG }}
+        path: ${{ env.PKG }}
+        if-no-files-found: error
+        # Aggressively short retention: we don't really need these
+        retention-days: 3
+
+    - name: Export output
+      shell: bash
+      id: set_output
+      run: |
+        echo "version=${{ env.VERSION }}" >> ${GITHUB_OUTPUT}
+        echo "crate_version=${{ env.CRATE_VERSION }}" >> ${GITHUB_OUTPUT}
+        echo "bundle=${{ env.BUNDLE }}" >> ${GITHUB_OUTPUT}
+        echo "package=${{ env.PKG }}" >> ${GITHUB_OUTPUT}

.github/actions/setup/action.yml

@@ -1,6 +1,7 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 name: Setup Kani Dependencies
+description: "Setup the machine to run Kani. Install rustup, dependencies and sync submodules."
 inputs:
   os:
     description: In which Operating System is this running
@@ -21,12 +22,15 @@ runs:
           sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
           df -h
 
-      - name: Install dependencies
-        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
+      - name: Install Rust toolchain
+        run: |
+          cd ${{ inputs.kani_dir }}
+          ./scripts/setup/install_rustup.sh
+          echo "$HOME/.cargo/bin" >> $GITHUB_PATH
         shell: bash
 
-      - name: Install Rust toolchain
-        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/install_rustup.sh
+      - name: Install dependencies
+        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
         shell: bash
 
       - name: Update submodules

.github/workflows/kani.yml

@@ -144,123 +144,3 @@ jobs:
           branch: gh-pages
           folder: docs/book/
           single-commit: true
-
-  releasebundle-macos:
-    runs-on: ${{ matrix.os }}
-    strategy:
-      matrix:
-        os: [macos-12]
-        include:
-          - os: macos-12
-            artifact: kani-latest-x86_64-apple-darwin.tar.gz
-    steps:
-      - name: Checkout Kani
-        uses: actions/checkout@v3
-
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ${{ matrix.os }}
-
-      - name: Build release bundle
-        run: |
-          cargo bundle -- latest
-          cargo package -p kani-verifier
-
-      # We can't run macos in a container, so we can only test locally.
-      # Hopefully any dependency issues won't be unique to macos.
-      - name: Local install test
-        if: ${{ matrix.os == 'macos-12' }}
-        run: |
-          cargo install --path ./target/package/kani-verifier-*[^e]
-          cargo-kani setup --use-local-bundle ./${{ matrix.artifact }}
-          (cd tests/cargo-kani/simple-lib && cargo kani)
-          (cd tests/cargo-kani/simple-visualize && cargo kani)
-          (cd tests/cargo-kani/build-rs-works && cargo kani)
-
-      - name: Upload artifact
-        uses: actions/upload-artifact@v3
-        with:
-          name: ${{ matrix.artifact }}
-          path: ${{ matrix.artifact }}
-          if-no-files-found: error
-          # Aggressively short retention: we don't really need these
-          retention-days: 3
-
-  releasebundle-ubuntu:
-    runs-on: ubuntu-20.04
-    container:
-      image: ubuntu:18.04
-      volumes:
-        - /usr/local:/mnt/host-local
-    steps:
-      - name: Remove unnecessary software to free up disk space
-        run: |
-          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
-          df -h
-          rm -r /mnt/host-local/lib/android /mnt/host-local/.ghcup
-          df -h
-      # This is required before checkout because the container does not
-      # have Git installed, so cannot run checkout action. The checkout
-      # action requires Git >=2.18, so use the Git maintainers' PPA.
-      - name: Install system dependencies
-        run: |
-          apt-get update
-          apt-get install -y software-properties-common apt-utils
-          add-apt-repository ppa:git-core/ppa
-          apt-get update
-          apt-get install -y \
-            build-essential bash-completion curl lsb-release sudo g++ gcc flex \
-            bison make patch git
-          curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL \
-            https://get.docker.com -o /tmp/install-docker.sh
-          bash /tmp/install-docker.sh
-
-      - name: Checkout Kani
-        uses: actions/checkout@v3
-
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-18.04
-
-      - name: Build release bundle
-        run: |
-          PATH=/github/home/.cargo/bin:$PATH cargo bundle -- latest
-          PATH=/github/home/.cargo/bin:$PATH cargo package -p kani-verifier
-
-      # -v flag: Use docker socket from host as we're running docker-in-docker
-      - name: Build container test
-        run: |
-          for tag in 20-04 20-04-alt 18-04; do
-            >&2 echo "Building test container for ${tag}"
-            docker build -t kani-$tag -f scripts/ci/Dockerfile.bundle-test-ubuntu-$tag .
-          done
-
-      - name: Run installed tests
-        run: |
-          for tag in kani-20-04 kani-20-04-alt kani-18-04; do
-            for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
-              >&2 echo "Tag $tag: running test $dir"
-              docker run -v /var/run/docker.sock:/var/run/docker.sock \
-                -w /tmp/kani/tests/cargo-kani/$dir $tag cargo kani
-            done
-            docker run -v /var/run/docker.sock:/var/run/docker.sock \
-              $tag cargo-kani setup \
-                --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
-          done
-
-          # While the above test OS issues, now try testing with nightly as
-          # default:
-          docker run -v /var/run/docker.sock:/var/run/docker.sock \
-            -w /tmp/kani/tests/cargo-kani/simple-lib kani-20-04  \
-            bash -c "rustup default nightly && cargo kani"
-
-      - name: Upload artifact
-        uses: actions/upload-artifact@v3
-        with:
-          name: kani-latest-x86_64-unknown-linux-gnu.tar.gz
-          path: kani-latest-x86_64-unknown-linux-gnu.tar.gz
-          if-no-files-found: error
-          # Aggressively short retention: we don't really need these
-          retention-days: 3