How to build releases from tags in my fork

Stream: lean4 dev

[Tobias Grosser]

I am trying to follow:

https://github.com/leanprover/lean4/blob/master/doc/dev/index.md

It is also possible to generate releases that others can use, simply by pushing a tag to your fork of the Lean 4 github repository (and waiting about an hour; check the Actions tab for completion). If you push my-tag to a fork in your github account my_name, you can then put my_name/lean4:my-tag in your lean-toolchain file in a project using lake. (You must use a tag name that does not start with a numeral, or contain _).

[Tobias Grosser]

I pushed new tags to https://github.com/opencompl/lean4/tags named opt-bug-fe986b4

[Tobias Grosser]

I am checking https://github.com/opencompl/lean4/actions to see if some GH action got kicked-off, but no activity is visible.

[Tobias Grosser]

Any idea how to debug this further. This feature would be really useful right now.

[Joscha Mennicken]

As far as I can tell, this is the place where the release should be created. The workflow should be triggered by tag pushes. It should appear in the actions tab shortly after the tag was pushed.

Trying this myself with my own lean4 clone, it seems like GitHub does not trigger workflows when multiple tags are pushed at the same time. To quote the docs:

Events will not be created for tags when more than three tags are pushed at once.

You could try first deleting your pushed tag using git push --delete origin opt-bug-fe986b4 and then re-pushing it (and only it) using git push origin opt-bug-fe986b4. This seemed to work for me at least.

[Tobias Grosser]

That did it for me.

[Tobias Grosser]

Thank you, @Joscha Mennicken