set-output is deprecated

Stream: general

[Yaël Dillies]

Are people aware that the set-output command in our CI workflow is deprecated and will stop working on the 31st of May? Are we doing anything to avoid our CI breaking?

[Alex J. Best]

Thanks for the reminder :smile:, I have done some things (#18761 #187612, #18763, #18764, #18765). When these are approved I will forward port to mathlib4.

The file .github/workflows/add_label_from_comment.yml (and the review version) need to be updated quite a bit it seems, to use the fromJSON feature (https://github.blog/changelog/2020-04-15-github-actions-new-workflow-features/#new-fromjson-method-in-expressions) instead of the outdated get-json-paths-action. But this will take a couple of minutes to work out the correct incantation, its probably easier if a maintainer does it anyway seeing as they can actually trigger the ready-to-merge and delegated labels with bors r+ (and then bors r- immediately to cancel) so they can actually test more easily than I could.

[Yaël Dillies]

Thank you for taking this on!

[Alex J. Best]

May I humbly :ping_pong: someone to review these 5 CI update PRs, :up: unfortunately @Ruben Van de Velde went and implemented one of these again and I guess others might too if they keep seeing deprecation warnings on their CI output.

Edit: thanks @Floris van Doorn :check:

[Floris van Doorn]

Thanks for doing this! I delegated two of them, but probably you can immediately merge them.

[Ruben Van de Velde]

Oops, thanks