Summary
Agda is an interactive proof editor, or proof assistant. Its input language, called Agda language (or simply Agda), is based on a constructive type theory á la Martin-Löf, extended with dependent record types, inductive definitions, module structures and a class hierarchy mechanism.
Versions
v2.5.2-r2 :: 0/2.5.2 :: gentoo
- Modified
- License
- MIT
- Keywords
- ~amd64 ~x86
- USE flags
- cpphs debug doc emacs hscolour profile stdlib uhc
v2.5.2-r1 :: 0/2.5.2 :: gentoo
- Modified
- License
- MIT
- Keywords
- ~amd64 ~x86
- USE flags
- cpphs debug doc emacs hscolour profile stdlib uhc
v2.4.2.5-r2 :: 0/2.4.2.5 :: gentoo
- Modified
- License
- MIT
- Keywords
- ~amd64 ~x86
- USE flags
- cpphs doc emacs hscolour profile stdlib
USE flags
General
- cpphs
- Use cpphs instead of cpp.
- debug
- Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see https://wiki.gentoo.org/wiki/Project:Quality_Assurance/Backtraces
- doc
- Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally
- emacs
- Add support for GNU Emacs
- hscolour
- Include coloured haskell sources to generated documentation (dev-haskell/hscolour)
- profile
- Add support for software performance analysis (will likely vary from ebuild to ebuild)
- stdlib
- Install the standard library.
- uhc
- Add support for the uhc backend.
Dependencies
app-editors / emacs : The extensible, customizable, self-documenting real-time display editor
app-emacs / haskell-mode : Mode for editing (and running) Haskell programs in Emacs
dev-haskell / alex : Alex is a tool for generating lexical analysers in Haskell
dev-haskell / binary : Binary serialisation for Haskell values using lazy ByteStrings
dev-haskell / boxes : 2D text pretty-printing library
dev-haskell / cabal : A framework for packaging Haskell software
dev-haskell / cpphs : A liberalised re-implementation of cpp, the C pre-processor
dev-haskell / data-hash : Combinators for building fast hashing functions
dev-haskell / edisoncore : A library of efficent, purely-functional data structures (Core Implementations)
dev-haskell / edit-distance : Levenshtein and restricted Damerau-Levenshtein edit distances
dev-haskell / equivalence : Maintaining an equivalence relation implemented as union-find using STT
dev-haskell / fail : Forward-compatible MonadFail class
dev-haskell / geniplate-mirror : Use Template Haskell to generate Uniplate-like functions
dev-haskell / gitrev : Compile git revision info into Haskell projects
dev-haskell / haddock : A documentation-generation tool for Haskell libraries
dev-haskell / happy : Happy is a parser generator for Haskell
dev-haskell / hashable : A class for types that can be converted to a hash value
dev-haskell / hashtables : Mutable hash tables in the ST monad
dev-haskell / haskeline : A command-line interface for user input, written in Haskell
dev-haskell / haskell-src-exts : Manipulating Haskell source: abstract syntax, lexer, parser, and pretty-printer
dev-haskell / hscolour : Colourise Haskell code
dev-haskell / ieee754 : Utilities for dealing with IEEE floating point numbers
dev-haskell / monadplus : Haskell98 partial maps and filters over MonadPlus
dev-haskell / mtl : Monad classes, using functional dependencies
dev-haskell / murmur-hash : MurmurHash2 implementation for Haskell
dev-haskell / parallel : Parallel programming library
dev-haskell / quickcheck : Automatic testing of Haskell programs
dev-haskell / regex-tdfa : Replaces/Enhances Text.Regex
dev-haskell / semigroups : Anything that associates
dev-haskell / shuffle : Shuffle tool for UHC
dev-haskell / strict : Strict data types and String IO
dev-haskell / text : An efficient packed Unicode text type
dev-haskell / transformers : Concrete functor and monad transformers
dev-haskell / transformers-compat : A small compatibility shim for dev-haskell/transformers
dev-haskell / uhc-light : Part of UHC packaged as cabal/hackage installable library
dev-haskell / uhc-util : UHC utilities
dev-haskell / unordered-containers : Efficient hashing-based container types
dev-haskell / uulib : Haskell Utrecht Tools Library
dev-haskell / void : A Haskell 98 logically uninhabited data type
dev-haskell / xhtml : An XHTML combinator library
dev-haskell / zlib : Compression and decompression in the gzip and zlib formats
Runtime Dependencies
app-editors / emacs : The extensible, customizable, self-documenting real-time display editor
app-emacs / haskell-mode : Mode for editing (and running) Haskell programs in Emacs
dev-haskell / binary : Binary serialisation for Haskell values using lazy ByteStrings
dev-haskell / boxes : 2D text pretty-printing library
dev-haskell / data-hash : Combinators for building fast hashing functions
dev-haskell / edisoncore : A library of efficent, purely-functional data structures (Core Implementations)
dev-haskell / edit-distance : Levenshtein and restricted Damerau-Levenshtein edit distances
dev-haskell / equivalence : Maintaining an equivalence relation implemented as union-find using STT
dev-haskell / fail : Forward-compatible MonadFail class
dev-haskell / geniplate-mirror : Use Template Haskell to generate Uniplate-like functions
dev-haskell / gitrev : Compile git revision info into Haskell projects
dev-haskell / hashable : A class for types that can be converted to a hash value
dev-haskell / hashtables : Mutable hash tables in the ST monad
dev-haskell / haskeline : A command-line interface for user input, written in Haskell
dev-haskell / haskell-src-exts : Manipulating Haskell source: abstract syntax, lexer, parser, and pretty-printer
dev-haskell / ieee754 : Utilities for dealing with IEEE floating point numbers
dev-haskell / monadplus : Haskell98 partial maps and filters over MonadPlus
dev-haskell / mtl : Monad classes, using functional dependencies
dev-haskell / murmur-hash : MurmurHash2 implementation for Haskell
dev-haskell / parallel : Parallel programming library
dev-haskell / quickcheck : Automatic testing of Haskell programs
dev-haskell / regex-tdfa : Replaces/Enhances Text.Regex
dev-haskell / semigroups : Anything that associates
dev-haskell / shuffle : Shuffle tool for UHC
dev-haskell / strict : Strict data types and String IO
dev-haskell / text : An efficient packed Unicode text type
dev-haskell / transformers : Concrete functor and monad transformers
dev-haskell / transformers-compat : A small compatibility shim for dev-haskell/transformers
dev-haskell / uhc-light : Part of UHC packaged as cabal/hackage installable library
dev-haskell / uhc-util : UHC utilities
dev-haskell / unordered-containers : Efficient hashing-based container types
dev-haskell / uulib : Haskell Utrecht Tools Library
dev-haskell / void : A Haskell 98 logically uninhabited data type
dev-haskell / xhtml : An XHTML combinator library
dev-haskell / zlib : Compression and decompression in the gzip and zlib formats
Depending packages
sci-mathematics / agda-stdlib : Agda standard library
Bugs
- 279085
- sci-mathematics/agda fails tests
- 540230
- sci-mathematics/agda-2.4.2.2-r1 - Preprocessing library Agda-2.4.2.2... cpphs: src/full/Agda/Interaction/BasicOps.hs: hGetContents: invalid argument (invalid byte sequence)
- 634944
- sci-mathematics/agda-2.5.2-r1 : * setup configure failed
- 703816
- sci-mathematics/agda-2.6.0.1 version bump
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Sergei Trofimovich · gentoo
sci-mathematics/agda: allow multiple revisions of agda-stdlib
Package-Manager: Portage-2.3.83, Repoman-2.3.20 Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sergei Trofimovich · gentoo
sci-mathematics/agda: allow edisoncore-1.3.2
Reported-by: Toralf Förster Closes: https://bugs.gentoo.org/703418 Package-Manager: Portage-2.3.82, Repoman-2.3.20 Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Ulrich Müller · gentoo
sci-mathematics/agda: Update virtual/emacs dependency.
The virtual is deprecated, depend on app-editors/emacs instead. Package-Manager: Portage-2.3.82, Repoman-2.3.20 Signed-off-by: Ulrich Müller <ulm@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Michał Górny · gentoo
*/*: Inline mirror://hackage and update URIs
This change inlines mirror://hackage in all ebuilds, and updates URIs to the modern form (old URIs redirect to that). The change has been made using the following command: find -name '*.ebuild' -exec sed -r -i \ -e 's@mirror://hackage/@https://hackage.haskell.org/@g' \ -e 's@https://hackage.haskell.org/packages/archive/([^/]*)/([^/]*)/@https://hackage.haskell.org/package/\1-\2/@g' \ -e '/hackage\.haskell\.org/s@\$\{PN}-\$\{PV}@${P}@g' \ -e '/hackage\.haskell\.org/s@\$\{MY_PN}-\$\{PV}@${MY_P}@g' \ -e '/hackage\.haskell\.org/s@\$\{PN}-\$\{MY_PV}@${MY_P}@g' \ {} + Signed-off-by: Michał Górny <mgorny@gentoo.org> - Robin H. Johnson · gentoo
Drop $Id$ per council decision in bug #611234.
Signed-off-by: Robin H. Johnson <robbat2@gentoo.org> - Sergei Trofimovich · gentoo
sci-mathematics/agda: bump up to 2.5.2
Package-Manager: Portage-2.3.3, Repoman-2.3.1 - T. Malfatti · gentoo
media-libs/portaudio: Version bump - Sergei Trofimovich · gentoo
sci-mathematics/agda: allow alex-3.2, bug #600034
Reported-by: Anton Kochkov Bug: https://bugs.gentoo.org/600034 Package-Manager: portage-2.3.2 - Sergei Trofimovich · gentoo
sci-mathematics/agda: allow cpphs-1.20
Package-Manager: portage-2.3.0 - Sergei Trofimovich · gentoo
sci-mathematics/agda: drop old
Package-Manager: portage-2.2.28 - Sergei Trofimovich · gentoo
sci-mathematics/agda: allow transformers-compat-0.4
Package-Manager: portage-2.2.28 - Sergei Trofimovich · gentoo
sci-mathematics/agda: drop old
Package-Manager: portage-2.2.28 - Sergei Trofimovich · gentoo
sci-mathematics/agda: fix hastables build failure, bu #574204
While at it made USE=emacs depend and files optional, fixed agda library reregistration. Reported-by: Toralf Förster Bug: https://bugs.gentoo.org/show_bug.cgi?id=574204 Package-Manager: portage-2.2.27 - Jauhien Piatlicki · gentoo
sci-mathematics/{agda,agda-stdlib}: version bump
Gentoo-Bug: 561772 Package-Manager: portage-2.2.26 - Patrice Clement · gentoo
Merge remote-tracking branch 'github/pr/644'. - Jauhien Piatlicki · gentoo
sci-mathematics/agda: fix dev-haskell/cpphs dependency
Package-Manager: portage-2.2.26 - Sergei Trofimovich · gentoo
sci-mathematics/agda: fix .agdai file generation on install, bug #559326
As we build dynamically linked binaries now we need to add LD_LIBRARY_PATH to temporary llibrary localtions to generate .agdai files. Reported-by: Toralf Förster Bug: https://bugs.gentoo.org/559326 Package-Manager: portage-2.2.22 - Robin H. Johnson · gentoo
proj/gentoo: Initial commit
This commit represents a new era for Gentoo: Storing the gentoo-x86 tree in Git, as converted from CVS. This commit is the start of the NEW history. Any historical data is intended to be grafted onto this point. Creation process: 1. Take final CVS checkout snapshot 2. Remove ALL ChangeLog* files 3. Transform all Manifests to thin 4. Remove empty Manifests 5. Convert all stale $Header$/$Id$ CVS keywords to non-expanded Git $Id$ 5.1. Do not touch files with -kb/-ko keyword flags. Signed-off-by: Robin H. Johnson <robbat2@gentoo.org> X-Thanks: Alec Warner <antarus@gentoo.org> - did the GSoC 2006 migration tests X-Thanks: Robin H. Johnson <robbat2@gentoo.org> - infra guy, herding this project X-Thanks: Nguyen Thai Ngoc Duy <pclouds@gentoo.org> - Former Gentoo developer, wrote Git features for the migration X-Thanks: Brian Harring <ferringb@gentoo.org> - wrote much python to improve cvs2svn X-Thanks: Rich Freeman <rich0@gentoo.org> - validation scripts X-Thanks: Patrick Lauer <patrick@gentoo.org> - Gentoo dev, running new 2014 work in migration X-Thanks: Michał Górny <mgorny@gentoo.org> - scripts, QA, nagging X-Thanks: All of other Gentoo developers - many ideas and lots of paint on the bikeshed