Bug 710031 (ghc-Agda)

Summary: Review Request: ghc-Agda - Dependently typed functional programming language
Product: [Fedora] Fedora Reporter: Jens Petersen <petersen>
Component: Package ReviewAssignee: Shakthi Kannan <shakthimaan>
Status: CLOSED CURRENTRELEASE QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: medium Docs Contact:
Priority: low    
Version: rawhideCC: fedora-package-review, haskell-devel, lakshminaras2002, miles, notting, shakthimaan
Target Milestone: ---Flags: shakthimaan: fedora-review+
gwync: fedora-cvs+
Target Release: ---   
Hardware: All   
OS: Linux   
Whiteboard:
Fixed In Version: Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: 2012-06-10 01:26:52 UTC Type: ---
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: --- Target Upstream Version:
Embargoed:
Bug Depends On: 782000    
Bug Blocks: 710383    

Description Jens Petersen 2011-06-02 10:04:04 UTC
Spec URL: http://petersen.fedorapeople.org/ghc-Agda/ghc-Agda.spec
SRPM URL: http://petersen.fedorapeople.org/ghc-Agda/ghc-Agda-2.2.10-1.fc15.src.rpm

Description: 
A dependently typed functional programming language and proof assistant.

http://wiki.portal.chalmers.se/agda/

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 provides the Agda core library and an emacs mode
for interacting with the language.

Comment 3 Jens Petersen 2011-11-24 04:35:10 UTC
Agda-2.3.0 was just released.  It has a new dependency on hashtables.

Comment 4 Jens Petersen 2012-02-07 09:51:17 UTC
I will update to 2.3.0 soon.

Comment 5 Jens Petersen 2012-02-14 04:16:53 UTC
Updating to current 2.3.0 release:

Spec URL: http://petersen.fedorapeople.org/reviews/ghc-Agda/ghc-Agda.spec
SRPM URL: http://petersen.fedorapeople.org/reviews/ghc-Agda/ghc-Agda-2.3.0-1.fc16.src.rpm

Note it needs latest redhat-rpm-config update to build for
%ghc_arches_with_ghci (currently being pushed to f15 updates stable).

http://koji.fedoraproject.org/koji/taskinfo?taskID=3788957 (25min in koji)

Comment 7 Shakthi Kannan 2012-05-30 09:30:25 UTC
Package Review
==============

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

==== C/C++ ====
[x]: MUST Package does not contain any libtool archives (.la)
[-]: MUST Package does not contain kernel modules.
[-]: MUST Package contains no static executables.
[-]: MUST Rpath absent or only used for internal libs.
[-]: MUST Package is not relocatable.
[!]: MUST Development (unversioned) .so files in -devel subpackage, if
     present.

Waived.

[-]: MUST Static libraries in -static subpackage, if present.

==== 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.
[!]: MUST Each %files section contains %defattr if rpm < 4.4
     Note: defattr(....) present in %files -n emacs-agda section. This is OK
     if packaging for EPEL5. Otherwise not needed
