[Bug 506567] New: Review Request: acl2 - Automated reasoning system based on Common Lisp

[bugzilla at redhat.com]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.

Summary: Review Request: acl2 - Automated reasoning system based on Common Lisp

https://bugzilla.redhat.com/show_bug.cgi?id=506567

           Summary: Review Request: acl2 - Automated reasoning system
                    based on Common Lisp
           Product: Fedora
           Version: rawhide
          Platform: All
        OS/Version: Linux
            Status: NEW
          Severity: medium
          Priority: medium
         Component: Package Review
        AssignedTo: nobody at fedoraproject.org
        ReportedBy: amdunn at gmail.com
         QAContact: extras-qa at fedoraproject.org
                CC: notting at redhat.com, fedora-package-review at redhat.com
   Estimated Hours: 0.0
    Classification: Fedora


Spec URL: https://www.openproofs.org/packages/acl2/acl2.spec
SRPM URL: https://www.openproofs.org/packages/acl2/acl2-3.5-1.fc10.src.rpm
Description:

ACL2 is an automated reasoning system developed at Computational
Logic, Inc., and the University of Texas at Austin.  It is valuable if
you want to prove properties about a system that can be easily
modeled as recursive functions in a Lisp-based language.  ACL2 stands
for "A Computational Logic for Applicative Common Lisp", and is
simultaneously a computational logic, formal specification language,
programming system, and theorem prover.  Its syntax is based on Common
Lisp, and many ACL2 specifications are executable (depending on how
ACL2 is used).

This package is largely complete in that it allows the user to use the
vast majority of the functionality of ACL2, the main thing that isn't
quite right (that I've been working with upstream to fix) is that some
of the (supplementary - program works without them) elisp files don't
seem to compile and/or give warnings.

I have tested a built version out with some of my own basic usage and have
encountered no problems (eg: books load properly despite having moved things
around - to comply with packaging policy - compared to their original locations
in a usual install).

rpmlint output with my comments:

acl2.i386: E: devel-dependency acl2-books-source

acl2-books-source is not really a "devel" repository in that it
contains the text of the theorem libraries, not of the LISP that runs
ACL2 itself. It is critical to using the theorem prover to have this
text available. My naming convention matches the Debian package.

acl2.i386: E: no-binary
acl2.i386: W: only-non-binary-in-usr-lib

I believe this is wrong - saved_acl2.core is a binary core file
(platform dependent I believe) used by LISP.

acl2-books.i386: W: only-non-binary-in-usr-lib

I believe the .fasl files are also binary and platform dependent.

acl2-books.i386: W: no-documentation
acl2-books-certs.noarch: W: no-documentation
acl2-books-source.noarch: W: no-documentation
acl2-emacs-el.noarch: W: no-documentation
acl2-xemacs-el.noarch: W: no-documentation

True, but not important IMO (acl2-doc has documentation).

acl2-doc.noarch: E: non-standard-dir-perm /usr/share/doc/acl2-3.5/HTML 0775
A standard directory should have permission set to 0755. If you get this
message, it means that you have wrong directory permissions in some dirs
included in your package.

This actually appears to be wrong, though I thought this was actually
corrected... (rebuilding now)

This package has built in Koji for F11:

x86:    http://koji.fedoraproject.org/koji/taskinfo?taskID=1406611
x86_64: http://koji.fedoraproject.org/koji/taskinfo?taskID=1406769

and I am rebuilding it now for F12 (builds unfortunately take a long time).

Issues that I see:

1) Elisp compilation as above (the compiled elisp packages currently
don't work, but downloading the elisp source packages still allows one
to use the supplementary LISP).

2) This package includes a LISP core. This core is specific to a given
version and implementation of LISP (eg: if built with F10, it would be
SBCL v1.0.22 as of now). Is there a good way of dealing with this?
(Should I have Fedora version-dependent conditionals that BuildRequire
and Require certain versions of LISP?)

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.