github/manual-verify: trigger on verification label #17

	name: Verification

	# Run this workflow when manually triggered or when a PR with
	# 'verification' label is created/updated
	on:
	workflow_dispatch:
	pull_request:
	types: [opened, synchronize, reopened, labeled, unlabeled]

	env:
	CARGO_TERM_COLOR: always

	jobs:
	check:
	name: Verification Check
	runs-on: ubuntu-latest
	if: github.event_name == 'workflow_dispatch' \|\| contains(github.event.pull_request.labels.*.name, 'verification')
	steps:
	- name: Checkout
	uses: actions/checkout@v3
	with:
	submodules: recursive

	- name: Install verus toolchains
	run: ./scripts/vinstall.sh --prebuilt-verusfmt

	- name: Format spec/proof code
	run: \|
	verusfmt --check `find ./ -name *.verus.rs` --verus-only

	# cargo-v doesn't propagate the `cargo build` exit code, so we need
	# to check stderr for errors.
	# When https://github.com/microsoft/verismo/issues/23 will be fixed
	# we can remove it.
	- name: Verify svsm with verus
	run: \|
	cargo verify 2>&1 \| tee verify.log
	! grep -q 'cargo build failed' verify.log
	working-directory: kernel

	- name: Verify extra proof libs with verus
	run: \|
	cargo verify 2>&1 \| tee verify.log
	! grep -q 'cargo build failed' verify.log
	working-directory: verification/verify_proof

Provide feedback