PR release not being updated

Stream: lean4

[Wojciech Nawrocki]

The original implementation of PR releases for lean4 (lean4#2448) states that "when the PR is updated the release is simply deleted and recreated". However, this doesn't seem to be happening for lean4#2964: the release is still 2 weeks old. Is it not implemented or a bug?

[Matthew Ballard]

I ran into this also recently but pointing the lean-toolchain to leanprover/lean4-pr-releases:pr-release-XXXX seems to work

[Mauricio Collares]

https://github.com/leanprover/lean4/actions/runs/7196319505/job/19600913597 is the job error message. Probably caused by lean4#3055

[Wojciech Nawrocki]

Matthew Ballard said:

I ran into this also recently but pointing the lean-toolchain to leanprover/lean4-pr-releases:pr-release-XXXX seems to work

This just points at the GitHub release I linked which is outdated.

[Matthew Ballard]

I don't know how things are building on my mathlib PR then

[Wojciech Nawrocki]

Mauricio Collares said:

https://github.com/leanprover/lean4/actions/runs/7196319505/job/19600913597 is the job error message. Probably caused by lean4#3055

Ah this is a good lead, but that PR changes a later step than the one that failed.

[Wojciech Nawrocki]

Ah it's already known, lean4#3051

[Mauricio Collares]

lean4#3066 is the revert PR

[Joachim Breitner]

Not a full revert, just the stuff I broke. Sorry for that

[Scott Morrison]

Just caught up with this thread. Things are still broken, but I'm hoping lean4#3070 will fix it, and otherwise hopefully @Joachim Breitner will take over :-)