Summary
Agda is a dependently typed functional programming language: It has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code). Agda is also a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. This package includes both a command-line program (agda) and an Emacs mode. If you want to use the Emacs mode you can set it up by running @agda-mode setup@ (see the README). Note that the Agda package does not follow the package versioning policy, because it is not intended to be used by third-party packages.
Versions
v2.6.1.2 :: 0/2.6.1.2 :: gentoo
- Modified
- License
- MIT
- Keywords
- ~amd64 ~x86
- USE flags
- cpphs debug doc emacs enable-cluster-counting hscolour profile stdlib
USE flags
General
- cpphs
- Use cpphs instead of cpp.
- debug
- Enable debugging features that may slow Agda down.
- doc
- Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally
- emacs
- Add support for GNU Emacs
- enable-cluster-counting
- Enable the --count-clusters flag. (If enable-cluster-counting is False, then the --count-clusters flag triggers an error message.)
- 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.
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 / aeson : Fast JSON parsing and encoding
dev-haskell / alex : Alex is a tool for generating lexical analysers in Haskell
dev-haskell / async : Run IO operations asynchronously and wait for their results
dev-haskell / blaze-html : A blazingly fast HTML combinator library for Haskell
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 / edit-distance : Levenshtein and restricted Damerau-Levenshtein edit distances
dev-haskell / equivalence : Maintaining an equivalence relation implemented as union-find using STT
dev-haskell / exceptions : Extensible optionally-pure exceptions
dev-haskell / geniplate-mirror : Use Template Haskell to generate Uniplate-like functions
dev-haskell / gitrev : Compile git revision info into Haskell projects
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 / hscolour : Colourise Haskell code
dev-haskell / ieee754 : Utilities for dealing with IEEE floating point numbers
dev-haskell / mtl : Monad classes, using functional dependencies
dev-haskell / murmur-hash : MurmurHash2 implementation for Haskell
dev-haskell / regex-tdfa : Replaces/Enhances Text.Regex
dev-haskell / split : Combinator library for splitting lists
dev-haskell / stm : Software Transactional Memory
dev-haskell / strict : Strict data types and String IO
dev-haskell / text : An efficient packed Unicode text type
dev-haskell / text-icu : Bindings to the ICU library
dev-haskell / unordered-containers : Efficient hashing-based container types
dev-haskell / uri-encode : Unicode aware uri-encoding
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 / aeson : Fast JSON parsing and encoding
dev-haskell / async : Run IO operations asynchronously and wait for their results
dev-haskell / blaze-html : A blazingly fast HTML combinator library for Haskell
dev-haskell / boxes : 2D text pretty-printing library
dev-haskell / data-hash : Combinators for building fast hashing functions
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 / exceptions : Extensible optionally-pure exceptions
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 / ieee754 : Utilities for dealing with IEEE floating point numbers
dev-haskell / mtl : Monad classes, using functional dependencies
dev-haskell / murmur-hash : MurmurHash2 implementation for Haskell
dev-haskell / regex-tdfa : Replaces/Enhances Text.Regex
dev-haskell / split : Combinator library for splitting lists
dev-haskell / stm : Software Transactional Memory
dev-haskell / strict : Strict data types and String IO
dev-haskell / text : An efficient packed Unicode text type
dev-haskell / text-icu : Bindings to the ICU library
dev-haskell / unordered-containers : Efficient hashing-based container types
dev-haskell / uri-encode : Unicode aware uri-encoding
dev-haskell / zlib : Compression and decompression in the gzip and zlib formats
Depending packages
sci-mathematics / agda-stdlib : Agda standard library
Bugs
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Sergei Trofimovich · gentoo
sci-mathematics/agda: allow ghc-8.10.4
Package-Manager: Portage-3.0.17, Repoman-3.0.2 Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sergei Trofimovich · gentoo
sci-mathematics/agda: set USE=-cpphs by default
USE=cpphs is not compatible to profiling builds. Reported-by: Toralf Förster Closes: https://bugs.gentoo.org/761805 Package-Manager: Portage-3.0.12, Repoman-3.0.2 Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Jack Todaro · gentoo
sci-mathematics/agda: drop old
Package-Manager: Portage-3.0.12, Repoman-3.0.2 Signed-off-by: Jack Todaro <solpeth@posteo.org> Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org> - Jack Todaro · gentoo
sci-mathematics/agda: bump up to 2.6.1.2
Signed-off-by: Jack Todaro <solpeth@posteo.org> Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sergei Trofimovich · gentoo
sci-mathematics/agda: drop USE=uhc
uhc is masked for removal. Package-Manager: Portage-3.0.9, Repoman-3.0.2 Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sergei Trofimovich · gentoo
sci-mathematics/agda: drop old
Package-Manager: Portage-3.0.8, Repoman-3.0.1 Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alexey Sokolov · gentoo
sci-mathematics/agda: update homepage
Package-Manager: Portage-2.3.99, Repoman-2.3.22 Signed-off-by: Alexey Sokolov <sokolov@google.com> Signed-off-by: Aaron Bauman <bman@gentoo.org> - 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