Errors: Introducing '--message_format github', for github actions

[mtzguido]

Inspired by @W95Psp 's PR #3491, I thought this could be a nice addition. By setting this flag the warnings and errors look like this:

::warning file=/home/guido/r/fstar/github/ulib/FStar.UInt.fsti,line=435,endLine=435::(271) Pattern uses these theory symbols or terms that should not be in an SMT pattern:   Prims.op_Subtraction

And are automatically picked up by Github actions to be displayed differently in the run log and also tallied at the end of a run

In log:

In workflow page:

In fact, we can also auto-detect if we're running in a Github actions environment by looking for GITHUB_ENV, and default to this format if so. This may be more controversial so I'm separating the patches.

Another option is using --message_format json and piping all output through this filter.

#!/bin/bash

set -eu

# Call this with no arguments and feeding a build log to stdin,
# or with arguments that are filenames to buildogs.

grep '^{' "$@" | while IFS= read -r msg; do
  echo "$msg" # Always echo everything back
  level=$(jq -r .level <<< $msg)
  file=$(jq -r .range.def.file_name <<< $msg)
  # -m: do not fail if file does not exist
  file=$(realpath -m --relative-to=. "${file}")
  line=$(jq -r .range.def.start_pos.line <<< $msg)
  endLine=$(jq -r .range.def.end_pos.line <<< $msg)
  body=$(cat <<< "$msg" | jq -r '.msg | join ("; ")')
  body=$(tr '\n' ' ' <<< $body)
  if [ "${level}" == "Error" ]; then
    glevel=error
  elif [ "${level}" == "Warning" ]; then
    glevel=warning
  else
    # Info message, probably
    continue
  fi
  echo "::${glevel} file=$file,line=$line,endLine=$endLine::$body"
done

This also works fine.. but wouldn't be surprised if it's broken in some edge cases.

[mtzguido]

I thought I could point to the CI run here to show it working, but running inside docker means we don't get GITHUB_ENV.

[mtzguido]

Also a whole other bunch of cool stuff we can do: https://docs.github.com/en/actions/writing-workflows/choosing-what-your-workflow-does/workflow-commands-for-github-actions#setting-an-error-message