Automic VaultAutomic Vault

brew

Install agda with Homebrew, apt, dnf, Nix, pacman

Dependently typed functional programming language. Version 2.8.0-r3 via Homebrew; verified 2026-06-22.

Install commandSecurity notes

install

Additional install commands

macOS

Homebrewverified · 100%
brew install agda

local Homebrew formula metadata

overview

Package summary

Dependently typed functional programming language

Commands and aliases

  • agda
  • agda-mode
  • agda2hs

history

Project history and usage

Agda is a dependently typed programming language and interactive theorem prover rooted in the Gothenburg tradition of Martin-Lof type theory systems. It is both a language-runtime package and a proof-assistant package, with an interactive editor workflow and a library system based on .agda-lib files.

Project history

The official history page traces the lineage back to proof assistants based on Martin-Lof type theory developed in Gothenburg since 1983, followed by intensional dependent type theory systems around 1990 such as ALF. In the mid-1990s, prototypes and redesigns explored theory mechanisms, proof editors, and type checking with metavariable constraints.

The original Agda, now often called Agda 1, was implemented in Haskell by Catarina Coquand. In 2004 the Programming Logic Group began collaborating with AIST in Japan, and the Agda Implementors Meetings started as biannual meetings alternating between Sweden and Japan.

Work on the current Agda system began after the 2005 AgdaLight prototype by Ulf Norell and Andreas Abel. Ulf Norell's 2007 thesis, 'Towards a practical programming language based on dependent type theory', is named by the official history page as a main reference for Agda 2.

Adoption history

Agda's adoption has grown through academic type theory, dependently typed programming, proof engineering, and formalized mathematics communities. The official wiki says the center of development is the Logic and Types group at Chalmers and Gothenburg University, while GitHub metadata shows a broad open-source contributor base.

As a package, Agda is visible across Haskell and OS package ecosystems. The README links Hackage and Stackage badges, the official installation docs describe binary releases, source builds with cabal and Nix, and a Python installer, and the supplied batch facts list Homebrew, Debian, Fedora, Nix, Arch, and Ubuntu.

How it is used

Users run agda to type-check files, use agda-mode or another editor integration for interactive development, and manage libraries through .agda-lib files plus AGDA_DIR/libraries and AGDA_DIR/defaults files. On Unix-like systems AGDA_DIR defaults to ~/.config/agda, with fallback behavior for ~/.agda; on Windows it defaults under AppData/Roaming/agda.

Agda code often depends on the standard library but the official installation page notes that the standard library is not necessarily bundled with every Agda distribution. The package-system documentation therefore matters to packagers and users because it defines how installed libraries become visible to the type checker.

Why package nerds care

Agda is one of those packages where the executable is only half the story: editor integration, Unicode input, library metadata, GHC compatibility, data files, standard-library versioning, and release notes all affect whether users can actually type-check projects.

The 2.8.0 release notes are especially package-relevant because they say Agda became a self-contained single binary and mention behavior around data files and library builds. That kind of upstream packaging change directly affects formulae, distro packages, and reproducible development environments.

Timeline

  • 1983: Gothenburg work on Martin-Lof type theory proof assistants begins.
  • 1990: ALF lineage of intensional dependent type theory systems begins around Gothenburg.
  • 2004: Agda collaboration with AIST begins and Agda Implementors Meetings start.
  • 2005: AgdaLight prototype work begins, leading toward Agda 2.
  • 2007: Ulf Norell thesis on a practical dependently typed programming language published.
  • 2025: Agda 2.8.0 released.

Related projects

  • ALF is the earlier Gothenburg logical framework named in the official history.
  • AgdaLight is the 2005 prototype named as a direct precursor to Agda 2.
  • The Agda standard library is a separately versioned library package used by many Agda projects.
  • Rocq, Epigram, Matita, and NuPRL are listed by the official wiki as related dependent-type proof assistants.

security posture

Risk level: yellow

generalized runtime or code generation signal.

Risk classifier

yellow risk · medium confidence · runtime

Why

  • generalized runtime or code generation signal

Signals

  • text:programming language

Install behavior

  • No Homebrew post-install hook is recorded in formula metadata.
  • Homebrew bottle metadata is available for 6 platform targets.
  • Installs with 3 runtime dependencies.
  • Build metadata lists 3 build dependencies.

Recommended review

Before unattended agent use, check whether the tool reads plaintext credentials, writes remote state, publishes artifacts, or shells out to plugins.

