From efe541ca11eccb8c03982ea947d8489b9b8b326f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 14 Nov 2025 17:51:07 +0000 Subject: [PATCH 1/7] Initial plan From 930ad4baaff2b5219a49471a9409c70f2a16df10 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 14 Nov 2025 17:54:26 +0000 Subject: [PATCH 2/7] Implement agda-setup-action composite action Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com> --- README.md | 103 ++++++++++++++++++++++++++++- action.yml | 185 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 287 insertions(+), 1 deletion(-) create mode 100644 action.yml diff --git a/README.md b/README.md index fca1abb..80f7030 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,103 @@ # agda-setup-action -Github action to install Agda from the official deployed binaries + +GitHub composite action to install Agda from the official deployed binaries and optionally the Agda standard library. + +## Features + +- Installs Agda from official GitHub releases +- Optional installation of the Agda standard library +- Cross-platform support: + - Ubuntu (latest) + - Windows (latest) + - macOS (latest, including macOS-15-intel) +- Outputs the path to the Agda executable and Agda application directory + +## Usage + +### Basic Usage (Agda only) + +```yaml +- name: Setup Agda + uses: agda/agda-setup-action@v1 + with: + agda-version: '2.8.0' +``` + +### With Standard Library + +```yaml +- name: Setup Agda with stdlib + uses: agda/agda-setup-action@v1 + with: + agda-version: '2.8.0' + agda-stdlib-version: '2.3' +``` + +### Using Outputs + +```yaml +- name: Setup Agda + id: setup-agda + uses: agda/agda-setup-action@v1 + with: + agda-version: '2.8.0' + agda-stdlib-version: '2.3' + +- name: Use Agda + run: | + echo "Agda path: ${{ steps.setup-agda.outputs.agda-path }}" + echo "Agda dir: ${{ steps.setup-agda.outputs.agda-dir }}" + agda --version +``` + +## Inputs + +| Name | Description | Required | Default | +|------|-------------|----------|---------| +| `agda-version` | Version of Agda to install (e.g., `2.8.0`) | Yes | - | +| `agda-stdlib-version` | Version of Agda standard library to install (e.g., `2.3`). If not specified, stdlib will not be installed. | No | `''` | + +## Outputs + +| Name | Description | +|------|-------------| +| `agda-path` | Path to the Agda executable | +| `agda-dir` | Path to the Agda application directory | + +## Example Workflow + +```yaml +name: Build with Agda + +on: [push, pull_request] + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + + - name: Setup Agda + uses: agda/agda-setup-action@v1 + with: + agda-version: '2.8.0' + agda-stdlib-version: '2.3' + + - name: Build Agda files + run: agda Main.agda +``` + +## Platform Support + +This action supports the following platforms: +- `ubuntu-latest` +- `windows-latest` +- `macos-latest` +- `macos-15-intel` + +The action automatically detects the platform and downloads the appropriate binary for your runner. + +## License + +This project is licensed under the same terms as Agda itself. diff --git a/action.yml b/action.yml new file mode 100644 index 0000000..b68e3ca --- /dev/null +++ b/action.yml @@ -0,0 +1,185 @@ +name: 'Setup Agda' +description: 'Install Agda from official releases and optionally the standard library' +author: 'Agda Team' + +inputs: + agda-version: + description: 'Version of Agda to install (e.g., 2.8.0)' + required: true + agda-stdlib-version: + description: 'Version of Agda standard library to install (e.g., 2.3). If not specified, stdlib will not be installed.' + required: false + default: '' + +outputs: + agda-path: + description: 'Path to the Agda executable' + value: ${{ steps.setup-agda.outputs.agda-path }} + agda-dir: + description: 'Path to the Agda application directory' + value: ${{ steps.setup-agda.outputs.agda-dir }} + +runs: + using: 'composite' + steps: + - name: Determine platform + id: platform + shell: bash + run: | + case "${{ runner.os }}" in + Linux) + echo "os=linux" + echo "archive-ext=tar.xz" + echo "archive-name=Agda-v${{ inputs.agda-version }}-linux.tar.xz" + ;; + Windows) + echo "os=windows" + echo "archive-ext=zip" + echo "archive-name=Agda-v${{ inputs.agda-version }}-windows.zip" + ;; + macOS) + # Determine if we're on Intel or ARM + if [[ "${{ runner.arch }}" == "X64" ]]; then + echo "os=macos-intel" + echo "archive-ext=tar.xz" + echo "archive-name=Agda-v${{ inputs.agda-version }}-macos-intel.tar.xz" + else + echo "os=macos" + echo "archive-ext=tar.xz" + echo "archive-name=Agda-v${{ inputs.agda-version }}-macos.tar.xz" + fi + ;; + *) + echo "Unsupported OS: ${{ runner.os }}" + exit 1 + ;; + esac >> "${GITHUB_OUTPUT}" + + - name: Download Agda ${{ inputs.agda-version }} + shell: bash + run: | + archive_name="${{ steps.platform.outputs.archive-name }}" + download_url="https://github.com/agda/agda/releases/download/v${{ inputs.agda-version }}/${archive_name}" + + echo "Downloading Agda from: ${download_url}" + http_code=$(curl -w '%{http_code}\n' -L "${download_url}" -o "agda-archive.${{ steps.platform.outputs.archive-ext }}") + exit_code=$? + + echo "curl exit code: ${exit_code}" + echo "curl http code: ${http_code}" + + if [[ "${exit_code}" != "0" || "${http_code}" != "200" ]]; then + echo "Download of Agda archive failed." + exit 1 + fi + + - name: Extract Agda (Unix) + if: runner.os != 'Windows' + shell: bash + run: | + tar xf "agda-archive.${{ steps.platform.outputs.archive-ext }}" + + - name: Extract Agda (Windows) + if: runner.os == 'Windows' + shell: pwsh + run: | + Expand-Archive -Path "agda-archive.${{ steps.platform.outputs.archive-ext }}" -DestinationPath . + + - name: Install Agda (Unix) + if: runner.os != 'Windows' + shell: bash + run: | + mkdir -p "${HOME}/.local/bin/" + if [[ -f "agda" ]]; then + mv agda "${HOME}/.local/bin/" + elif [[ -f "bin/agda" ]]; then + mv bin/agda "${HOME}/.local/bin/" + else + echo "Could not find agda executable in archive" + ls -la + exit 1 + fi + echo "${HOME}/.local/bin" >> "${GITHUB_PATH}" + + - name: Install Agda (Windows) + if: runner.os == 'Windows' + shell: pwsh + run: | + $installPath = Join-Path $env:USERPROFILE ".local\bin" + New-Item -ItemType Directory -Force -Path $installPath | Out-Null + + if (Test-Path "agda.exe") { + Move-Item -Path "agda.exe" -Destination $installPath -Force + } elseif (Test-Path "bin\agda.exe") { + Move-Item -Path "bin\agda.exe" -Destination $installPath -Force + } else { + Write-Error "Could not find agda.exe in archive" + Get-ChildItem -Recurse + exit 1 + } + + "$installPath" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append + + - name: Setup Agda directories + id: setup-agda + shell: bash + run: | + agda --version + agda --setup + + if [[ "${{ runner.os }}" == "Windows" ]]; then + AGDA_DIR=$(agda --print-agda-app-dir | sed 's/\\/\//g') + else + AGDA_DIR=$(agda --print-agda-app-dir) + fi + + mkdir -p "${AGDA_DIR}" + mkdir -p "${AGDA_DIR}/libraries.d" + + # Find agda executable path + if [[ "${{ runner.os }}" == "Windows" ]]; then + AGDA_PATH=$(where agda | head -1) + else + AGDA_PATH=$(which agda) + fi + + echo "agda-dir=${AGDA_DIR}" >> "${GITHUB_OUTPUT}" + echo "agda-path=${AGDA_PATH}" >> "${GITHUB_OUTPUT}" + echo "AGDA_DIR=${AGDA_DIR}" >> "${GITHUB_ENV}" + + - name: Download Agda standard library + if: inputs.agda-stdlib-version != '' + shell: bash + run: | + download_url="https://github.com/agda/agda-stdlib/archive/refs/tags/v${{ inputs.agda-stdlib-version }}.tar.gz" + + echo "Downloading Agda standard library from: ${download_url}" + http_code=$(curl -w '%{http_code}\n' -L "${download_url}" -o "agda-stdlib.tar.gz") + exit_code=$? + + echo "curl exit code: ${exit_code}" + echo "curl http code: ${http_code}" + + if [[ "${exit_code}" != "0" || "${http_code}" != "200" ]]; then + echo "Download of Agda standard library archive failed." + exit 1 + fi + + tar xf agda-stdlib.tar.gz -C "${AGDA_DIR}/libraries.d/" + + - name: Setup Agda standard library + if: inputs.agda-stdlib-version != '' + shell: bash + run: | + stdlib_path="${AGDA_DIR}/libraries.d/agda-stdlib-${{ inputs.agda-stdlib-version }}/standard-library.agda-lib" + + if [[ ! -f "${stdlib_path}" ]]; then + echo "Standard library file not found at: ${stdlib_path}" + echo "Contents of libraries.d:" + ls -la "${AGDA_DIR}/libraries.d/" + exit 1 + fi + + echo "${stdlib_path}" >> "${AGDA_DIR}/libraries" + echo "Agda libraries file content:" + cat "${AGDA_DIR}/libraries" From 51c0389a7dc84a5fe784be96ff21e6c2e9563068 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 14 Nov 2025 17:56:26 +0000 Subject: [PATCH 3/7] Fix archive naming and simplify extraction logic Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com> --- .github/workflows/test.yml | 97 ++++++++++++++++++++++++++++++++++++++ action.yml | 32 +++---------- 2 files changed, 104 insertions(+), 25 deletions(-) create mode 100644 .github/workflows/test.yml diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml new file mode 100644 index 0000000..e9e2a03 --- /dev/null +++ b/.github/workflows/test.yml @@ -0,0 +1,97 @@ +name: Test Action + +on: + push: + branches: + - main + - master + - 'copilot/**' + pull_request: + workflow_dispatch: + +jobs: + test-linux: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Setup Agda + id: setup + uses: ./ + with: + agda-version: '2.8.0' + agda-stdlib-version: '2.3' + + - name: Verify Agda installation + run: | + echo "Agda path: ${{ steps.setup.outputs.agda-path }}" + echo "Agda dir: ${{ steps.setup.outputs.agda-dir }}" + agda --version + + - name: Create test file + run: | + cat > test.agda << 'EOF' + module test where + + data Bool : Set where + true false : Bool + EOF + + - name: Test Agda + run: agda test.agda + + test-windows: + runs-on: windows-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Setup Agda + id: setup + uses: ./ + with: + agda-version: '2.8.0' + + - name: Verify Agda installation + run: | + echo "Agda path: ${{ steps.setup.outputs.agda-path }}" + echo "Agda dir: ${{ steps.setup.outputs.agda-dir }}" + agda --version + + test-macos: + runs-on: macos-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Setup Agda + id: setup + uses: ./ + with: + agda-version: '2.8.0' + agda-stdlib-version: '2.3' + + - name: Verify Agda installation + run: | + echo "Agda path: ${{ steps.setup.outputs.agda-path }}" + echo "Agda dir: ${{ steps.setup.outputs.agda-dir }}" + agda --version + + test-macos-intel: + runs-on: macos-13 # Intel-based macOS + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Setup Agda + id: setup + uses: ./ + with: + agda-version: '2.8.0' + + - name: Verify Agda installation + run: | + echo "Agda path: ${{ steps.setup.outputs.agda-path }}" + echo "Agda dir: ${{ steps.setup.outputs.agda-dir }}" + agda --version diff --git a/action.yml b/action.yml index b68e3ca..6aafe91 100644 --- a/action.yml +++ b/action.yml @@ -35,18 +35,18 @@ runs: Windows) echo "os=windows" echo "archive-ext=zip" - echo "archive-name=Agda-v${{ inputs.agda-version }}-windows.zip" + echo "archive-name=Agda-v${{ inputs.agda-version }}-win64.zip" ;; macOS) # Determine if we're on Intel or ARM if [[ "${{ runner.arch }}" == "X64" ]]; then - echo "os=macos-intel" + echo "os=macos-x64" echo "archive-ext=tar.xz" - echo "archive-name=Agda-v${{ inputs.agda-version }}-macos-intel.tar.xz" + echo "archive-name=Agda-v${{ inputs.agda-version }}-macOS-x64.tar.xz" else - echo "os=macos" + echo "os=macos-arm64" echo "archive-ext=tar.xz" - echo "archive-name=Agda-v${{ inputs.agda-version }}-macos.tar.xz" + echo "archive-name=Agda-v${{ inputs.agda-version }}-macOS-arm64.tar.xz" fi ;; *) @@ -90,15 +90,7 @@ runs: shell: bash run: | mkdir -p "${HOME}/.local/bin/" - if [[ -f "agda" ]]; then - mv agda "${HOME}/.local/bin/" - elif [[ -f "bin/agda" ]]; then - mv bin/agda "${HOME}/.local/bin/" - else - echo "Could not find agda executable in archive" - ls -la - exit 1 - fi + mv agda "${HOME}/.local/bin/" echo "${HOME}/.local/bin" >> "${GITHUB_PATH}" - name: Install Agda (Windows) @@ -107,17 +99,7 @@ runs: run: | $installPath = Join-Path $env:USERPROFILE ".local\bin" New-Item -ItemType Directory -Force -Path $installPath | Out-Null - - if (Test-Path "agda.exe") { - Move-Item -Path "agda.exe" -Destination $installPath -Force - } elseif (Test-Path "bin\agda.exe") { - Move-Item -Path "bin\agda.exe" -Destination $installPath -Force - } else { - Write-Error "Could not find agda.exe in archive" - Get-ChildItem -Recurse - exit 1 - } - + Move-Item -Path "agda.exe" -Destination $installPath -Force "$installPath" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append - name: Setup Agda directories From 3f18b1c0edab9ab6cc39704df9fd2f36c211cdb8 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 14 Nov 2025 17:57:55 +0000 Subject: [PATCH 4/7] Add example workflow and .gitignore Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com> --- .github/workflows/example.yml | 39 +++++++++++++++++++++++++++++++++++ .gitignore | 24 +++++++++++++++++++++ 2 files changed, 63 insertions(+) create mode 100644 .github/workflows/example.yml create mode 100644 .gitignore diff --git a/.github/workflows/example.yml b/.github/workflows/example.yml new file mode 100644 index 0000000..8d9a596 --- /dev/null +++ b/.github/workflows/example.yml @@ -0,0 +1,39 @@ +name: Example Usage + +on: [push, pull_request] + +jobs: + example: + runs-on: ubuntu-latest + + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Setup Agda + id: setup-agda + uses: agda/agda-setup-action@v1 + with: + agda-version: '2.8.0' + agda-stdlib-version: '2.3' + + - name: Show Agda info + run: | + echo "Agda path: ${{ steps.setup-agda.outputs.agda-path }}" + echo "Agda dir: ${{ steps.setup-agda.outputs.agda-dir }}" + agda --version + + - name: Create a simple Agda file + run: | + cat > Example.agda << 'EOF' + module Example where + + open import Data.Bool + open import Data.Nat + + example : Bool + example = true + EOF + + - name: Type-check Agda file + run: agda Example.agda diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..1818a89 --- /dev/null +++ b/.gitignore @@ -0,0 +1,24 @@ +# Temporary files +*.tmp +*.temp +/tmp/ + +# Archive files used during testing +*.tar.xz +*.tar.gz +*.zip + +# Agda build artifacts +*.agdai +_build/ + +# OS files +.DS_Store +Thumbs.db + +# IDE files +.vscode/ +.idea/ +*.swp +*.swo +*~ From 7b55b2f4b9d36db6989f5f89ff75470480ba15da Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 14 Nov 2025 18:00:17 +0000 Subject: [PATCH 5/7] Add explicit permissions to workflows for security Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com> --- .github/workflows/example.yml | 3 +++ .github/workflows/test.yml | 3 +++ 2 files changed, 6 insertions(+) diff --git a/.github/workflows/example.yml b/.github/workflows/example.yml index 8d9a596..26b51ed 100644 --- a/.github/workflows/example.yml +++ b/.github/workflows/example.yml @@ -2,6 +2,9 @@ name: Example Usage on: [push, pull_request] +permissions: + contents: read + jobs: example: runs-on: ubuntu-latest diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index e9e2a03..8ac20f6 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -9,6 +9,9 @@ on: pull_request: workflow_dispatch: +permissions: + contents: read + jobs: test-linux: runs-on: ubuntu-latest From b7f43b06aa64416415659f75311d4264199e45af Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 14 Nov 2025 18:19:01 +0000 Subject: [PATCH 6/7] Initial plan From 8dcb628a5082470f17913d1394dc677d1a2384b7 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 14 Nov 2025 18:24:44 +0000 Subject: [PATCH 7/7] Address review comments from PR #1 Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com> --- .github/workflows/example.yml | 6 +-- .github/workflows/test.yml | 77 ++++++++--------------------------- README.md | 8 ++-- 3 files changed, 25 insertions(+), 66 deletions(-) diff --git a/.github/workflows/example.yml b/.github/workflows/example.yml index 26b51ed..b4c3cde 100644 --- a/.github/workflows/example.yml +++ b/.github/workflows/example.yml @@ -11,7 +11,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Setup Agda id: setup-agda @@ -31,8 +31,8 @@ jobs: cat > Example.agda << 'EOF' module Example where - open import Data.Bool - open import Data.Nat + open import Data.Bool.Base + open import Data.Nat.Base example : Bool example = true diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 8ac20f6..0f6d262 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -13,18 +13,30 @@ permissions: contents: read jobs: - test-linux: - runs-on: ubuntu-latest + test: + strategy: + matrix: + os: [ubuntu-latest, windows-latest, macos-latest, macos-13] + include: + - os: ubuntu-latest + agda-stdlib-version: '2.3' + - os: windows-latest + agda-stdlib-version: '' + - os: macos-latest + agda-stdlib-version: '2.3' + - os: macos-13 + agda-stdlib-version: '' + runs-on: ${{ matrix.os }} steps: - name: Checkout - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Setup Agda id: setup uses: ./ with: agda-version: '2.8.0' - agda-stdlib-version: '2.3' + agda-stdlib-version: ${{ matrix.agda-stdlib-version }} - name: Verify Agda installation run: | @@ -33,6 +45,7 @@ jobs: agda --version - name: Create test file + if: matrix.os == 'ubuntu-latest' run: | cat > test.agda << 'EOF' module test where @@ -42,59 +55,5 @@ jobs: EOF - name: Test Agda + if: matrix.os == 'ubuntu-latest' run: agda test.agda - - test-windows: - runs-on: windows-latest - steps: - - name: Checkout - uses: actions/checkout@v4 - - - name: Setup Agda - id: setup - uses: ./ - with: - agda-version: '2.8.0' - - - name: Verify Agda installation - run: | - echo "Agda path: ${{ steps.setup.outputs.agda-path }}" - echo "Agda dir: ${{ steps.setup.outputs.agda-dir }}" - agda --version - - test-macos: - runs-on: macos-latest - steps: - - name: Checkout - uses: actions/checkout@v4 - - - name: Setup Agda - id: setup - uses: ./ - with: - agda-version: '2.8.0' - agda-stdlib-version: '2.3' - - - name: Verify Agda installation - run: | - echo "Agda path: ${{ steps.setup.outputs.agda-path }}" - echo "Agda dir: ${{ steps.setup.outputs.agda-dir }}" - agda --version - - test-macos-intel: - runs-on: macos-13 # Intel-based macOS - steps: - - name: Checkout - uses: actions/checkout@v4 - - - name: Setup Agda - id: setup - uses: ./ - with: - agda-version: '2.8.0' - - - name: Verify Agda installation - run: | - echo "Agda path: ${{ steps.setup.outputs.agda-path }}" - echo "Agda dir: ${{ steps.setup.outputs.agda-dir }}" - agda --version diff --git a/README.md b/README.md index 80f7030..eb23b9d 100644 --- a/README.md +++ b/README.md @@ -4,13 +4,13 @@ GitHub composite action to install Agda from the official deployed binaries and ## Features -- Installs Agda from official GitHub releases -- Optional installation of the Agda standard library +- Installs Agda from official GitHub releases. +- Optional installation of the Agda standard library. - Cross-platform support: - Ubuntu (latest) - Windows (latest) - macOS (latest, including macOS-15-intel) -- Outputs the path to the Agda executable and Agda application directory +- Outputs the path to the Agda executable and Agda application directory. ## Usage @@ -76,7 +76,7 @@ jobs: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v5 - name: Setup Agda uses: agda/agda-setup-action@v1