Bug 506567 - Review Request: acl2 - Automated reasoning system based on Common Lisp
Review Request: acl2 - Automated reasoning system based on Common Lisp
Status: CLOSED NOTABUG
Product: Fedora
Classification: Fedora
Component: Package Review (Show other bugs)
rawhide
All Linux
medium Severity medium
: ---
: ---
Assigned To: Nobody's working on this, feel free to take it
Fedora Extras Quality Assurance
:
Depends On:
Blocks: FE-DEADREVIEW
  Show dependency treegraph
 
Reported: 2009-06-17 14:57 EDT by Alan Dunn
Modified: 2010-12-17 12:50 EST (History)
3 users (show)

See Also:
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: ---


Attachments (Terms of Use)

  None (edit)
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.

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