local files

Configuration and credential file locations

These source-backed paths show where this package keeps local settings or durable credentials. Automic Vault can use them as review targets for secret scanning, migration, and command approval.

Configuration files

Config paths the tool may read or write during local use.

Unix
.agda-lib~/.config/agda/libraries~/.config/agda/libraries-VERSION~/.config/agda/defaults~/.config/agda/defaults-VERSION~/.agda
Windows
.agda-libC:\Users\USERNAME\AppData\Roaming\agda\librariesC:\Users\USERNAME\AppData\Roaming\agda\libraries-VERSIONC:\Users\USERNAME\AppData\Roaming\agda\defaultsC:\Users\USERNAME\AppData\Roaming\agda\defaults-VERSION

executables

Installed executables

CommandKindExposureNote
agdacliglobal executable
agda-modecliglobal executable
agda2hscliglobal executable

freshness

Version and freshness

These signals separate page generation age, package-manager activity, and upstream release comparison. Version lag is warned only when an evidence URL and comparable versions are present.

page generated2026-07-08
manager version2.8.0-r3
manager updated2026-06-22
local dataok
upstreamcurrent
latest detectedv2.8.0-r3

https://github.com/agda/agda

  • okNo freshness warnings were generated.

install metadata

Package metadata

Package keybrew:agda
Version2.8.0-r3
Package managerHomebrew
Package manager pagehttps://formulae.brew.sh/formula/agda
Homepagehttps://wiki.portal.chalmers.se/agda/
Repositoryhttps://github.com/agda/agda
Upstream docshttps://agda.readthedocs.io/en/latest
LicenseMIT AND BSD-3-Clause
Source archivehttps://github.com/agda/agda/archive/refs/tags/v2.8.0-r3.tar.gz
Last updated2026-06-22T14:02:41-07:00
Pulseupdated
Dependenciesghc@9.12, gmp, icu4c@78
Build dependenciescabal-install, emacs, pkgconf
Uses from macOSlibffi, ncurses
Bottleavailable (on arm64_linux, arm64_sequoia, arm64_sonoma, arm64_tahoe, sonoma, x86_64_linux)
Homebrew post-installnot defined
Servicenone declared
CaveatsTo use the installed Agda libraries, execute the following commands: mkdir -p $HOME/.config/agda cp $HOMEBREW_PREFIX/opt/agda/share/agda/example-libraries $HOME/.config/agda/libraries cp $HOMEBREW_PREFIX/opt/agda/share/agda/example-defaults $HOME/.config/agda/defaults You can then inspect the copied files and customize them as needed. If you have upgraded your Agda installation from a previous version, you may need to redo this.

registry facts

Source database details

Source DatabaseHomebrew formula API
Taphomebrew/core
Full Nameagda
Version Scheme0
Revision0
Head VersionHEAD
Bottle Stable Root URLhttps://ghcr.io/v2/homebrew/core
Deprecatedno
Disabledno
Keg Onlyno
URL Keys
  • head
  • stable

source database matches

Other package-manager records

Matches are pulled from external package-manager indexes and kept separate from local Automic Vault package links.

Debian apt95%

agda 2.6.4.3-1

dependently typed functional programming language

https://wiki.portal.chalmers.se/agda/

sudo apt install agda
  • Section: misc
  • Architecture: all
  • 5 dependencies
  • normalized package name match
  • Matched by: Agda
Debian stable package indexes · deb.debian.org · Debian stable package indexes: agda from https://deb.debian.org/debian/dists/stable/main/binary-amd64/Packages.xz
Debian apt95%

agda-bin 2.6.4.3-1+b2

commandline interface to Agda

https://wiki.portal.chalmers.se/agda/

sudo apt install agda-bin
  • Section: haskell
  • Architecture: amd64
  • Source Package: agda
  • 7 dependencies
  • 1 optional deps
  • normalized package name match
  • Matched by: Agda
Debian stable package indexes · deb.debian.org · Debian stable package indexes: agda-bin from https://deb.debian.org/debian/dists/stable/main/binary-amd64/Packages.xz
Debian apt95%

elpa-agda2-mode 2.6.4.3-1

dependently typed functional programming language — emacs mode

https://wiki.portal.chalmers.se/agda/

sudo apt install elpa-agda2-mode
  • Section: editors
  • Architecture: all
  • Source Package: agda
  • 4 dependencies
  • 1 optional deps
  • normalized package name match
  • Matched by: Agda
