Register: document provenance, fix conversion implementations. #878
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Calculates the size diffs for the each example binary. Runs when a pull | |
| # request is created or modified. | |
| name: size-diff | |
| # We want to run this on all pull requests. Additionally, GitHub actions merge | |
| # queue needs workflows to run on the `merge_queue` trigger to block merges on | |
| # them. | |
| on: | |
| pull_request: | |
| merge_group: | |
| jobs: | |
| size-diff: | |
| # Using ubuntu-latest can cause breakage when ubuntu-latest is updated to | |
| # point at a new Ubuntu version. Instead, explicitly specify the version, so | |
| # we can update when we need to. This *could* break if we don't update it | |
| # until support for this version is dropped, but it is likely we'll have a | |
| # reason to update to a newer Ubuntu before then anyway. | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| # Clones a single commit from the libtock-rs repository. The commit cloned | |
| # is a merge commit between the PR's target branch and the PR's source. | |
| # We'll later add another commit (the pre-merge target branch) to the | |
| # repository. | |
| - name: Clone repository | |
| uses: actions/checkout@v3 | |
| # The main diff script. Stores the sizes of the example binaries for both | |
| # the merge commit and the target branch. We display the diff in a | |
| # separate step to make it easy to navigate to in the GitHub Actions UI. | |
| # | |
| # If the build on master doesn't work (`make -j2 examples` fails), we | |
| # output a warning message and ignore the error. Ignoring the error | |
| # prevents this workflow from blocking PRs that fix a broken build in | |
| # master. | |
| - name: Compute sizes | |
| run: | | |
| UPSTREAM_REMOTE_NAME="${UPSTREAM_REMOTE_NAME:-origin}" | |
| GITHUB_BASE_REF="${GITHUB_BASE_REF:-master}" | |
| cd "${GITHUB_WORKSPACE}" | |
| make -j2 examples # The VM this runs on has 2 logical cores. | |
| cargo run --release -p print_sizes >'${{runner.temp}}/merge-sizes' | |
| git remote set-branches "${UPSTREAM_REMOTE_NAME}" "${GITHUB_BASE_REF}" | |
| git fetch --depth=1 "${UPSTREAM_REMOTE_NAME}" "${GITHUB_BASE_REF}" | |
| git checkout "${UPSTREAM_REMOTE_NAME}/${GITHUB_BASE_REF}" | |
| make -j2 examples && \ | |
| cargo run --release -p print_sizes >'${{runner.temp}}/base-sizes' || \ | |
| echo 'Broken build on the master branch.' | |
| # Computes and displays the size diff. diff returns a nonzero status code | |
| # if the files differ, and GitHub interprets a nonzero status code as an | |
| # error. To avoid GitHub interpreting a difference as an error, we add | |
| # || exit 0 to the command. This also prevents the workflow from failing | |
| # if the master build is broken and we didn't generate base-sizes. | |
| - name: Size diff | |
| run: diff '${{runner.temp}}/base-sizes' '${{runner.temp}}/merge-sizes' || exit 0 |