Missing nightly

Stream: lean4

[Bryan Gin-ge Chen]

The macOS binary is missing from https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2021-02-12

Out of curiosity I took a look at the macOS job log that should have generated this. For some reason the "Prepare Nightly release" and "Release Nightly" steps were skipped. Could something be going wrong in this line of the workflow config?

[Bryan Gin-ge Chen]

Ah, there seems to be a race condition, where one of the other jobs might push the tag to nightly before the others start on this step. I think it's correct to skip the "Prepare Nightly Release" if that tag has already been pushed, but I think you would still want to run the "Release Nightly" step. I'm not sure of the best way of ensuring this, maybe through another environment variable?

[Sebastian Ullrich]

Thanks, this should be fixed with https://github.com/leanprover/lean4/commit/5db8073c32e580eb4c7669ccf2dcf7b0c95de1c9... hopefully

[Bryan Gin-ge Chen]

@Sebastian Ullrich Thanks! But it seems there's a missing semicolon or something breaking the script: https://github.com/leanprover/lean4/runs/1890427489#step:8:26

[Sebastian Ullrich]

Ah, it's well-known that it's impossible to write a Bash script the correct way on the first try