search

wenkokke / setup-agda

Set up a specific version of Agda for your GitHub Actions workflow.
Other
26 stars 3 forks source link

Upstream to `agda/actions/setup` #32

Open wenkokke opened 2 years ago

wenkokke commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

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 commented 2 years ago

@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 commented 2 years ago

@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 commented 1 year ago

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 commented 1 year ago

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:

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

wenkokke commented 1 year ago

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 commented 11 months ago

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

wenkokke commented 11 months ago

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.