No binary for lean PR testing locally

Stream: lean4

[Thomas Murrills]

I noticed that binaries (sometimes?) seem to be only generated for Linux. This makes working on adaptations on the lean-pr-testing-NNNN branch locally awkward. (Here's another message I found about the same issue.)

However, I'm not sure if this is typical now, or is just due to my (experimental) PR modifying basic meta code and updating stage0; I don't recall encountering this issue previously.

I figure the current options are

1. figure out how to make the release yourself from your fork
2. ask a maintainer to add the release-ci label
3. get access to a Linux machine somehow

Are these in fact the only options?

If this is just for stage0-modifying PRs, it's probably not too much of an issue. But I was curious if it's (now) a more widespread phenomenon, given that I saw another message about it. In that case, I'd wonder if it would be worth adding another option—for instance, the ability to add the release-ci label via a comment. (For reference, the PR I'm experimenting with is lean4#5341.)

[Kim Morrison]

They are created for macos as well - we decided not to do windows, balancing fast CI vs me needing the toolchains on Mac regularly.

[Thomas Murrills]

Hmm, I’m currently on Mac as well.

[Thomas Murrills]

(But still got an error message involving ‘darwin’.)

[Kim Morrison]

I added release-ci

[Kim Morrison]

Not sure what's going on. I use release PRs on mac every day.

[Thomas Murrills]

Are you on an M1/2/3 Mac, maybe? (I’m on an older Intel-based Mac.) (No idea if this is relevant.)

[Kim Morrison]

Yes, M2

[Kim Morrison]

Adding the label via a comment seems good. There's an existing workflow for this, so it just needs another case. Happy to merge such a PR.

[Thomas Murrills]

I wonder what the right place is for people to hear that they need to comment release-ci if the PR testing toolchain doesn't work on their device.

I put it in (1.) the pull request template for now, but could also imagine (2.) the PR testing bot comment and/or (3.) the docs linked to by the PR testing bot comment.

(Note: I think simply mentioning that the user can manage the tag if they want leaves too much information off the table, given the rather opaque tooltip on that tag, and the lack of reason to think that toolchain-available might not actually mean that the toolchain you need is available! :) )

[Thomas Murrills]

lean4#5343

[Thomas Murrills]

Out of sheer coincidence, I also noticed that that PR (lean4#5343) was generating every binary in CI even though I hadn't added release-ci! Note that the level, as seen under "configure build matrix" in these logs, is 2 (the level for release CI PRs) when it should be 0.

This led me to a bug: when the check-level is set in the workflow, we get the labels of the PR via gh, but some arguments to gh are unintentionally outside of the command subsitution (e.g. $(gh ...) <args> instead of $(gh ... <args>)).

Fixed in lean4#5344.

[Thomas Murrills]

The relevant bit of logic was

labels="$(gh api repos/leanprover/lean4/pulls/5343) --jq '.labels'"
if echo "$labels" | grep -q "release-ci"; then
  check_level=2
...

The grep was then looking through the entire output of gh api repos/leanprover/lean4/pulls/5343 (with "--jq '.labels'" appended), and since that PR happened to mention release-ci, it dutifully set the check level to 2 and behaved as though it were tagged release-ci!

So, as an ultra-short-term workaround before lean4#5343 is merged, you can generate all toolchains by just adding release-ci to your PR description. :upside_down:

[Kim Morrison]

Oops, thank you for sorting that out!