Bug 947819 (idris) - Review Request: idris - Functional Programming Language with Dependent Types
Summary: Review Request: idris - Functional Programming Language with Dependent Types
Keywords:
Status: CLOSED ERRATA
Alias: idris
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: Unspecified
OS: Unspecified
unspecified
unspecified
Target Milestone: ---
Assignee: Rick Elrod
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On: ghc-libffi ghc-language-java
Blocks:
TreeView+ depends on / blocked
 
Reported: 2013-04-03 11:17 UTC by Jens Petersen
Modified: 2013-09-12 02:05 UTC (History)
3 users (show)

Fixed In Version: idris-0.9.4.1-2.fc18
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2013-09-12 01:51:37 UTC
Type: ---
relrod: fedora-review+
gwync: fedora-cvs+


Attachments (Terms of Use)

Description Jens Petersen 2013-04-03 11:17:03 UTC
Spec URL: http://petersen.fedorapeople.org//idris.spec
SRPM URL: http://petersen.fedorapeople.org//idris-0.9.7-1.fc18.src.rpm

Description:
Idris is a general purpose language with full dependent types.
It is compiled, with eager evaluation. Dependent types allow types to
be predicated on values, meaning that some aspects of a program's
behavior can be specified precisely in the type. The language is
closely related to Epigram and Agda. There is a tutorial at
<http://www.idris-lang.org/documentation>. Features include:

- Full dependent types with dependent pattern matching
- where clauses, with rule, simple case expressions,
  pattern matching let and lambda bindings
- Type classes, monad comprehensions
- do notation, idiom brackets, syntactic conveniences for lists, tuples,
  dependent pairs
- Totality checking
- Coinductive types
- Indentation significant syntax, extensible syntax
- Tactic based theorem proving (influenced by Coq)
- Cumulative universes
- Simple foreign function interface (to C)
- Hugs style interactive environment.

Comment 1 Jens Petersen 2013-04-03 11:17:11 UTC
This package built on koji:  http://koji.fedoraproject.org/koji/taskinfo?taskID=5203096

Comment 2 Jens Petersen 2013-04-06 04:17:32 UTC
Spec: http://petersen.fedorapeople.org/reviews/idris/idris.spec
SRPM: http://petersen.fedorapeople.org/reviews/idris/idris-0.9.7-2.fc18.src.rpm

Added a requires for gcc, which idris uses when compiling executables.

Comment 3 Jens Petersen 2013-04-08 06:31:09 UTC
(I think 0.9.4.1 builds with haskeline-0.6)

Comment 4 Jens Petersen 2013-06-06 01:22:37 UTC
0.9.8 is out though it needs some additional Haskell dependencies:
language-java and libffi.

Comment 5 Rick Elrod 2013-06-30 16:33:29 UTC
If you want to package the two deps and bump this to the latest upstream version, I'll review the set.

