Note: This is a public test instance of Red Hat Bugzilla. The data contained within is a snapshot of the live data so any changes you make will not be reflected in the production Bugzilla. Email is disabled so feel free to test any aspect of the site that you want. File any problems you find or give feedback at bugzilla.redhat.com.
Bug 710383 (Agda)
Summary: | Review Request: Agda - Commandline for dependently typed functional language | ||
---|---|---|---|
Product: | [Fedora] Fedora | Reporter: | Jens Petersen <petersen> |
Component: | Package Review | Assignee: | Shakthi Kannan <shakthimaan> |
Status: | CLOSED ERRATA | QA Contact: | Fedora Extras Quality Assurance <extras-qa> |
Severity: | medium | Docs Contact: | |
Priority: | medium | ||
Version: | rawhide | CC: | dwmw2, fedora-package-review, haskell-devel, miles, notting, package-review, shakthimaan |
Target Milestone: | --- | Flags: | shakthimaan:
fedora-review+
j: 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-08-02 11:21:49 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: | 710031 | ||
Bug Blocks: | 634048, 839260 |
Description
Jens Petersen
2011-06-03 09:28:20 UTC
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. |