Zulip Chat Archive

Stream: lean4

Topic: Missing nightly


Bryan Gin-ge Chen (Feb 12 2021 at 18:34):

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 (Feb 12 2021 at 20:58):

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 (Feb 12 2021 at 21:18):

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

Bryan Gin-ge Chen (Feb 12 2021 at 21:42):

@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 (Feb 12 2021 at 21:56):

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


Last updated: Dec 20 2023 at 11:08 UTC