Comment 6 Jens Petersen 2013-07-01 14:02:19 UTC
(In reply to Ricky Elrod from comment #5)
> If you want to package the two deps and bump this to the latest upstream
> version, I'll review the set.

Thank you, you're on!  That would be great. :)

I posted RRs above for libffi and language-java.

I think I have idris nearly ready but I need to build it first
on Rawhide to check since it requires haskeline-0.7 to build...

Comment 7 Jens Petersen 2013-07-01 15:06:03 UTC
I uploaded:

Spec: http://petersen.fedorapeople.org/reviews/idris/idris.spec
SRPM: http://petersen.fedorapeople.org/reviews/idris/idris-0.9.8-1.fc19.src.rpm

but have not built it yet.  (I tried to do mockchain locally
but it failed with some repo metadata errors...)

Comment 8 Jens Petersen 2013-07-02 15:06:15 UTC
Maybe the F19 yum updated got mock and yum working together again.

Anyway with it I managed to build the above package in a mock rawhide root.

But quite a lot of rpmlint output:

idris.x86_64: E: arch-dependent-file-in-usr-share /usr/share/idris-0.9.8/rts/libidris_rts.a
idris.x86_64: W: executable-stack /usr/bin/idris
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/libidris_rts.a
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/libidris_rts.a
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_bitstring.h
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/idris_bitstring.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_opts.h
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/idris_opts.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_stats.h
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/idris_stats.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_gmp.h
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/idris_gmp.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_stdfgn.h
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/idris_stdfgn.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_gc.h
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/idris_gc.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_heap.h
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/idris_heap.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_main.c
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/libtest.c
idris.x86_64: W: devel-file-in-non-devel-package /usr/share/idris-0.9.8/rts/idris_rts.h
idris.x86_64: W: spurious-executable-perm /usr/share/idris-0.9.8/rts/idris_rts.h
idris.x86_64: W: no-manual-page-for-binary idris

Comment 9 Jens Petersen 2013-07-04 10:29:08 UTC
I will try to clean up the rpmlint issues soon.

Comment 10 Jens Petersen 2013-07-08 10:15:57 UTC
Okay I moved the devel files from datadir to under libdir
that at least address the above rpmlint error.

Spec: http://petersen.fedorapeople.org/reviews/idris/idris.spec
SRPM: http://petersen.fedorapeople.org/reviews/idris/idris-0.9.8-2.fc19.src.rpm

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

Comment 11 Rick Elrod 2013-07-08 10:51:09 UTC
Well, we're close ;)

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

Legend:
[x] = Pass, [!] = Fail, [-] = Not applicable, [?] = Not evaluated
[ ] = Manual review needed


Issues:
=======
- Static libraries in -static subpackage, if present.
  Note: Archive *.a files found in idris
  See: http://fedoraproject.org/wiki/Packaging/Guidelines#StaticLibraries

  (This might be a result of https://fedoraproject.org/wiki/Packaging:Haskell#Static_vs._Dynamic_Linking and allowable.
  Can you comment?)

- Header files in -devel subpackage, if present.
  Note: idris :
  /usr/lib64/idris-0.9.8/rts/idris_bitstring.h idris :
  /usr/lib64/idris-0.9.8/rts/idris_gc.h idris :
  /usr/lib64/idris-0.9.8/rts/idris_gmp.h idris :
  /usr/lib64/idris-0.9.8/rts/idris_heap.h idris :
  /usr/lib64/idris-0.9.8/rts/idris_opts.h idris :
  /usr/lib64/idris-0.9.8/rts/idris_rts.h idris :
  /usr/lib64/idris-0.9.8/rts/idris_stats.h idris :
  /usr/lib64/idris-0.9.8/rts/idris_stdfgn.h
  See: http://fedoraproject.org/wiki/Packaging/Guidelines#DevelPackages

  (I am assuming that these header files are required at runtime? Or can we move them into a -devel subpackage?)

- idris.x86_64: W: executable-stack /usr/bin/idris

  (See this link for help with getting rid of this warning:
   https://fedoraproject.org/wiki/Packaging_tricks#Executable_stack)

- Spec use %global instead of %define.
  Note: %define cabal_configure_options --datadir=%{_libdir}

  (Use %global instead :))

===== MUST items =====

C/C++:
[x]: Package does not contain kernel modules.
[x]: Package contains no static executables.
[x]: Package does not contain any libtool archives (.la)
[x]: Rpath absent or only used for internal libs.

Generic:
[x]: Package is licensed with an open-source compatible license and meets
     other legal requirements as defined in the legal section of Packaging
     Guidelines.
[x]: %build honors applicable compiler flags or justifies otherwise.
[x]: Package contains no bundled libraries without FPC exception.
[x]: Changelog in prescribed format.
[x]: Sources contain only permissible code or content.
[-]: Package contains desktop file if it is a GUI application.
[!]: Development files must be in a -devel package
[x]: Package requires other packages for directories it uses.
[x]: Package uses nothing in %doc for runtime.
[x]: Package is not known to require ExcludeArch.
[x]: Package complies to the Packaging Guidelines
[x]: License field in the package spec file matches the actual license.
[x]: Package consistently uses macros (instead of hard-coded directory names).
[x]: Package is named according to the Package Naming Guidelines.
[x]: Package does not generate any conflict.
[x]: Package obeys FHS, except libexecdir and /usr/target.
[-]: If the package is a rename of another package, proper Obsoletes and
     Provides are present.
[x]: Package must own all directories that it creates.
[x]: Package does not own files or directories owned by other packages.
[x]: Requires correct, justified where necessary.
[x]: Spec file is legible and written in American English.
[-]: Package contains systemd file(s) if in need.
[-]: Useful -debuginfo package or justification otherwise.
[x]: Large documentation must go in a -doc subpackage.
[x]: All build dependencies are listed in BuildRequires, except for any that
     are listed in the exceptions section of Packaging Guidelines.
[x]: Package does not run rm -rf %{buildroot} (or $RPM_BUILD_ROOT) at the
     beginning of %install.
[x]: Each %files section contains %defattr if rpm < 4.4
[x]: Macros in Summary, %description expandable at SRPM build time.
[x]: Package does not contain duplicates in %files.
[x]: Permissions on files are set properly.
[x]: Fully versioned dependency in subpackages, if present.
[x]: 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]: Package use %makeinstall only when make install' ' DESTDIR=... doesn't
     work.
