[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

RFS: agda

Hello everyone [agda list, Nisse asked me to CC you in, but this message is just informational for you guys],

I'm seeking a review/sponsor for my NEW package, Agda. In case you don't know what it is, here's a paste from the long description which was in turn stolen from the cabal package description.

 Agda is a dependently typed functional programming language: It has inductive
 families, which are like 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.

The package is built using haskell-devscripts and is lintian clean (as far as it can be; upstream doesn't ship changelogs), and builds/installs/runs well as far as I can tell.

It's packaged in git on collab-maint (sorry for not using darcs...), and you can get it by:

 git clone git://git.debian.org/collab-maint/agda.git


 git clone http://git.debian.org/git/collab-maint/agda.git

and you can view it on the web at:


Co-maintainers are more than welcome. Just make any changes you want (you'll need to be a member of collab-maint on Alioth). I'm Laney on #debian-haskell (OFTC) if you want to get me there.

I'd appreciate a review and comments, and sponsorship once it's ready...


Attachment: signature.asc
Description: OpenPGP digital signature

Reply to: