home cooked release

Stream: lean4

[Matthew Ballard]

Scott added some helpful documentation on making your own release for use in lean-toolchain file in a project.

I thought I should at least write down the learning experiences I had during the process of generating before I forget

[Matthew Ballard]

• After you fork the lean4 repo, make sure that you have GitHub actions enabled.
• Go into settings and make sure there no tag protection rules set.
• Make sure that both the Nix-CI and CI workflows are enabled to run. The first was fine but the second was turned off by default for me.
• I didn't figure out how to avoid the Publish manual step in the Nix-CI workflow so I just deleted it from .github/workflows/nix-ci.yml
• The action for releasing can require additional permission set directly in the .github/workflows/ci.yml. This seems like a known issue and can be fixed by adding

permissions:
  contents: write

after the on: node in the file

[Matthew Ballard]

The last one was especially annoying because I couldn't seem to rerun the CI workflow after changing the ci.yml file without rerunning everything, ie building all the releases for all the platforms + other stuff. Waiting ~2 hrs to find out things went wrong is not fun

[Matthew Ballard]

If had I been aware of this to start, it would have shortened the time to generate the release from ~8 hours to ~2 hours (less head slapping too). Hopefully someone finds it helpful

[Matthew Ballard]

Probably me in 5 years...

[Scott Morrison]

I don't understand why these instructions are so complicated. My experience has been that as long as you have GitHub actions enabled, everything just works?

[Matthew Ballard]

I don’t either but they were very much needed in my case.