[x]: Package is named using only allowed ASCII characters.
[x]: Package do not use a name that already exist
[x]: Package is not relocatable.
[x]: Sources used to build the package match the upstream source, as provided
     in the spec URL.
[x]: Spec file name must match the spec package %{name}, in the format
     %{name}.spec.
[x]: File names are valid UTF-8.
[x]: Packages must not store files under /srv, /opt or /usr/local
[x]: Package successfully compiles and builds into binary rpms on at least one
     supported primary architecture.
[x]: Package installs properly.
[x]: Rpmlint is run on all rpms the build produces.
     Note: There are rpmlint messages (see attachment).

Java:
[x]: Fully versioned dependency in subpackages, if present.
[x]: Bundled jar/class files should be removed before build

===== SHOULD items =====

Generic:
[!]: Spec use %global instead of %define.
     Note: %define cabal_configure_options --datadir=%{_libdir}
[-]: 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]: Final provides and requires are sane (see attachments).
[x]: Package functions as described.
[x]: Latest version is packaged.
[x]: Package does not include license text files separate from upstream.
[-]: Description and summary sections in the package spec file contains
     translations for supported Non-English languages, if available.
[x]: Package should compile and build into binary rpms on all supported
     architectures.
[-]: %check is present and all tests pass.
[x]: Packages should try to preserve timestamps of original installed files.
[x]: Packager, Vendor, PreReq, Copyright tags should not be in spec file
[x]: Sources can be downloaded from URI in Source: tag
[x]: Reviewer should test that the package builds in mock.
[x]: Buildroot is not present
[x]: Package has no %clean section with rm -rf %{buildroot} (or
     $RPM_BUILD_ROOT)
[x]: Dist tag is present.
[x]: No file requires outside of /etc, /bin, /sbin, /usr/bin, /usr/sbin.
[x]: SourceX tarball generation or download is documented.
[x]: SourceX is a working URL.

===== EXTRA items =====

Generic:
[x]: Large data in /usr/share should live in a noarch subpackage if package is
     arched.
[x]: Rpmlint is run on all installed packages.
     Note: There are rpmlint messages (see attachment).
[x]: Spec file according to URL is the same as in SRPM.


Rpmlint
-------
Checking: idris-0.9.8-2.fc20.x86_64.rpm
idris.x86_64: W: spelling-error %description -l en_US http -> HTTP
idris.x86_64: W: spelling-error %description -l en_US www -> WWW, wow
idris.x86_64: W: spelling-error %description -l en_US lang -> Lang, lag, slang
idris.x86_64: W: spelling-error %description -l en_US monad -> nomad, gonad, Mona
idris.x86_64: W: spelling-error %description -l en_US tuples -> letups
idris.x86_64: W: executable-stack /usr/bin/idris
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_gmp.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_gmp.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_stats.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_stats.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_gc.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_gc.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_opts.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_opts.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_bitstring.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_bitstring.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/libtest.c
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_stdfgn.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_stdfgn.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_main.c
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_rts.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_rts.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/libidris_rts.a
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/libidris_rts.a
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_heap.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_heap.h
idris.x86_64: W: no-manual-page-for-binary idris
1 packages and 0 specfiles checked; 0 errors, 27 warnings.




Rpmlint (installed packages)
----------------------------
# rpmlint idris
idris.x86_64: W: spelling-error %description -l en_US http -> HTTP
idris.x86_64: W: spelling-error %description -l en_US www -> WWW, wow
idris.x86_64: W: spelling-error %description -l en_US lang -> Lang, lag, slang
idris.x86_64: W: spelling-error %description -l en_US monad -> nomad, gonad, Mona
idris.x86_64: W: spelling-error %description -l en_US tuples -> letups
idris.x86_64: W: executable-stack /usr/bin/idris
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_gmp.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_gmp.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_stats.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_stats.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_gc.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_gc.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_opts.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_opts.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_bitstring.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_bitstring.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/libtest.c
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_stdfgn.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_stdfgn.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_main.c
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_rts.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_rts.h
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/libidris_rts.a
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/libidris_rts.a
idris.x86_64: W: devel-file-in-non-devel-package /usr/lib64/idris-0.9.8/rts/idris_heap.h
idris.x86_64: W: spurious-executable-perm /usr/lib64/idris-0.9.8/rts/idris_heap.h
idris.x86_64: W: no-manual-page-for-binary idris
1 packages and 0 specfiles checked; 0 errors, 27 warnings.
# echo 'rpmlint-done:'



