Using a custom toolchain from a fork of lean4

Stream: lean4

[Alex Keizer]

EDIT: Of course, the minute after I post this, the issue resolves itself somehow. I guess some CI job was just being very slow.
I'll leave this message for the next person who get's confused by the error

I have a fork of lean4 where I made some changes here. Locally, I've managed to use my modified Lean compiler in a project by using elan toolchain link to my local checkout.

Now I want to record this modified toolchain in the lean-toolchain file, so that others can just download the project and elan automatically picks my fork, without them having to build the modified compiler. Following @Scott Morrison's advice on this zulip message, I created an extensible-injection tag of my fork, and tried to use the toolchain alexkeizer/lean4:extensible-injection, but this fails:

❯ elan toolchain install alexkeizer/lean4:extensible-injection
info: downloading component 'lean'
error: binary package was not provided for 'linux'

Can anybody help me figure out how to make this work?

[Scott Morrison]

@Alex Keizer, even simpler is to make a draft PR to lean4, and then wait until CI completes. If CI succeeded, you will see a toolchain-available label appear on your PR, after which everyone can use the leanprover/lean4-pr-releases:pr-release-NNNN toolchain.