Github Actions to check local PRs

Stream: general

[Marcello Seri]

Is there a standard setup for GitHub Actions to check that PRs against some lean4/mathlib4 project are building (and also to help keeping up to date with mathlib updates)?

[Oliver Butterley]

I'll add a solution which works here because the thread might be useful for others. The page about github CI on the lean community site is outdated. Adding the following to a Github action will build a lean project. Action will fail on a lean error but will succeed even if there are warnings, e.g., from a sorry.

jobs:
  build_project:
    runs-on: ubuntu-latest
    name: Build project
    steps:
      - name: Checkout project
        uses: actions/checkout@v4
      - name: Install elan
        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
      - name: Get cache
        run: ~/.elan/bin/lake exe cache get || true
      - name: Build project
        run: ~/.elan/bin/lake build

Full file: build.yml.
Then one probably wants to do other things like linting, building documentation, building the blueprint. For example as done in in the CLT project push.yml.

[Kim Morrison]

@Oliver Butterley, thanks for this!

Why the -Kenv=dev?

Would you be able to make a PR to correct that information on the community site?

[Oliver Butterley]

No, -Kenv=dev shouldn't be there for this (I'll edit the message). Thanks for the correction!

OK, fairly soon I'll try to write something to update that page.

[Oliver Butterley]

By the way, I noticed that the page about github CI on the lean community site no longer exists in the source. It appears the build setup there updates changed pages but doesn't remove pages which are removed in the source. Anyway, I promised to update that page but did nothing because it appears that it was decided somewhere to remove it instead.

Anyway, I do believe that useful info about using github actions is relevant to many and I'm willing to add some info somewhere. I see that an action is being developed for this task so I believe an update to the documentation can wait for that.

[Oliver Butterley]

Concerning an update workflow, we have been testing our own creation that runs on cron, checks if an update is available, opens a PR if it is available and the updated version builds or opens an issue if the updated version fails to build. Still unclear to us what the preferred behaviour is from the user side but I could turn our sketch into a fully fledged action if that were useful.

[Mario Carneiro]

I don't think they were removed because we don't want them, but rather because the information was misleading because it was too out of date

[Mario Carneiro]

See https://github.com/leanprover-community/leanprover-community.github.io/commit/892d9086699a5676dbc4d24d7909c0ac9b1be212 for the commit which removes that page