Requires
--------
idris (rpmlib, GLIBC filtered):
    gcc
    ghc(Cabal-1.16.0-eb3c12450ebbf2810048acb780cbe706)
    ghc(array-0.4.0.1-3b78425c10ff2dad7acf7e8c8ae014c3)
    ghc(base-4.6.0.1-8aa5d403c45ea59dcd2c39f123e27d57)
    ghc(binary-0.5.1.1-72ed744c57c32286a49da6dda4f660b7)
    ghc(bytestring-0.10.0.2-4f93248f75667c2c3321a7a6761b576f)
    ghc(containers-0.5.0.0-ab1dae9a94cd3cc84e7b2805636ebfa2)
    ghc(cpphs-1.16-15d27b0080912629e5fe51cce6f4d42a)
    ghc(deepseq-1.3.0.1-5cc4cd89bdc2e8f6db1833d95ec36926)
    ghc(directory-1.2.0.1-91a788fd88acd7f149f0f10f5f1e23f2)
    ghc(filepath-1.3.0.1-b12cbe18566fe1532a1fda4c85e31cbe)
    ghc(ghc-prim-0.3.0.0-d5221a8c8a269b66ab9a07bdc23317dd)
    ghc(haskeline-0.7.0.3-8894d9bc6e16c683c2ede97ddf359f66)
    ghc(integer-gmp-0.5.0.0-2f15426f5b53fe4c6490832f9b20d8d7)
    ghc(language-java-0.2.4-0b0e647223770d9fdac16675bfcd278f)
    ghc(libffi-0.1-246dc5ea50873b4e73708a886ef510f1)
    ghc(mtl-2.1.2-82086cac9073862cbe01e44b81ec8b9b)
    ghc(old-locale-1.0.0.5-6729cb9d9cc62d150655de8fc5401b91)
    ghc(old-time-1.1.0.1-2f8ea093d0c7014780a8a5772f948883)
    ghc(parsec-3.1.3-441f1388bc13de47c52a9ba8a23194f4)
    ghc(pretty-1.1.1.0-66181c695e6a2e173ba2088cf55cc396)
    ghc(process-1.1.0.2-76e05340eb66705981411022731ca84a)
    ghc(split-0.2.2-7a3d16e611eda8c6cc8850aa57490f5e)
    ghc(terminfo-0.3.2.5-fb31957b4beb6a67d2abe1b1ac2ae4e0)
    ghc(text-0.11.3.1-e38859e86485c167fa7c9441789e7607)
    ghc(time-1.4.0.1-10dc4804a19dc0000fab79908f1a9f50)
    ghc(transformers-0.3.0.0-387c76a892254b0b8fe4d66f4780ad17)
    ghc(unix-2.6.0.1-4f219f792083f70ec440ce406f12ce57)
    libHSCabal-1.16.0-ghc7.6.3.so()(64bit)
    libHSarray-0.4.0.1-ghc7.6.3.so()(64bit)
    libHSbase-4.6.0.1-ghc7.6.3.so()(64bit)
    libHSbinary-0.5.1.1-ghc7.6.3.so()(64bit)
    libHSbytestring-0.10.0.2-ghc7.6.3.so()(64bit)
    libHScontainers-0.5.0.0-ghc7.6.3.so()(64bit)
    libHScpphs-1.16-ghc7.6.3.so()(64bit)
    libHSdeepseq-1.3.0.1-ghc7.6.3.so()(64bit)
    libHSdirectory-1.2.0.1-ghc7.6.3.so()(64bit)
    libHSfilepath-1.3.0.1-ghc7.6.3.so()(64bit)
    libHSghc-prim-0.3.0.0-ghc7.6.3.so()(64bit)
    libHShaskeline-0.7.0.3-ghc7.6.3.so()(64bit)
    libHSinteger-gmp-0.5.0.0-ghc7.6.3.so()(64bit)
    libHSlanguage-java-0.2.4-ghc7.6.3.so()(64bit)
    libHSlibffi-0.1-ghc7.6.3.so()(64bit)
    libHSmtl-2.1.2-ghc7.6.3.so()(64bit)
    libHSold-locale-1.0.0.5-ghc7.6.3.so()(64bit)
    libHSold-time-1.1.0.1-ghc7.6.3.so()(64bit)
    libHSparsec-3.1.3-ghc7.6.3.so()(64bit)
    libHSpretty-1.1.1.0-ghc7.6.3.so()(64bit)
    libHSprocess-1.1.0.2-ghc7.6.3.so()(64bit)
    libHSrts-ghc7.6.3.so()(64bit)
    libHSsplit-0.2.2-ghc7.6.3.so()(64bit)
    libHSterminfo-0.3.2.5-ghc7.6.3.so()(64bit)
    libHStext-0.11.3.1-ghc7.6.3.so()(64bit)
    libHStime-1.4.0.1-ghc7.6.3.so()(64bit)
    libHStransformers-0.3.0.0-ghc7.6.3.so()(64bit)
    libHSunix-2.6.0.1-ghc7.6.3.so()(64bit)
    libc.so.6()(64bit)
    libdl.so.2()(64bit)
    libffi.so.6()(64bit)
    libgmp.so.10()(64bit)
    libm.so.6()(64bit)
    libncursesw.so.5()(64bit)
    libpthread.so.0()(64bit)
    librt.so.1()(64bit)
    libtinfo.so.5()(64bit)
    libutil.so.1()(64bit)
    rtld(GNU_HASH)



