Zulip Chat Archive

Stream: lean4

Topic: Missing nightly


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (Feb 12 2021 at 21:18):

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

view this post on Zulip 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

view this post on Zulip 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: May 07 2021 at 12:15 UTC