A functional programming language and proof assistant Maintained by:haskell@FreeBSD.org Port Added: 04 Jan 2010 03:26:01 Also Listed In:haskell License: not specified in port
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-Lof. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
WWW: http://wiki.portal.chalmers.se/agda/
To install the port:cd /usr/ports/math/hs-Agda/ && make install clean To add the package:pkg_add -r hs-Agda
Configuration Options
===> The following configuration options are available for hs-Agda-2.3.0:
USE_LOCALE=off (default) "Use encoding specified by the locale"
EPIC=off (default) "Install the Epic compiler"
===> Use 'make config' to modify these settings
Reason:
GHC has been updated to version 7.0.4, and Haskell Platform to version
2011.4.0.0, and other Haskell ports are also updated to their Haskell
Platform versions or latest versions.
To update all affected ports:
# portmaster -r lang/ghc
or
# portupgrade -r lang/ghc
2011-05-09
Affects: users of lang/ghc and */hs-*
Author: ashish@FreeBSD.org
Reason:
GHC has been updated to version 7.0.3 and other Haskell ports are also
updated to their Haskell Platform versions or latest versions.
To update all affected ports:
# portmaster -r lang/ghc
or
# portupgrade -r lang/ghc
Number of commits found: 10
Commit History - (may be incomplete: see CVSWeb link above for full details)
Bump PORTREVISION of all ports dependent on lang/ghc as during
upgrade, lang/ghc cabal package cache gets invalidated causing all
dependent ports to be reinstalled.
Obtained from: FreeBSD Haskell
- Please welcome GHC 7.0.3
GHC in the ports tree has been updated to 7.0.3 and all other Haskell ports
are also updated to their corresponding Haskell Platform versions, or latest
versions.
We would like to acknowledge the support of the FreeBSD Donations Team and
Eotvos Lorand University, Faculty of Informatics who contributed to the server
that we used for testing.
We would also like to thank all the testers who tested FreeBSD Haskell ports
and provided their feedback.
PR: ports/156642
Approved by: tabthorpe (mentor)
Obtained from: FreeBSD Haskell
Introduce a new (and hopefully better) ports infrastructure for Haskell Cabal
ports which makes possible the direct translation of Cabal package
descriptions to FreeBSD ports. It promises both easier addition and
maintenance for Cabal-based ports.
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-Lof. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
WWW: http://wiki.portal.chalmers.se/agda/
PR: ports/142141
Submitted by: Jacula Modyun <jacula(at)gmail.com>