Debian stable package indexes · deb.debian.org · Debian stable package indexes: elpa-agda2-mode from https://deb.debian.org/debian/dists/stable/main/binary-amd64/Packages.xz
Debian apt95%

libghc-agda-dev 2.6.4.3-1+b2

dependently typed functional programming language

https://wiki.portal.chalmers.se/agda/

sudo apt install libghc-agda-dev
  • Section: haskell
  • Architecture: amd64
  • Source Package: agda
  • 32 dependencies
  • 1 provides
  • normalized package name match
  • Matched by: Agda
Debian stable package indexes · deb.debian.org · Debian stable package indexes: libghc-agda-dev from https://deb.debian.org/debian/dists/stable/main/binary-amd64/Packages.xz
Debian apt95%

libghc-agda-doc 2.6.4.3-1

dependently typed functional programming language; documentation

https://wiki.portal.chalmers.se/agda/

sudo apt install libghc-agda-doc
  • Section: doc
  • Architecture: all
  • Source Package: agda
  • 1 dependencies
  • 1 provides
  • 29 optional deps
  • normalized package name match
  • Matched by: Agda
Debian stable package indexes · deb.debian.org · Debian stable package indexes: libghc-agda-doc from https://deb.debian.org/debian/dists/stable/main/binary-amd64/Packages.xz
Nix95%

agda

nix profile install nixpkgs#agda
  • normalized package name match
  • Matched by: Agda
nixpkgs package indexes · raw.githubusercontent.com · nixpkgs package indexes: agda from https://raw.githubusercontent.com/NixOS/nixpkgs/master/pkgs/top-level/all-packages.nix
Ubuntu apt95%

agda 2.6.3-1build1

dependently typed functional programming language

https://wiki.portal.chalmers.se/agda/

sudo apt install agda
  • Section: universe/misc
  • Architecture: all
  • 5 dependencies
  • normalized package name match
  • Matched by: Agda
Ubuntu 24.04 LTS package indexes · archive.ubuntu.com · Ubuntu 24.04 LTS package indexes: agda from https://archive.ubuntu.com/ubuntu/dists/noble/universe/binary-amd64/Packages.gz
Ubuntu apt95%

agda-bin 2.6.3-1build1

commandline interface to Agda

https://wiki.portal.chalmers.se/agda/

sudo apt install agda-bin
  • Section: universe/haskell
  • Architecture: amd64
  • Source Package: agda
  • 6 dependencies
  • 1 optional deps
  • normalized package name match
  • Matched by: Agda
Ubuntu 24.04 LTS package indexes · archive.ubuntu.com · Ubuntu 24.04 LTS package indexes: agda-bin from https://archive.ubuntu.com/ubuntu/dists/noble/universe/binary-amd64/Packages.gz
Ubuntu apt95%

elpa-agda2-mode 2.6.3-1build1

dependently typed functional programming language — emacs mode

https://wiki.portal.chalmers.se/agda/

sudo apt install elpa-agda2-mode
  • Section: universe/editors
  • Architecture: all
  • Source Package: agda
  • 4 dependencies
  • 1 optional deps
  • normalized package name match
  • Matched by: Agda
Ubuntu 24.04 LTS package indexes · archive.ubuntu.com · Ubuntu 24.04 LTS package indexes: elpa-agda2-mode from https://archive.ubuntu.com/ubuntu/dists/noble/universe/binary-amd64/Packages.gz
Ubuntu apt95%

libghc-agda-dev 2.6.3-1build1

dependently typed functional programming language

https://wiki.portal.chalmers.se/agda/

sudo apt install libghc-agda-dev
  • Section: universe/haskell
  • Architecture: amd64
  • Source Package: agda
  • 32 dependencies
  • 1 provides
  • normalized package name match
  • Matched by: Agda
Ubuntu 24.04 LTS package indexes · archive.ubuntu.com · Ubuntu 24.04 LTS package indexes: libghc-agda-dev from https://archive.ubuntu.com/ubuntu/dists/noble/universe/binary-amd64/Packages.gz
Ubuntu apt95%

libghc-agda-doc 2.6.3-1build1

dependently typed functional programming language; documentation

https://wiki.portal.chalmers.se/agda/

sudo apt install libghc-agda-doc
  • Section: universe/doc
  • Architecture: all
  • Source Package: agda
  • 1 dependencies
  • 1 provides
  • 27 optional deps
  • normalized package name match
  • Matched by: Agda
