Bug 710383 (Agda) - Review Request: Agda - Commandline for dependently typed functional language
Summary: Review Request: Agda - Commandline for dependently typed functional language
Alias: Agda
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
Target Milestone: ---
Assignee: Shakthi Kannan
QA Contact: Fedora Extras Quality Assurance
Depends On: ghc-Agda
Blocks: Haskell-pkg-reviews Agda-stdlib
TreeView+ depends on / blocked
Reported: 2011-06-03 09:28 UTC by Jens Petersen
Modified: 2012-08-02 11:24 UTC (History)
7 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of:
Last Closed: 2012-08-02 11:21:49 UTC
shakthimaan: fedora-review+
tibbs: fedora-cvs+

Attachments (Terms of Use)

Description Jens Petersen 2011-06-03 09:28:20 UTC
Spec URL: http://petersen.fedorapeople.org/Agda/Agda.spec
SRPM URL: http://petersen.fedorapeople.org/Agda/Agda-2.2.10-1.fc15.src.rpm
Commandline wrapper for the Agda dependently typed
functional programming language.

Comment 1 Jens Petersen 2012-06-15 01:29:03 UTC
Needs to be updated to Agda 2.3

Comment 2 Jens Petersen 2012-07-10 08:19:59 UTC
Ok finally:

Spec: http://petersen.fedorapeople.org/reviews/Agda/Agda.spec
SRPM: http://petersen.fedorapeople.org/reviews/Agda/Agda-

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.

Comment 3 Shakthi Kannan 2012-07-10 11:29:56 UTC
Even though the hackage page doesn't mention it, the Agda stdlib are required for Agda-executable:


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:


Comment 4 Jens Petersen 2012-07-11 06:13:59 UTC
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.

Comment 5 Jens Petersen 2012-07-11 12:11:50 UTC
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.

Comment 6 Jens Petersen 2012-07-12 00:41:12 UTC
I see Debian has an "agda" meta-package that pulls in Agda-executable,
Agda and the stdlib.

Comment 7 Shakthi Kannan 2012-07-12 14:34:13 UTC
Package Review

- = 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
[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
     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
[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- :
  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
[-]: 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,
[x]: SHOULD Final provides and requires are sane (rpm -q --provides and rpm -q
[x]: SHOULD Package functions as described.
[x]: SHOULD Latest version is packaged.
[x]: SHOULD Package does not include license text files separate from
[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
[-]: SHOULD %check is present and all tests pass.
[x]: SHOULD Packages should try to preserve timestamps of original installed
[x]: SHOULD Spec use %global instead of %define.

Generated by fedora-review 0.1.3
External plugins:

Package approved.

Comment 8 Jens Petersen 2012-07-13 01:17:24 UTC
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

Comment 9 Jason Tibbitts 2012-07-13 22:58:05 UTC
Git done (by process-git-requests).

Comment 10 Fedora Update System 2012-07-15 08:10:02 UTC
Agda- has been submitted as an update for Fedora 17.

Comment 11 Fedora Update System 2012-07-15 08:10:12 UTC
Agda- has been submitted as an update for Fedora 16.

Comment 12 Fedora Update System 2012-07-15 21:25:09 UTC
Agda- has been pushed to the Fedora 16 testing repository.

Comment 13 Fedora Update System 2012-08-02 11:21:49 UTC
Agda- has been pushed to the Fedora 17 stable repository.

Comment 14 Fedora Update System 2012-08-02 11:24:20 UTC
Agda- has been pushed to the Fedora 16 stable repository.

Note You need to log in before you can comment on or make changes to this bug.