Skip to content

Add GitHub composite action for installing Agda and standard library#1

Merged
andreasabel merged 5 commits intomasterfrom
copilot/add-agda-installation-action
Nov 14, 2025
Merged

Add GitHub composite action for installing Agda and standard library#1
andreasabel merged 5 commits intomasterfrom
copilot/add-agda-installation-action

Conversation

Copy link
Contributor

Copilot AI commented Nov 14, 2025

Implements a reusable composite action that installs Agda from official releases with optional standard library support.

Implementation

  • Platform detection: Automatically selects correct binary for Linux, Windows, macOS ARM64, and macOS x64
  • Inputs: agda-version (required), agda-stdlib-version (optional)
  • Outputs: agda-path, agda-dir
  • Installation flow: Downloads official release binary → extracts → installs to ~/.local/bin → configures Agda directories → optionally installs stdlib

Usage

- name: Setup Agda
  uses: agda/agda-setup-action@v1
  with:
    agda-version: '2.8.0'
    agda-stdlib-version: '2.3'  # optional

- name: Compile Agda code
  run: agda Main.agda

Files

  • action.yml: Composite action with conditional stdlib installation
  • README.md: Documentation with examples
  • .github/workflows/test.yml: Multi-platform validation (Ubuntu, Windows, macOS ARM/Intel)
  • .github/workflows/example.yml: Usage demonstration with stdlib imports

Binary naming patterns verified against Agda 2.8.0 release: Agda-v{version}-{linux|win64|macOS-arm64|macOS-x64}.{tar.xz|zip}

Warning

Firewall rules blocked me from connecting to one or more addresses (expand for details)

I tried to connect to the following addresses, but was blocked by firewall rules:

  • https://api.github.com/repos/agda/agda/releases
    • Triggering command: curl -s REDACTED (http block)
  • https://api.github.com/repos/agda/agda/releases/latest
    • Triggering command: curl -s REDACTED (http block)

If you need me to access, download, or install something from one of these locations, you can either:

Original prompt

A github composite action that installs Agda from releases at #agda/agda, and possibly the standard library. Input parameters to the action should be the version of Agda and the version of the std-lib. If no std-lib version is given, don't install the std-lib. Outputs: the path to the agda executable and the agda-dir. Usable under images ubuntu/windows/macos-latest & macos-15-intel. Similar to https://github.com/graded-type-theory/graded-type-theory/blob/master/.github/workflows/deploy.yml


✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.

Copilot AI and others added 4 commits November 14, 2025 17:54
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
Copilot AI changed the title [WIP] Add GitHub composite action to install Agda Add GitHub composite action for installing Agda and standard library Nov 14, 2025
Copilot AI requested a review from andreasabel November 14, 2025 18:02
Copy link
Member

@andreasabel andreasabel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great job!

Please address the inline comments, these are minor issues.

module Example where

open import Data.Bool
open import Data.Nat
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Restrict these two imports to the .Base submodules.


steps:
- name: Checkout repository
uses: actions/checkout@v4
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Use v5 of the checkout action, here and everywhere.

jobs:
test-linux:
runs-on: ubuntu-latest
steps:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Refactor this so that there is only one test job but running in a matrix of the four images.

- Ubuntu (latest)
- Windows (latest)
- macOS (latest, including macOS-15-intel)
- Outputs the path to the Agda executable and Agda application directory
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

End each of the 4 main bullet points here with a ".".

Copilot AI added a commit that referenced this pull request Nov 14, 2025
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
@andreasabel andreasabel merged commit 322b4db into master Nov 14, 2025
12 of 15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants