Upstream to agda/actions/setup

[wenkokke]

@andreasabel, @UlfNorell, @nad, @asr, and others.

Would you support upstreaming this action to a repository agda/actions in a subdirectory setup? Is the Agda organisation eligible for (reasonably) unlimited and free GitHub Actions usage?

[wenkokke]

@L-TChen With the simple addition of the ability to set agda-version to 'HEAD', this action could probably replace most of Agda’s deploy.yml workflow. It figures out what the latest supported GHC version is, configures and builds Agda, and bundles the binaries & data with icu4c. It doesn’t currently bundle any setup scripts or README files, but those could be added, either here on in deploy.yml. The resulting workflow would only need to download the artefacts and publish them in a rolling nightly release.

[andreasabel]

@wenkokke wrote:

Would you support upstreaming this action to a repository agda/actions in a subdirectory setup? Is the Agda organisation eligible for (reasonably) unlimited and free GitHub Actions usage?

I'd certainly support this! Great to have such an action!

Is the Agda organisation eligible for (reasonably) unlimited and free GitHub Actions usage?

How could I find out?
We haven't run into any restrictions yet. Sometimes jobs are queued for some time, but never long.

Uses of agda/actions/setup would still run on the user's github account, I suppose? So we wouldn't "pay" anything by hosting this action?

[wenkokke]

@andreasabel wrote:

How could I find out? We haven't run into any restrictions yet. Sometimes jobs are queued for some time, but never long.

I believe you’d know. I think actions on public repositories are free, but after the difficulties with Travis CI I figured I’d check.

[wenkokke]

@andreasabel wrote:

Uses of agda/actions/setup would still run on the user's github account, I suppose? So we wouldn't "pay" anything by hosting this action?

Yes, but the weekly builds of latest version and the (possible future) nightly builds that create the binary distributions will still run under the Agda organisation.

[andreasabel]

Uses of agda/actions/setup would still run on the user's github account, I suppose? So we wouldn't "pay" anything by hosting this action?

Yes, but the weekly builds of latest version and the (possible future) nightly builds that create the binary distributions will still run under the Agda organisation.

Ok. We have currently a gazillion builds daily, so this shouldn't matter.

[andreasabel]

@wenkokke : I checked, but I think you already have the right to create new repos on the agda organization, so, welcome to go ahead!

[L-TChen]

@L-TChen With the simple addition of the ability to set agda-version to 'HEAD', this action could probably replace most of Agda’s deploy.yml workflow. It figures out what the latest supported GHC version is, configures and builds Agda, and bundles the binaries & data with icu4c. It doesn’t currently bundle any setup scripts or README files, but those could be added, either here on in deploy.yml. The resulting workflow would only need to download the artefacts and publish them in a rolling nightly release.

Sounds good! I definitely would like to replace most of the deploy.yml by this action. I will do it.

[wenkokke]

This is blocked on #120, because if I upstream the action by transferring the repository, all the binary distribution links break.

Though presumably some light downtime wouldn't be super harmful at the moment, so let's consider it lightly blocked.

[andreasabel]

Would you support upstreaming this action to a repository agda/actions in a subdirectory setup?

I found out that GitHub Marketplace wants single-action repos. Cf:

• Splitting this repo into one repo for each action! haskell/actions#141

Thus, the home would be agda/setup-action or similar, depending on your taste.

[wenkokke]

Ah, I hadn't realised that.

I'm currently still blocked on GitHub Support to figure out why I can't publish this action to the Marketplace, so I guess I wouldn't get to publish it for now anyway, but I'll keep it in mind when doing the migration.

Thanks!

[andreasabel]

@wenkokke : Any news on this?
You could simply transfer this repo to the agda organisation, no renaming needed.
Greetings from AIM XXXVII!

[wenkokke]

For me, the primary blocker on this has been the need to transfer the artifacts to the new repository as well and change all the corresponding URLs on HEAD and all release branches.