Provides
--------
idris:
    idris
    idris(x86-64)



Source checksums
----------------
http://hackage.haskell.org/packages/archive/idris/0.9.8/idris-0.9.8.tar.gz :
  CHECKSUM(SHA256) this package     : f0f868788aa83c29a8832c07dd9587fa08170646bce39ba245a0b4c16235acd7
  CHECKSUM(SHA256) upstream package : f0f868788aa83c29a8832c07dd9587fa08170646bce39ba245a0b4c16235acd7


Generated by fedora-review 0.4.1 (b2e211f) last change: 2013-04-29
Buildroot used: fedora-rawhide-x86_64
Command line :/usr/bin/fedora-review -m fedora-rawhide-x86_64 -b 947819

Comment 12 Jens Petersen 2013-07-10 04:04:05 UTC
Thanks Ricky for reviewing

> - Static libraries in -static subpackage, if present.
>   Note: Archive *.a files found in idris
>   See: http://fedoraproject.org/wiki/Packaging/Guidelines#StaticLibraries
> 
>   (This might be a result of
> https://fedoraproject.org/wiki/Packaging:Haskell#Static_vs._Dynamic_Linking
> and allowable.

(cf also the newer approved https://fedoraproject.org/wiki/PackagingDrafts/Haskell#Shared_and_static_library_linking)

>   Can you comment?)

Well I agree it would be nicer to have a shared dynamic runtime library.
But given that currently there is only a static one and idris is still
kind of experimental I think the packaging is probably okay for now:
given the status quo I don't really see a point in subpackaging
the static library.  Maybe if we come to packaging projects written
in Idris some day we should revisit this - but most distros don't even
use dynamic linking for Haskell executables yet (unlike Fedora)...

The other problem is that adding a -devel subpackage will probably
make idris multilib which is a bit silly IMHO.

But see also more comments below. :)

> - Header files in -devel subpackage, if present.
>   Note: idris :
>   /usr/lib64/idris-0.9.8/rts/idris_bitstring.h idris :
>   /usr/lib64/idris-0.9.8/rts/idris_gc.h idris :
>   /usr/lib64/idris-0.9.8/rts/idris_gmp.h idris :
>   /usr/lib64/idris-0.9.8/rts/idris_heap.h idris :
>   /usr/lib64/idris-0.9.8/rts/idris_opts.h idris :
>   /usr/lib64/idris-0.9.8/rts/idris_rts.h idris :
>   /usr/lib64/idris-0.9.8/rts/idris_stats.h idris :
>   /usr/lib64/idris-0.9.8/rts/idris_stdfgn.h
>   See: http://fedoraproject.org/wiki/Packaging/Guidelines#DevelPackages
> 
>   (I am assuming that these header files are required at runtime? Or can we
> move them into a -devel subpackage?)

Right - they are needed when compiling idris code into an executable.

Personally I would prefer just to keep the current packaging.
While the idris interpreter can run without the rts files -
some functionality like compilation will not work.

idris would have to require idris-devel anyway.
IMHO since idris is a development package 
it doesn't need to have a devel subpackage
(at this time anyway).