[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 Fully versioned dependency in subpackages, if present.
[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
[x]: 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.
[!]: MUST License field in the package spec file matches the actual license.

The http://hackage.haskell.org/package/Agda page says "OtherLicense" while  http://code.haskell.org/Agda/LICENSE says it is a BSD license. Why does the .spec file say it is MIT license?

[x]: MUST License file installed when any subpackage combination is installed.
[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.

$  rpmlint ghc-Agda-2.3.0.1-1.fc16.src.rpm 
ghc-Agda.src: W: spelling-error %description -l en_US parameterized -> parameter
ghc-Agda.src: W: spelling-error %description -l en_US mixfix -> mix fix, mix-fix, mix
ghc-Agda.src: W: spelling-error %description -l en_US intuitionistic -> intuition, contortionist, constitutions
ghc-Agda.src: W: spelling-error %description -l en_US foundational -> foundation, unconditional
ghc-Agda.src: W: spelling-error %description -l en_US emacs -> Emacs, macs, maces
1 packages and 0 specfiles checked; 0 errors, 5 warnings.

$  rpmlint ghc-Agda-2.3.0.1-1.fc16.x86_64.rpm 
ghc-Agda.x86_64: W: spelling-error %description -l en_US parameterized -> parameter
ghc-Agda.x86_64: W: spelling-error %description -l en_US mixfix -> mix fix, mix-fix, mix
ghc-Agda.x86_64: W: spelling-error %description -l en_US intuitionistic -> intuition, contortionist, constitutions
ghc-Agda.x86_64: W: spelling-error %description -l en_US foundational -> foundation, unconditional
ghc-Agda.x86_64: W: spelling-error %description -l en_US emacs -> Emacs, macs, maces
1 packages and 0 specfiles checked; 0 errors, 5 warnings.

$  rpmlint ghc-Agda-devel-2.3.0.1-1.fc16.x86_64.rpm 
ghc-Agda-devel.x86_64: W: spelling-error %description -l en_US parameterized -> parameter
ghc-Agda-devel.x86_64: W: spelling-error %description -l en_US mixfix -> mix fix, mix-fix, mix
ghc-Agda-devel.x86_64: W: spelling-error %description -l en_US intuitionistic -> intuition, contortionist, constitutions
ghc-Agda-devel.x86_64: W: spelling-error %description -l en_US foundational -> foundation, unconditional
1 packages and 0 specfiles checked; 0 errors, 4 warnings.

$  rpmlint ../SPECS/ghc-Agda.spec 
0 packages and 1 specfiles checked; 0 errors, 0 warnings.

[x]: MUST Sources used to build the package match the upstream source, as
     provided in the spec URL.
/home/shaks/710031/Agda-2.3.0.1.tar.gz :
  MD5SUM this package     : 3caa2466ae4f925dd37320336e2e839c
  MD5SUM upstream package : 3caa2466ae4f925dd37320336e2e839c

[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.
[-]: MUST Useful -debuginfo package or justification otherwise.
[x]: SHOULD Reviewer should test that the package builds in mock.
[-]: 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.
[-]: 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.

Issues:
[!]: MUST Each %files section contains %defattr if rpm < 4.4
     Note: defattr(....) present in %files -n emacs-agda section. This is OK
     if packaging for EPEL5. Otherwise not needed
See: http://fedoraproject.org/wiki/Packaging/Guidelines#FilePermissions
[!]: MUST License field in the package spec file matches the actual license.

Generated by fedora-review 0.1.3
External plugins:

Comment 8 Jens Petersen 2012-05-30 10:00:40 UTC
> [!]: MUST Each %files section contains %defattr if rpm < 4.4
>      Note: defattr(....) present in %files -n emacs-agda section. This is OK
>      if packaging for EPEL5. Otherwise not needed

No plans presently to build for epel5.

> [!]: MUST License field in the package spec file matches the actual license.
> 
> The http://hackage.haskell.org/package/Agda page says "OtherLicense" while 
> http://code.haskell.org/Agda/LICENSE says it is a BSD license. Why does the
> .spec file say it is MIT license?

The LICENSE file is MIT, plus one file which is BSD.  So strictly speaking
I guess the Fedora License tag should actually be "MIT and BSD" I guess.

I think older Cabal did not support the MIT license tag so that
is why it is OtherLicense.  Probably the .cabal could/should be
updated upstream to say MIT now.  I will try to ask them about it -
anyway don't think it blocks this review.

Comment 9 Shakthi Kannan 2012-05-30 10:05:13 UTC
Kindly update the license info, and also request upstream to do the same. Otherwise, the package looks good.

Package approved.

Comment 10 Jens Petersen 2012-05-30 10:14:12 UTC
Thanks again for the review.

Sure, I will fix the License tag when importing.


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

Comment 11 Gwyn Ciesla 2012-05-30 11:53:20 UTC
Git done (by process-git-requests).

Comment 12 Fedora Update System 2012-05-31 05:41:11 UTC
ghc-Agda-2.3.0.1-2.fc16 has been submitted as an update for Fedora 16.
https://admin.fedoraproject.org/updates/ghc-Agda-2.3.0.1-2.fc16

Comment 13 Fedora Update System 2012-05-31 05:43:20 UTC
ghc-Agda-2.3.0.1-2.fc17 has been submitted as an update for Fedora 17.
https://admin.fedoraproject.org/updates/ghc-Agda-2.3.0.1-2.fc17

Comment 14 Fedora Update System 2012-06-01 17:00:47 UTC
ghc-Agda-2.3.0.1-2.fc16 has been pushed to the Fedora 16 testing repository.

Comment 15 Fedora Update System 2012-06-10 01:26:52 UTC
ghc-Agda-2.3.0.1-2.fc17 has been pushed to the Fedora 17 stable repository.

Comment 16 Fedora Update System 2012-06-10 01:38:11 UTC
ghc-Agda-2.3.0.1-2.fc16 has been pushed to the Fedora 16 stable repository.

Comment 17 Fedora Update System 2012-12-13 07:46:41 UTC
ghc-Agda-2.3.0.1-9.el6 has been submitted as an update for Fedora EPEL 6.
https://admin.fedoraproject.org/updates/ghc-Agda-2.3.0.1-9.el6

Comment 18 Fedora Update System 2012-12-29 19:33:22 UTC
ghc-Agda-2.3.0.1-9.el6 has been pushed to the Fedora EPEL 6 stable repository.