Add a workflow that runs Verus on each task

[parno]

No description provided.

[parno]

@jaybosamiya It was harder than I expected to figure out how retrieve the latest released version of Verus. I ended up using a custom action that I cobbled together, but it left me wondering if there was a simpler way.

[parno]

Also, when I push to this PR, it appears to run the jobs twice, which seems sub-optimal.

[parno]

@mmcloughlin suggested the following script, which looks much simpler and easier to maintain, so I'm planning to move to that when there's time.

#!/usr/bin/env bash

REPO="verus-lang/verus"

# Determine tag of latest release.
function latest_release_tag() {
    gh release list \
        --repo "${REPO}" \
        --limit 1 \
        --json tagName \
        --template '{{range .}}{{.tagName}}{{end}}'
}

tag=$(latest_release_tag)

# Download the x86 Linux package.
gh release download \
    --repo "${REPO}" \
    "${tag}" \
    --pattern '*-x86-linux.zip' \
    --output "verus.zip"

[jaybosamiya]

Yep, would suggest using something similar to what @mmcloughlin suggested. A few alternative ways to get that URL:

curl -s https://api.github.com/repos/verus-lang/verus/releases | \
  awk -F'"' '/download/{print $4}' | grep x86-linux

curl -s https://api.github.com/repos/verus-lang/verus/releases | \
  jq -r '.[].assets.[].browser_download_url' | grep x86-linux

The running-twice happens because of the push, pull_request; iirc, the push makes it run on the branch's commit itself, and the pull_request runs on a hypothetical merge between the main branch and the branch. My suggestion would be to remove the push portion and/or restrict push to just being on main via a branches filter.

[parno]

With some fiddling, I got a non-JS version working. Thanks for all of the suggestions!