chore: refactor pr release workflow

[nomeata]

In particular:

• Do not use deprecated potiuk/get-workflow-origin.
• Use a bare checkout to push PR to pr-releases
• Replace script/most-recent-nightly-tag.sh by a one-liner inside the workflow, so that th workflow is self-contained

[nomeata]

I did some testing over at https://github.com/nomeata/lean4/actions/workflows/pr-release.yml and it may actually work.

The cloning and pushing is awfully slow, thought.

Hmm, a bit work needed with the git merge-base.

[nomeata]

I maybe have weeded out all the bugs. Quite tedious, writing and testing such actions. But better double check, or test, or be prepared to use admin rights to revert quickly if it doesn’t work after all.

BTW, can someone delete the tag nightly-2023-11-20 in the lean4 repo? Looks like it was pushed to the wrong repo.

[Kha]

BTW, can someone delete the tag nightly-2023-11-20 in the lean4 repo? Looks like it was pushed to the wrong repo.

Done, thanks

[nomeata]

https://github.com/nomeata/lean4/actions/runs/7092668924/job/19304449256 ran through till the mathlib steps which I did not touch. So might work :-)

[nomeata]

I just learned about --filter=tree:0 for a treeless clone: https://github.blog/2020-12-21-get-up-to-speed-with-partial-clone-and-shallow-clone/

I wonder if this will speed up the job noticably.

[nomeata]

I just learned about --filter=tree:0 for a treeless clone: https://github.blog/2020-12-21-get-up-to-speed-with-partial-clone-and-shallow-clone/

I wonder if this will speed up the job noticably.

Just tried locally. Cloning treeless is super fast, and one can calculate the merge base this way, but then pushing to the other repo is super slow; it seems that git is downloading the missing trees and blobs that it wants to push one by one.

So maybe let's keep it as it is for now.

[kim-em]

This looks good to me.

(I'm going to be flying back to Australia over the weekend; perhaps we can merge this on Monday so I'll be available in case anything unexpected happens.)

[nomeata]

Sounds good! I'll let you merge it when it suits you