Agda Files

Agda is a dependently typed programming language

This is an exact mirror of the Agda project, hosted at https://github.com/agda/agda. SourceForge is not affiliated with Agda.

The interactive file manager requires Javascript. Please enable it or use sftp or scp.
You may still browse the files here.

Name	Modified	Size	InfoDownloads / Week
Parent folder
Agda-v2.8.0.1-linux.tar.xz	2026-08-31	8.5 MB	1
Agda-v2.8.0.1-macOS-arm64.tar.xz	2026-08-31	15.9 MB	0
Agda-v2.8.0.1-macOS-x64.tar.xz	2026-08-31	7.5 MB	0
Agda-v2.8.0.1-win64.zip	2026-08-31	20.9 MB	14
README.md	2026-08-31	163 Bytes	0
v2.8.0.1 source code.tar.gz	2026-08-31	5.0 MB	0
v2.8.0.1 source code.zip	2026-08-31	7.9 MB	0
Totals: 7 Items		65.6 MB	15

Release notes for Agda version 2.8.0.1

Added support for GHC 9.14.1
Agda supports GHC versions 8.8.4 to 9.14.1.

Source: README.md, updated 2026-08-31

Other Useful Business Software

$300 Free Credits to Build on Google Cloud

New customers can spin up VMs, build with AI, and query data at no cost.

Put your $300 in credit toward real workloads, then keep building with free monthly usage for 20+ products. No commitment and no charge until you upgrade.

Start Free

Go from Code to Production URL in Seconds

Cloud Run deploys apps in any language instantly. Scales to zero. Pay only when code runs.

Skip the Kubernetes configs. Cloud Run handles HTTPS, scaling, and infrastructure automatically. Two million requests free per month.

Start Free

$300 Free Credits to Build on Google Cloud

New customers can spin up VMs, build with AI, and query data at no cost.

Put your $300 in credit toward real workloads, then keep building with free monthly usage for 20+ products. No commitment and no charge until you upgrade.

Start Free

Recommended Projects

SASyLF
SASyLF is an proof assistant for reasoning about programs.
DeepSeekMath-V2
Towards self-verifiable mathematical reasoning
Metal and Money
Metal and Money is a puzzle game involving acquiring items, meeting people, using their services. Its design goal was this: Playing M&M mirrors the activity of doing proofs in intuitionistic propositional logic. (Isn't that fascinating!?)
Archive of Formal Proofs
A collection of machine-checkend mathematical proofs
Obelisk
Functional reactive web and mobile applications, with batteries

Agda Files

Agda is a dependently typed programming language

Get an email when there's a new version of Agda

Release notes for Agda version 2.8.0.1