Test

Fix windows CI builds #7291

Workflow file for this run

	name: Test

	on:
	push:
	branches: 'master'
	paths-ignore: 'docs/**'
	pull_request:
	branches: 'master'
	paths-ignore: 'docs/**'

	# Cancel previous runs in a PR when pushing new commits
	concurrency:
	group: worflow-${{ github.workflow }}-${{ github.event.pull_request.number \|\| github.ref }}
	# Do not cancel when testing the master branch
	cancel-in-progress: ${{ startsWith(github.ref, 'refs/pull/') }}

	env:
	RUST_BACKTRACE: 1
	PRUSTI_ASSERT_TIMEOUT: 60000

	jobs:
	# Check formatting
	# fmt-check:
	# runs-on: ubuntu-latest
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Check formatting
	# run: \|
	# rustup component add rustfmt
	# python ./x.py fmt-check-all

	# # Run clippy checks
	# clippy-check:
	# runs-on: ubuntu-latest
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Set up Java
	# uses: actions/setup-java@v3
	# with:
	# java-version: '15'
	# distribution: 'zulu'
	# - name: Set up the environment
	# run: python x.py setup
	# - name: Cache cargo
	# uses: Swatinem/rust-cache@v2
	# with:
	# shared-key: "shared"
	# - name: Check and report Clippy errors
	# run: \|
	# python ./x.py clippy-all

	# # Detect missing dependencies in workspace packages
	# # See: https://stackoverflow.com/a/74293494/2491528
	# check-deps:
	# runs-on: ubuntu-latest
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Set up Java
	# uses: actions/setup-java@v3
	# with:
	# java-version: '15'
	# distribution: 'zulu'
	# - name: Set up the environment
	# run: python x.py setup
	# - name: Cache cargo
	# uses: Swatinem/rust-cache@v2
	# with:
	# shared-key: "shared"
	# - name: Compile each workspace package individually
	# run: \|
	# cargo install cargo-hack
	# python ./x.py hack build --workspace

	# # Check that we depend on the compiler only through SMIR.
	# smir-check:
	# runs-on: ubuntu-latest
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Check and report illegal extern crate.
	# run: \|
	# python ./x.py check-smir

	# # Run a subset of the tests that used to fail often.
	# # The goal here is to fail fast and give quick feedback to the developers.
	# # This job intentionally doesn't use the verification cache.
	# quick-tests:
	# runs-on: ubuntu-latest
	# env:
	# PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Set up Java
	# uses: actions/setup-java@v3
	# with:
	# java-version: '15'
	# distribution: 'zulu'
	# - name: Set up the environment
	# run: python x.py setup
	# - name: Cache cargo
	# uses: Swatinem/rust-cache@v2
	# with:
	# shared-key: "shared"
	# - name: Build with cargo
	# run: python x.py build --all
	# - name: Run quick tests
	# run: python x.py test --all quick

	# # Run a subset of the tests with the purification optimization enabled
	# # to ensure that we do not introduce regressions.
	# purification-tests:
	# needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
	# runs-on: ubuntu-latest
	# env:
	# PRUSTI_ENABLE_PURIFICATION_OPTIMIZATION: true
	# PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Set up Java
	# uses: actions/setup-java@v3
	# with:
	# java-version: '15'
	# distribution: 'zulu'
	# - name: Set up the environment
	# run: python x.py setup
	# - name: Cache cargo
	# uses: Swatinem/rust-cache@v2
	# with:
	# shared-key: "shared"
	# - name: Prepare verification cache keys
	# shell: bash
	# run: \|
	# VER_CACHE_KEY_SHARED=prusti-cache-$(cat viper-toolchain)-$(date +%Y-%m)
	# echo "VER_CACHE_KEY_SHARED=$VER_CACHE_KEY_SHARED" >> $GITHUB_ENV
	# echo "VER_CACHE_KEY_UNIQUE=$VER_CACHE_KEY_SHARED-${RANDOM}${RANDOM}" >> $GITHUB_ENV
	# - name: Load verification cache
	# uses: actions/cache@v3
	# with:
	# path: ${{ env.PRUSTI_CACHE_PATH }}
	# # Use a unique key, so that the job will always store the cache at the end of the run
	# key: ${{ env.VER_CACHE_KEY_UNIQUE }}
	# # Restore from the most recent cache that matches a shared prefix of the key
	# restore-keys: ${{ env.VER_CACHE_KEY_SHARED }}
	# - name: Build with cargo
	# run: python x.py build --all
	# - name: Run quick tests
	# run: \|
	# python x.py verify-test prusti-tests/tests/verify/pass/rosetta/Knuth_shuffle.rs
	# # python x.py test --all pass/rosetta/Binary_search_shared.rs
	# # python x.py test --all pass/demos/account.rs
	# # python x.py test --all pass/rosetta/Knights_tour.rs
	# # python x.py test --all pass/quick/fold-unfold.rs
	# # python x.py test --all pass/quick/moves.rs
	# # python x.py test --all pass/quick/mut-borrows.rs
	# # python x.py test --all pass/quick/shared-borrows.rs
	# # python x.py test --all pass/quick/trait-contracts-refinement.rs
	# # python x.py test --all pass/quick/fibonacci.rs
	# # python x.py test --all pass/pure-fn/len-lookup.rs
	# # python x.py test --all pass/pure-fn/quantifiers.rs
	# # python x.py test --all pass/pure-fn/recursive-pure-fn.rs
	# # python x.py test --all pass/pure-fn/ref-mut-arg.rs
	# # python x.py test --all pass/rosetta/Ackermann_function.rs
	# # python x.py test --all pass/rosetta/Heapsort.rs
	# - name: Run with purification.
	# env:
	# PRUSTI_VIPER_BACKEND: silicon
	# PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
	# PRUSTI_VERIFY_CORE_PROOF: true
	# PRUSTI_VERIFY_SPECIFICATIONS: true
	# PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
	# PRUSTI_INLINE_CALLER_FOR: false
	# run: \|
	# python x.py test core_proof
	# - name: Run with purification with Carbon.
	# env:
	# PRUSTI_VIPER_BACKEND: silicon
	# PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: carbon
	# PRUSTI_VERIFY_CORE_PROOF: true
	# PRUSTI_VERIFY_SPECIFICATIONS: true
	# PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
	# PRUSTI_INLINE_CALLER_FOR: false
	# run: \|
	# python x.py test core_proof
	# - name: Run without purification.
	# env:
	# PRUSTI_VIPER_BACKEND: silicon
	# PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
	# PRUSTI_VERIFY_CORE_PROOF: true
	# PRUSTI_VERIFY_SPECIFICATIONS: true
	# PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: true
	# PRUSTI_INLINE_CALLER_FOR: false
	# run: \|
	# python x.py test core_proof
	# - name: Inline caller for functions
	# env:
	# PRUSTI_VIPER_BACKEND: silicon
	# PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
	# PRUSTI_VERIFY_CORE_PROOF: true
	# PRUSTI_VERIFY_SPECIFICATIONS: true
	# PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
	# PRUSTI_INLINE_CALLER_FOR: true
	# run: \|
	# python x.py test core_proof

	# # Run all the tests.
	# all-tests:
	# needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
	# strategy:
	# matrix:
	# os: [ubuntu-latest, windows-latest, macos-latest]
	# fail-fast: false
	# runs-on: ${{ matrix.os }}
	# env:
	# PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Set up Python 3
	# uses: actions/setup-python@v4
	# with:
	# python-version: '3.x'
	# - name: Set up Java
	# uses: actions/setup-java@v3
	# with:
	# java-version: '15'
	# distribution: 'zulu'
	# - name: Set up the environment
	# run: python x.py setup
	# - name: Cache cargo
	# uses: Swatinem/rust-cache@v2
	# with:
	# shared-key: "shared"
	# - name: Prepare verification cache keys
	# shell: bash
	# run: \|
	# VER_CACHE_KEY_SHARED=prusti-cache-$(cat viper-toolchain)-$(date +%Y-%m)
	# echo "VER_CACHE_KEY_SHARED=$VER_CACHE_KEY_SHARED" >> $GITHUB_ENV
	# echo "VER_CACHE_KEY_UNIQUE=$VER_CACHE_KEY_SHARED-${RANDOM}${RANDOM}" >> $GITHUB_ENV
	# - name: Load verification cache
	# uses: actions/cache@v3
	# with:
	# path: ${{ env.PRUSTI_CACHE_PATH }}
	# # Use a unique key, so that the job will always store the cache at the end of the run
	# key: ${{ env.VER_CACHE_KEY_UNIQUE }}
	# # Restore from the most recent cache that matches a shared prefix of the key
	# restore-keys: ${{ env.VER_CACHE_KEY_SHARED }}
	# - name: Build with cargo
	# run: python x.py build --all --jobs 1
	# - name: Run cargo tests
	# run: python x.py test --all
	# - name: Run a subset of tests with Carbon
	# run: \|
	# python x.py test pass/no-annotation --all --verbose
	# env:
	# PRUSTI_VIPER_BACKEND: carbon
	# - name: Check prusti-contracts
	# run: \|
	# cd prusti-contracts/prusti-contracts-test/
	# cargo +stable build
	# - name: "Windows debugging: show open file handles for any running process"
	# if: matrix.os == 'windows-latest' && failure()
	# shell: cmd
	# run: \|
	# C:\msys64\usr\bin\wget.exe https://download.sysinternals.com/files/Handle.zip
	# 7z x Handle.zip
	# handle.exe -u -nobanner -accepteula

	release-build:
	needs: []
	# needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
	strategy:
	matrix:
	os: [windows-latest]
	# os: [ubuntu-latest, windows-latest, macos-latest]
	fail-fast: false
	runs-on: ${{ matrix.os }}
	steps:
	- name: Check out the repo
	uses: actions/checkout@v3

	- name: Set up Python 3
	uses: actions/setup-python@v4
	with:
	python-version: '3.x'

	- name: Set up Java
	uses: actions/setup-java@v3
	with:
	java-version: '15'
	distribution: 'zulu'

	- name: Set up the environment
	run: python x.py setup

	- name: Build with cargo --release
	run: python x.py build --release ${{ matrix.os == 'windows-latest' && '--target x86_64-pc-windows-msvc' \|\| '' }}

	# Run Prusti on itself.
	# Disabled because of a bug when compiling jni-gen
	# test-on-prusti:
	# needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
	# runs-on: ubuntu-latest
	# if: false
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Set up Java
	# uses: actions/setup-java@v3
	# with:
	# java-version: '15'
	# distribution: 'zulu'
	# - name: Set up the environment
	# run: python x.py setup
	# - name: Cache cargo
	# uses: Swatinem/rust-cache@v2
	# with:
	# shared-key: "shared"
	# - name: Build with cargo
	# run: python x.py build --release --all
	# - name: Run cargo-prusti on Prusti
	# run: python x.py exec target/release/cargo-prusti
	# env:
	# PRUSTI_SKIP_UNSUPPORTED_FEATURES: true
	# PRUSTI_FULL_COMPILATION: true
	# PRUSTI_CHECK_PANICS: false
	# PRUSTI_CHECK_OVERFLOWS: false
	# PRUSTI_INTERNAL_ERRORS_AS_WARNINGS: true

	# # Test cargo-prusti on a collection of crates.
	# test-crates:
	# needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
	# runs-on: ubuntu-22.04
	# strategy:
	# matrix:
	# shard_index: [0, 1, 2, 3]
	# steps:
	# - name: Check out the repo
	# uses: actions/checkout@v3
	# - name: Setup Python 3
	# uses: actions/setup-python@v4
	# with:
	# python-version: '3.x'
	# - name: Set up Java
	# uses: actions/setup-java@v3
	# with:
	# java-version: '15'
	# distribution: 'zulu'
	# - name: Set up the environment
	# run: python x.py setup
	# - name: Cache cargo
	# uses: Swatinem/rust-cache@v2
	# with:
	# shared-key: "shared"
	# - name: Build with cargo --release
	# run: \|
	# python x.py build --release -p prusti
	# python x.py build --release -p prusti-launch
	# python x.py build --release -p test-crates
	# - name: Test Prusti on a collection of crates
	# run: ./target/release/test-crates --fail-fast --num-shards=4 --shard-index=${{ matrix.shard_index }}

	# # Dummy job to specify the jobs that must pass before merging on master
	# can-merge:
	# runs-on: ubuntu-latest
	# needs: [all-tests, purification-tests, release-build, test-crates]
	# # Always run, even if the workflow was cancelled
	# if: ${{ always() }}
	# steps:
	# - name: Fail if the workflow failed or was cancelled
	# uses: re-actors/alls-green@release/v1
	# with:
	# jobs: ${{ toJSON(needs) }}

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix windows CI builds #7291

Workflow file

Fix windows CI builds #7291

Jobs

Run details

Workflow file for this run