Needs to be updated to Agda 2.3

Ok finally:

Spec: http://petersen.fedorapeople.org/reviews/Agda/Agda.spec
SRPM: http://petersen.fedorapeople.org/reviews/Agda/Agda-2.3.0.1-1.fc17.src.rpm

Koji: http://koji.fedoraproject.org/koji/taskinfo?taskID=4229387

Builds for me in F17 too locally.

I need to check if it needs "Requires: ghc-Agda-devel" too.

Even though the hackage page doesn't mention it, the Agda stdlib are required for Agda-executable:

  http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary

These need to be made available for use with the command line tool. For example, in the following example the IO module is provided by the Agda stdlib:

=== TEST CODE ===

open import IO

main : _
main = run (putStrLn "Hello world!")

=== END ===

Gentoo (for example) has an ebuild for the same:

http://sources.gentoo.org/cgi-bin/viewvc.cgi/gentoo-x86/sci-mathematics/agda-stdlib/

Yeah it would be good to add the stdlib too.
I have a draft package of it though Agda doesn't have proper
packaging conventions yet.

Actually Agda is needed to compile stdlib (at least to generate
the interface files) so I think this package will still
come before Agda-stdlib even if it is not very useful without it.

Also I verified that Agda doesn't seem to need ghc-Agda-devel:
it is dynamically linked to ghc-Agda anyway.

I think the example above does not compile with Agda-2.3?
but the example from http://strugglingthroughproblems.blogspot.in/2012/03/agda-as-programming-language-hello.html you found might with stdlib-0.6.

A small example of usage:

$ cat test.agda
module test where

data Bool : Set where
  true : Bool
  false : Bool
$ agda test.agda
Checking test (/home/petersen/pkgreview/Agda/test/test.agda).
Finished test.
$

I see Debian has an "agda" meta-package that pulls in Agda-executable,
Agda and the stdlib.

Package Review
==============

Key:
- = N/A
x = Pass
! = Fail
? = Not evaluated

==== Generic ====
[x]: MUST Package is licensed with an open-source compatible license and meets
     other legal requirements as defined in the legal section of Packaging
     Guidelines.
[x]: MUST Package successfully compiles and builds into binary rpms on at
     least one supported primary architecture.
[x]: MUST %build honors applicable compiler flags or justifies otherwise.
[x]: MUST All build dependencies are listed in BuildRequires, except for any
     that are listed in the exceptions section of Packaging Guidelines.
     Note: The package did not built BR could therefore not be checked or the
     package failed to build because of missing BR
[x]: MUST Buildroot is not present
     Note: Unless packager wants to package for EPEL5 this is fine
[x]: MUST Package contains no bundled libraries.
[x]: MUST Changelog in prescribed format.
[x]: MUST Package has no %clean section with rm -rf %{buildroot} (or
     $RPM_BUILD_ROOT)
     Note: Clean would be needed if support for EPEL is required
[x]: MUST Sources contain only permissible code or content.
[x]: MUST Each %files section contains %defattr if rpm < 4.4
     Note: Note: defattr macros not found. They would be needed for EPEL5
[x]: MUST Macros in Summary, %description expandable at SRPM build time.
[x]: MUST Package requires other packages for directories it uses.
[x]: MUST Package uses nothing in %doc for runtime.
[x]: MUST Package is not known to require ExcludeArch.
[x]: MUST Permissions on files are set properly.
[x]: MUST Package does not contain duplicates in %files.
[x]: MUST Spec file lacks Packager, Vendor, PreReq tags.
[x]: MUST Package does not run rm -rf %{buildroot} (or $RPM_BUILD_ROOT) at the
     beginning of %install.
     Note: rm -rf would be needed if support for EPEL5 is required
[-]: MUST Large documentation files are in a -doc subpackage, if required.
[x]: MUST If (and only if) the source package includes the text of the
     license(s) in its own file, then that file, containing the text of the
     license(s) for the package is included in %doc.
[x]: MUST License field in the package spec file matches the actual license.
[x]: MUST Package consistently uses macros (instead of hard-coded directory
     names).
[x]: MUST Package is named according to the Package Naming Guidelines.
[x]: MUST Package does not generate any conflict.
[x]: MUST Package obeys FHS, except libexecdir and /usr/target.
[x]: MUST Package must own all directories that it creates.
[x]: MUST Package does not own files or directories owned by other packages.
[x]: MUST Package installs properly.
[x]: MUST Requires correct, justified where necessary.
[x]: MUST Rpmlint output is silent.
[x]: MUST Sources used to build the package match the upstream source, as
     provided in the spec URL.
/home/shaks/710383/Agda-executable-2.3.0.1.tar.gz :
  MD5SUM this package     : a9c803f0a829cf54d35b1a82f0ba6181
  MD5SUM upstream package : a9c803f0a829cf54d35b1a82f0ba6181

[x]: MUST Spec file is legible and written in American English.
[x]: MUST Spec file name must match the spec package %{name}, in the format
     %{name}.spec.
[-]: MUST Package contains a SysV-style init script if in need of one.
[x]: MUST File names are valid UTF-8.
[x]: MUST Useful -debuginfo package or justification otherwise.
[x]: SHOULD Reviewer should test that the package builds in mock.
[x]: SHOULD If the source package does not include license text(s) as a
     separate file from upstream, the packager SHOULD query upstream to
     include it.
[x]: SHOULD Dist tag is present.
[x]: SHOULD No file requires outside of /etc, /bin, /sbin, /usr/bin,
     /usr/sbin.
[x]: SHOULD Final provides and requires are sane (rpm -q --provides and rpm -q
     --requires).
[x]: SHOULD Package functions as described.
[x]: SHOULD Latest version is packaged.
[x]: SHOULD Package does not include license text files separate from
     upstream.
[x]: SHOULD SourceX is a working URL.
[x]: SHOULD Description and summary sections in the package spec file contains
     translations for supported Non-English languages, if available.
[x]: SHOULD Package should compile and build into binary rpms on all supported
     architectures.
[-]: SHOULD %check is present and all tests pass.
[x]: SHOULD Packages should try to preserve timestamps of original installed
     files.
[x]: SHOULD Spec use %global instead of %define.

Generated by fedora-review 0.1.3
External plugins:

Package approved.

Thank you for reviewing.


New Package SCM Request
=======================
Package Name: Agda
Short Description: Dependently typed functional language commandline
Owners: petersen
Branches: f16 f17
InitialCC: haskell-sig

Git done (by process-git-requests).

Agda-2.3.0.1-1.fc17 has been submitted as an update for Fedora 17.
https://admin.fedoraproject.org/updates/Agda-2.3.0.1-1.fc17

Agda-2.3.0.1-1.fc16 has been submitted as an update for Fedora 16.
https://admin.fedoraproject.org/updates/Agda-2.3.0.1-1.fc16

Agda-2.3.0.1-1.fc16 has been pushed to the Fedora 16 testing repository.

Agda-2.3.0.1-1.fc17 has been pushed to the Fedora 17 stable repository.

Agda-2.3.0.1-1.fc16 has been pushed to the Fedora 16 stable repository.