CI logs should be public

[samuelgruetter]

I think it's really cool that Amazon provides a beefy CI machine for Dafny 😃

However, when I go to https://github.com/dafny-lang/dafny/commits/master and click on the latest green tick to see the build log, I get to a login page. For an open source project, that's really bad: Everyone should be able to see the CI build logs, without having to create an account or be given special permissions.

This is a follow-up on #438.
/cc @robin-aws

[robin-aws]

Hi @samuelgruetter! Yes, I agree it's unfortunate that it's not possible to grant full public access to the build logs. The workaround we're using is the github-codebuild-logs Lambda application, which posts the build logs as a comment on the PRs - you can see some examples on this PR: #459 (look for "AWS CodeBuild CI Report" comments labelled as being from me, since it's using my Oauth token :))

[samuelgruetter]

I see -- so that means I can find the build logs of the branches up for PR, but I can't read the build logs of the merge commits, is that correct?

[robin-aws]

Yeah, that seems to be a limitation of that Lambda application, likely because it only knows how to comment on PRs. I'm not sure where it would attach the information otherwise.

I agree that the workaround isn't that great, and this is going to be a common pain point for any integration with CodeBuild. Let me contact the team and see if there is a better solution out there or in the works.

[robin-aws]

We suspect that using GitHub Actions to trigger CodeBuild and echo the logs will be a much better solution for this. Stay tuned while we investigate!

[robin-aws]

After a lot of discussion and experimentation, I've got a solution ready to go: #558. I thought I'd write down the context, motivation and next steps here, though, since this is one instance of a more general problem we are still investigating.

In this particular case, I switched from Travis to CodeBuild because Travis was failing to build consistently before the 50 minute timeout, and even if it did this is already quite a long build time. However, I've discovered that lit supports splitting test cases into multiple shards, specifically for distributed builds. This lines up well with the GitHub Action build matrix feature (https://help.github.com/en/actions/configuring-and-managing-workflows/configuring-a-workflow#configuring-a-build-matrix), intended to replicate builds for different combinations of operating systems, dependency versions, etc. It can also be used to shard expensive work into multiple smaller builds, and that means we don't necessarily need a single 8-core CodeBuild project to build in a reasonable amount of time.

The relevant part of the PR looks like this:

jobs:
  build:

    runs-on: ${{ matrix.os }}

    strategy:
      matrix:
        os: [ubuntu-latest, windows-latest]
        shard: [1, 2, 3, 4, 5]
      fail-fast: false
    steps:
    ...
    - name: Run lit tests
      run: lit --time-tests -v --num-shards=5 --run-shard=${{ matrix.shard }} dafny/Test

Using GitHub Actions workflows provides a much better user experience, since the logs are directly visible on GitHub for everyone. It also unlocks easy solutions for things like "nightly builds" by triggering on events other than PRs. See the sample run from my fork here: https://github.com/robin-aws/dafny/pull/2/checks

The main disadvantage to this is that there's a limit of 20 concurrent jobs per GitHub account at the free tier: https://help.github.com/en/actions/getting-started-with-github-actions/about-github-actions#usage-limits. We're not in great danger of bumping into that for a while though, and a single GitHub Actions workflow can create up to 256 jobs, it's just that some may queue if you've hit the limit.