Ubuntu 24.04 LTS package indexes · archive.ubuntu.com · Ubuntu 24.04 LTS package indexes: libghc-agda-doc from https://archive.ubuntu.com/ubuntu/dists/noble/universe/binary-amd64/Packages.gz
dnf95%

Agda 2.8.0-59.fc44

A dependently typed functional programming language and proof assistant

https://hackage.haskell.org/package/Agda

sudo dnf install Agda
  • License: MIT AND BSD-3-Clause
  • Category: Unspecified
  • Architecture: x86_64
  • Source Package: Agda
  • 9 dependencies
  • 3 provides
  • normalized package name match
  • Matched by: Agda
Fedora Rawhide package metadata · dl.fedoraproject.org · Fedora Rawhide package metadata: Agda from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst
dnf95%

Agda-common 2.8.0-59.fc44

Agda common files

https://hackage.haskell.org/package/Agda

sudo dnf install Agda-common
  • License: MIT AND BSD-3-Clause AND BSD-2-Clause
  • Category: Unspecified
  • Architecture: noarch
  • Source Package: Agda
  • 1 provides
  • normalized package name match
  • Matched by: Agda
Fedora Rawhide package metadata · dl.fedoraproject.org · Fedora Rawhide package metadata: Agda-common from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst
dnf95%

ghc-Agda 2.8.0-59.fc44

Haskell Agda library

https://hackage.haskell.org/package/Agda

sudo dnf install ghc-Agda
  • License: MIT AND BSD-3-Clause
  • Category: Unspecified
  • Architecture: x86_64
  • Source Package: Agda
  • 32 dependencies
  • 2 provides
  • normalized package name match
  • Matched by: Agda
Fedora Rawhide package metadata · dl.fedoraproject.org · Fedora Rawhide package metadata: ghc-Agda from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst
dnf95%

ghc-Agda-devel 2.8.0-59.fc44

Haskell Agda library development files

https://hackage.haskell.org/package/Agda

sudo dnf install ghc-Agda-devel
  • License: MIT AND BSD-3-Clause
  • Category: Unspecified
  • Architecture: x86_64
  • Source Package: Agda
  • 3 dependencies
  • 3 provides
  • normalized package name match
  • Matched by: Agda
Fedora Rawhide package metadata · dl.fedoraproject.org · Fedora Rawhide package metadata: ghc-Agda-devel from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst
dnf95%

ghc-Agda-doc 2.8.0-59.fc44

Haskell Agda library documentation

https://hackage.haskell.org/package/Agda

sudo dnf install ghc-Agda-doc
  • License: MIT AND BSD-3-Clause
  • Category: Unspecified
  • Architecture: noarch
  • Source Package: Agda
  • 1 dependencies
  • 1 provides
  • normalized package name match
  • Matched by: Agda
Fedora Rawhide package metadata · dl.fedoraproject.org · Fedora Rawhide package metadata: ghc-Agda-doc from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst

package graph

Links come from deterministic package relationships, av.db category and tag curation, ecosystem matches, and package hub membership.

Related tools

  • ghc@9.12Runtime dependency declared by Homebrew.
  • cabal-installBuild dependency declared by Homebrew.
  • emacsBuild dependency declared by Homebrew.
  • pkgconfBuild dependency declared by Homebrew.

Same workflow

  • idris2Shares av.db curated category or tags: cli, dependent-types, functional-programming, language-runtime, programming-language.
  • ats2-postiatsShares av.db curated category or tags: cli, dependent-types, language-runtime, programming-language.
  • coconutShares av.db curated category or tags: cli, functional-programming, language-runtime, programming-language.
  • elixirShares av.db curated category or tags: cli, functional-programming, language-runtime, programming-language.
  • elmShares av.db curated category or tags: cli, functional-programming, language-runtime, programming-language.
  • flixShares av.db curated category or tags: cli, functional-programming, language-runtime, programming-language.

source trail

Generated from repository data

This page is generated by av-web from the private package SQLite artifact built by scripts/generate-pkg-sqlite.py.

Used sources

  • Geiger risk classifier
  • Nucleus package database
  • av.db category and tag curation
  • cross-ecosystem install command graph
  • curated configuration and credential file locations
  • curated package history
  • external package-manager database matches
  • package relationship graph
  • package version freshness
  • package-page enrichment