> - idris.x86_64: W: executable-stack /usr/bin/idris
> 
>   (See this link for help with getting rid of this warning:
>    https://fedoraproject.org/wiki/Packaging_tricks#Executable_stack)

See bug 973512.

I sent a mail to the ghc users list yesterday and this got fixed
already upstream yesterday.  I just backported the patch
to ghc-7.6.3-15.fc20 so far, but not actually tested yet...

> - Spec use %global instead of %define.
>   Note: %define cabal_configure_options --datadir=%{_libdir}
> 
>   (Use %global instead :))

Okay - though it was intentional (since it's only needed for
the %build section).  Anyway let me replace it with a variable. :)


Spec: http://petersen.fedorapeople.org/reviews/idris/idris.spec
SRPM: http://petersen.fedorapeople.org/reviews/idris/idris-0.9.8-3.fc19.src.rpm

Koji: http://koji.fedoraproject.org/koji/taskinfo?taskID=5589311
(built with ghc-7.6.3-15.fc20)

Comment 13 Jens Petersen 2013-07-10 09:55:54 UTC
(Unfortunately ghc-7.6.3-15.fc20 didn't fix the execstack issue apparently
so I put a workaround in ghc-rpm-macros for now so that %ghc_bin_install
and %ghc_lib_install should clear the execstack flag for all executables.)

You can see it working in this scratch build:
http://koji.fedoraproject.org/koji/taskinfo?taskID=5589735

I will backport this change to f18 and f19 ghc-rpm-macros shortly.

Comment 14 Jens Petersen 2013-07-11 10:41:43 UTC
(In reply to Jens Petersen from comment #13)
> I will backport this change to f18 and f19 ghc-rpm-macros shortly.

(Actually as far as I can determine it only affects ghc-7.4.2 (f19) and
ghc-7.6.3 (f20), and I have pushed an update for ghc-rpm-macros to
f19 testing.)

Comment 15 Jens Petersen 2013-07-16 05:53:44 UTC
Ricky, anything more left here?

Comment 16 Rick Elrod 2013-07-16 05:56:05 UTC
I think this looks good now.
APPROVED.

Comment 17 Jens Petersen 2013-07-16 09:21:16 UTC
Thank you for the review.


New Package SCM Request
=======================
Package Name: idris
Short Description: Functional programming language with dependent types
Owners: petersen
Branches: f19 f18 el6
InitialCC: haskell-sig

Comment 18 Gwyn Ciesla 2013-07-16 12:03:43 UTC
Git done (by process-git-requests).

Comment 19 Jens Petersen 2013-07-17 01:18:29 UTC
idris-0.9.8-3.fc20 has been built for rawhide.

I will build it soonish for F19 and earlier.

Comment 20 Rick Elrod 2013-08-11 15:31:19 UTC
any update here? :)

Comment 21 Fedora Update System 2013-08-20 04:12:48 UTC
hledger-0.19.3-1.fc19,idris-0.9.8-3.fc19,darcs-2.8.4-1.fc19,Agda-2.3.2.1-1.fc19,ghc-haskeline-0.7.0.3-1.fc19,ghc-hledger-lib-0.19.3-1.fc19 has been submitted as an update for Fedora 19.
https://admin.fedoraproject.org/updates/hledger-0.19.3-1.fc19,idris-0.9.8-3.fc19,darcs-2.8.4-1.fc19,Agda-2.3.2.1-1.fc19,ghc-haskeline-0.7.0.3-1.fc19,ghc-hledger-lib-0.19.3-1.fc19

Comment 22 Fedora Update System 2013-08-20 09:02:14 UTC
idris-0.9.4.1-1.fc18 has been submitted as an update for Fedora 18.
https://admin.fedoraproject.org/updates/idris-0.9.4.1-1.fc18

Comment 23 Fedora Update System 2013-08-21 00:08:30 UTC
idris-0.9.4.1-1.fc18 has been pushed to the Fedora 18 testing repository.

Comment 24 Fedora Update System 2013-09-12 01:51:37 UTC
hledger-0.19.3-1.fc19, idris-0.9.8-3.fc19, darcs-2.8.4-1.fc19, ghc-haskeline-0.7.0.3-1.fc19, ghc-hledger-lib-0.19.3-1.fc19, Agda-2.3.2.1-5.fc19 has been pushed to the Fedora 19 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 25 Fedora Update System 2013-09-12 02:05:58 UTC
idris-0.9.4.1-2.fc18 has been pushed to the Fedora 18 stable repository.


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