Your message dated Mon, 03 Dec 2007 17:32:05 +0000 with message-id <[EMAIL PROTECTED]> and subject line Bug#440353: fixed in acl2 3.3-1 has caused the attached Bug report to be marked as done.
This means that you claim that the problem has been dealt with. If this is not the case it is now your responsibility to reopen the Bug report if necessary, and/or fix the problem forthwith. (NB: If you are a system administrator and have no idea what I am talking about this indicates a serious mail system misconfiguration somewhere. Please contact me immediately.) Debian bug tracking system administrator (administrator, Debian Bugs database)
--- Begin Message ---Package: acl2 Version: 3.2-1 Severity: normal ------------------------------------------------------------ ACL2 !>(include-book "arithmetic/top" :dir :system) ACL2 Error in ( INCLUDE-BOOK "arithmetic/top" ...): There is no file named "/build/buildd/acl2-3.2/books/arithmetic/top.lisp" that can be opened for input. [...] ACL2 !>(include-book "/usr/share/acl2-3.2/books/arithmetic/top") [... loads the book correctly] ------------------------------------------------------------ A hint on how to fix this can be found on [1]: ------------------------------------------------------------ Distributed Books Directory. We refer to the ``books directory'' of an executable image as the full pathname string of the books directory associated with :dir :system for that image. This is where the distributed books directory should reside. By default, it is the books/ subdirectory of the directory where the sources reside and the executable image is thus built (except for ACL2(r) -- see real --, where it is books/nonstd/). If those books reside elsewhere, the environment variable ACL2_SYSTEM_BOOKS can be set to the books/ directory under which they reside (a Unix-style pathname, typically ending in books/ or books, is permissible). In most cases, your ACL2 executable is a small script in which you can set this environment variable just above the line on which the actual ACL2 image is invoked, for example: export ACL2_SYSTEM_BOOKS ACL2_SYSTEM_BOOKS=/home/acl2/v3-2/acl2-sources/books ------------------------------------------------------------ Sami [1] http://www.cs.utexas.edu/users/moore/acl2/v3-2/INCLUDE-BOOK.html -- System Information: Debian Release: lenny/sid APT prefers unstable APT policy: (500, 'unstable') Architecture: amd64 (x86_64) Kernel: Linux 2.6.22.3-sli (PREEMPT) Locale: LANG=C, [EMAIL PROTECTED] (charmap=ISO-8859-15) Shell: /bin/sh linked to /bin/bash Versions of packages acl2 depends on: ii libc6 2.6.1-1 GNU C Library: Shared libraries ii libgmp3c2 2:4.2.1+dfsg-5 Multiprecision arithmetic library ii libice6 2:1.0.4-1 X11 Inter-Client Exchange library ii libncurses5 5.6+20070825-1 Shared libraries for terminal hand ii libreadline5 5.2-3 GNU readline and history libraries ii libsm6 2:1.0.3-1+b1 X11 Session Management library ii libx11-6 2:1.0.3-7 X11 client-side library ii libxaw7 2:1.0.4-1 X11 Athena Widget library ii libxext6 1:1.0.3-2 X11 miscellaneous extension librar ii libxmu6 1:1.0.3-1 X11 miscellaneous utility library ii libxt6 1:1.0.5-3 X11 toolkit intrinsics library Versions of packages acl2 recommends: ii acl2-books 3.2-1 A Computational Logic for Applicat pn acl2-source <none> (no description available) -- no debconf information
signature.asc
Description: Digital signature
--- End Message ---
--- Begin Message ---Source: acl2 Source-Version: 3.3-1 We believe that the bug you reported is fixed in the latest version of acl2, which is due to be installed in the Debian FTP archive: acl2-books-certs_3.3-1_all.deb to pool/main/a/acl2/acl2-books-certs_3.3-1_all.deb acl2-books-source_3.3-1_all.deb to pool/main/a/acl2/acl2-books-source_3.3-1_all.deb acl2-books_3.3-1_i386.deb to pool/main/a/acl2/acl2-books_3.3-1_i386.deb acl2-doc_3.3-1_all.deb to pool/main/a/acl2/acl2-doc_3.3-1_all.deb acl2-emacs_3.3-1_all.deb to pool/main/a/acl2/acl2-emacs_3.3-1_all.deb acl2-infix-source_3.3-1_all.deb to pool/main/a/acl2/acl2-infix-source_3.3-1_all.deb acl2-infix_3.3-1_i386.deb to pool/main/a/acl2/acl2-infix_3.3-1_i386.deb acl2-source_3.3-1_all.deb to pool/main/a/acl2/acl2-source_3.3-1_all.deb acl2_3.3-1.diff.gz to pool/main/a/acl2/acl2_3.3-1.diff.gz acl2_3.3-1.dsc to pool/main/a/acl2/acl2_3.3-1.dsc acl2_3.3-1_i386.deb to pool/main/a/acl2/acl2_3.3-1_i386.deb acl2_3.3.orig.tar.gz to pool/main/a/acl2/acl2_3.3.orig.tar.gz A summary of the changes between this version and the previous one is attached. Thank you for reporting the bug, which will now be closed. If you have further comments please address them to [EMAIL PROTECTED], and the maintainer will reopen the bug report if appropriate. Debian distribution maintenance software pp. Camm Maguire <[EMAIL PROTECTED]> (supplier of updated acl2 package) (This message was generated automatically at their request; if you believe that there is a problem with it please contact the archive administrators by mailing [EMAIL PROTECTED]) -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Format: 1.7 Date: Mon, 03 Dec 2007 10:10:09 -0500 Source: acl2 Binary: acl2-books-certs acl2-doc acl2 acl2-infix-source acl2-infix acl2-source acl2-books-source acl2-books acl2-emacs Architecture: source all i386 Version: 3.3-1 Distribution: unstable Urgency: low Maintainer: Camm Maguire <[EMAIL PROTECTED]> Changed-By: Camm Maguire <[EMAIL PROTECTED]> Description: acl2 - A Computational Logic for Applicative Common Lisp: main binary acl2-books - A Computational Logic for Applicative Common Lisp: compiled libra acl2-books-certs - A Computational Logic for Applicative Common Lisp: library certif acl2-books-source - A Computational Logic for Applicative Common Lisp: library source acl2-doc - A Computational Logic for Applicative Common Lisp: documentation acl2-emacs - A Computational Logic for Applicative Common Lisp: emacs interfac acl2-infix - A Computational Logic for Applicative Common Lisp: infix interfac acl2-infix-source - A Computational Logic for Applicative Common Lisp: infix source acl2-source - A Computational Logic for Applicative Common Lisp: source files Closes: 430471 434915 440353 Changes: acl2 (3.3-1) unstable; urgency=low . * New upstream release * build-dep on latest gcl to get arm build * Bug fix: "acl2's idea of the system book path is wrong", thanks to Sami Liedes (Closes: #440353). Apply suggested fix to wrapper script, Thanks! * Bug fix: "acl2-emacs: please prefer emacs22", thanks to Tatsuya Kinoshita (Closes: #434915). prefer emacs22 * Bug fix: "acl2: not binNMU safe", thanks to Lior Kaplan (Closes: #430471). Apply suggested patch, Thanks! * build-dep texlive-latex-recommended Files: cd5c565ffb39161847ee959c15f650dd 811 math optional acl2_3.3-1.dsc ec026b72d47d839539ef152ba0784c27 7318498 math optional acl2_3.3.orig.tar.gz 9df68c9351a07d91b5d2939cdce32a87 13522 math optional acl2_3.3-1.diff.gz ae5afcf37bdac945dad9876c6f9b8a4f 2484088 math optional acl2-source_3.3-1_all.deb 86da33b65e4083731fbd1243f5c8f664 54416 math optional acl2-emacs_3.3-1_all.deb 19e19b6b4a1120a6542d3819576b9b8a 85598 math optional acl2-infix-source_3.3-1_all.deb 26baa2c79495807818dd999c2f0614b1 2441412 math optional acl2-books-source_3.3-1_all.deb fd15fde81e21690789dc82efd6085831 1241888 math optional acl2-books-certs_3.3-1_all.deb aaafd3f881967261aebac00401785e3b 2157140 doc optional acl2-doc_3.3-1_all.deb c80dc056aaa5320bfadad7dd1142b233 16892330 math optional acl2_3.3-1_i386.deb 3f8f7038ad75377bee9cf546e1ddec39 170482 math optional acl2-infix_3.3-1_i386.deb 5064abdfdbd124190aa1ea1d9dca8a84 4590788 math optional acl2-books_3.3-1_i386.deb -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) iD8DBQFHVDj7czG1wFfwRdwRAu7PAJ9WpMSHWJeh2i2aVjV78p135XLFZACff37V zhqqIpnCwd1SkFeLi7JJAII= =svkk -----END PGP SIGNATURE-----
--- End Message ---
