Note: This is a beta release of Red Hat Bugzilla 5.0. The data contained within is a snapshot of the live data so any changes you make will not be reflected in the production Bugzilla. Also email is disabled so feel free to test any aspect of the site that you want. File any problems you find or give feedback here.
Bug 506567 - Review Request: acl2 - Automated reasoning system based on Common Lisp
Summary: Review Request: acl2 - Automated reasoning system based on Common Lisp
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
Target Milestone: ---
Assignee: Nobody's working on this, feel free to take it
QA Contact: Fedora Extras Quality Assurance
Depends On:
TreeView+ depends on / blocked
Reported: 2009-06-17 18:57 UTC by Alan Dunn
Modified: 2010-12-17 17:50 UTC (History)
3 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of:
Last Closed: 2010-12-17 17:50:15 UTC

Attachments (Terms of Use)

Description Alan Dunn 2009-06-17 18:57:05 UTC
Spec URL:

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:


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 14:41:57 UTC
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 16:12:37 UTC
Could you acknowledge that you still wish to submit this?  Sorry if my previous message did not look sufficiently like a ping.

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