Bumping more often

Stream: nightly-testing

[Joachim Breitner]

Could we increase the frequency of the workflow
https://github.com/leanprover-community/mathlib4/actions/workflows/nightly_bump_toolchain.yml
and/or allow manual trigger?
Sometimes it misses the nightly release and we have to wait for a day.

[Joachim Breitner]

Alternatively we can make that push-based, and add to https://github.com/leanprover/lean4/blob/master/.github/workflows/ci.yml after

      - name: Update release.lean-lang.org
        run: |
          gh workflow -R leanprover/release-index run update-index.yml
        env:
          GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}

a similar section that triggers the nightly_bump_toolchain.yml workflow. Would secrets.MATHLIB4_BOT have the permissions for that (once we add workflow_dispatch to the job?)

[Kim Morrison]

Let's do both, this workflow is cheap and idempotent.

[Kim Morrison]

Indeed, that secret should be sufficient.

[Kim Morrison]

#15142: run every 3 hours (and don't fail if there's nothing to commit)

[Kim Morrison]

#15143: enable workflow dispatch

[Kim Morrison]

@Joachim Breitner, I'll leave it to you to do the push side once that is merged?

[Joachim Breitner]

Will have a look after breakfast, hopefully in time before the nightly.

I'm of a mind of simply creating the commit directly after the release, instead of going through that extra workflow, using the GitHub API to avoid checking mathlib out:
https://stackoverflow.com/a/71130304
Seems simpler. WDYT?

[Joachim Breitner]

OTOH, why bother when the workflow is already written and works. https://github.com/leanprover/lean4/pull/4838.

[Joachim Breitner]

Works:
foo.png