Bug 506567

Summary: Review Request: acl2 - Automated reasoning system based on Common Lisp
Product: [Fedora] Fedora Reporter: Alan Dunn <amdunn>
Component: Package ReviewAssignee: Nobody's working on this, feel free to take it <nobody>
Status: CLOSED NOTABUG QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: medium Docs Contact:
Priority: medium    
Version: rawhideCC: fedora-package-review, grue, notting
Target Milestone: ---   
Target Release: ---   
Hardware: All   
OS: Linux   
Whiteboard:
Fixed In Version: Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: 2010-12-17 12:50:15 EST Type: ---
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: ---
Bug Depends On:    
Bug Blocks: 201449    

Description Alan Dunn 2009-06-17 14:57:05 EDT
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?)
Comment 1 Jason Tibbitts 2010-11-03 10:41:57 EDT
I tried building this, but even on a fast machine I gave up before it finished.  How long is it supposed to take, anyway?

Adding the blocker for the SciTech sig so hopefully more folks will notice.
Comment 2 Jason Tibbitts 2010-11-15 11:12:37 EST
Could you acknowledge that you still wish to submit this?  Sorry if my previous message did not look sufficiently like a ping.