Distracting quicklisp warnings

[MattKaufmann]

I think this has cdoame up before, but I can't
remember what was said and I think this deserves
to be a GitHub Issue. Recently an ACL2 user asked
me about this, and in general, such warnings are a
distraction.

Certification of some of the quicklisp books, at
least using CCL (I don't think I've seen this
using SBCL), produces warnings like the following
(this one is taken from
books/centaur/4v-sexpr/sexpr-purebool-p.cert.out).
Note: This is a very long line!

; Warning: System definition file #P"/v/filer4b/v11q002/acl2space/acl2/acl2/books/quicklisp/bundle/software/cl-fad-0.7.4/cl-fad.asd" contains definition for system "cl-fad-test". Please only define "cl-fad" and secondary systems with a name starting with "cl-fad/" (e.g. "cl-fad/test") in that file.

Can someone eliminate these warnings, please?

[ragerdl]

Might be worth updating our quicklisp files and seeing if we still get these warnings.

[MattKaufmann]

Regarding: Might be worth updating our quicklisp files and seeing if we still get these warnings. Is it obvious to a quicklisp-literate person how to do such updates? I did a very quick scan of :doc quicklisp and I didn't see anything obvious about how merely to do an update. "David L. Rager" <notifications@github.com> writes:

…

[1:text/plain Hide] Might be worth updating our quicklisp files and seeing if we still get these warnings. -- You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub: #861 (comment) [2:text/html Show]

[ragerdl]

FWIW, I put some directions on the wiki here:

https://github.com/acl2/acl2/wiki/How-to-update-quicklisp

Which I think is just a rehash of the heading "Adding Quicklisp Libraries" at:

http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____QUICKLISP

Regarding difficulty, I don't think there was much to it. It took a while because one has to build the books. And, I seem to recall doing a thing or two that was off-script in order to deal with errors that cropped up. IIRC, the fixes were relatively intuitive from that update.sh script (somewhere in the quicklisp directory).

[MattKaufmann]

Thanks, David; that wiki page looks great. In my opinion, it would be best to have everything that's helpful for the ACL2 books in the :doc, rather than on a wiki page (which people might not think to consult, and which could disappear the next time we move to the latest fad in version control systems ;). I'd be happy simply to copy that page into a new section of :doc quicklisp entitled, say, "Updating Quicklisp without Adding New Libraries". Shall I do that? I might change "start from a clean git slate" to "Make sure that your git repository is up to date". Thanks -- -- Matt "David L. Rager" <notifications@github.com> writes:

…

[1:text/plain Hide] FWIW, I put some directions on the wiki here: https://github.com/acl2/acl2/wiki/How-to-update-quicklisp Which I think is just a rehash of the heading "Adding Quicklisp Libraries" at: http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____QUICKLISP Regarding difficulty, I don't think there was much to it. It took a while because one has to build the books. And, I seem to recall doing a thing or two that was off-script in order to deal with errors that cropped up. IIRC, the fixes were relatively intuitive from that update.sh script (somewhere in the quicklisp directory). -- You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub: #861 (comment) [2:text/html Show]

[ragerdl]

Hi Matt,

Yeah, I definitely agree that the right place for these things is in the :doc topics. Thanks~

BTW, "start from a clean slate" is a slightly ambiguous version of "make a fresh git clone." And indeed, due to commands in that update-libs.sh script (maybe "git add *" calls... I forget), imo it's best to start with a fresh git clone and not just "make sure that the repo is up to date."

Thanks,
David

[MattKaufmann]

Thanks, David. I'll update :doc quicklisp accordingly sometime in the next several days unless someone stops me first.

…

-- Matt "David L. Rager" <notifications@github.com> writes:

[1:text/plain Hide] Hi Matt, Yeah, I definitely agree that the right place for these things is in the :doc topics. Thanks~ BTW, "start from a clean slate" is a slightly ambiguous version of "make a fresh git clone." And indeed, due to commands in that update-libs.sh script (maybe "git add *" calls... I forget), imo it's best to start with a fresh git clone and not just "make sure that the repo is up to date." Thanks, David -- You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub: #861 (comment) [2:text/html Show]

[MattKaufmann]

I thought I'd try Sol's instructions. So I cloned acl2 and then, in
books/quicklisp, this happened.

% ./update-libs.sh
Defaulting LISP to ccl
Defaulting STARTJOB to bash
Rebuilding Quicklisp Bundle
./update-libs.sh: 1: cd: can't cd to ../../build
%

Probably I'm not the one to be doing this, since I know nothing about
quicklisp. But I don't think :doc quicklisp is just a rehash of Sol's
instructions, and also, Sol's instructions mention update.sh but now
it's presumably update-libs.sh.

I hope someone will sort this out; that's very unlikely to be me.

[ragerdl]

Somehow my change to update-libs.sh didn't make it in last time. Basically, one "../" needs to be removed from that cd call. Working on this.

[MattKaufmann]

Thanks, David! I apologize for not noticing Issue #813; I guess this is really the same issue.

[ragerdl]

Ran out of memory too much to get this done this weekend. Hope to look into it again soon but reviewing papers is probably higher priority.

[ragerdl]

No idea whether the warnings are now fixed, but I did finally update quicklisp.

[acoglio]

Is this Issue still relevant/applicable?

[MattKaufmann]

It's still relevant. I don't know if it happens in other than CCL, but I'm still seeing it with CCL on Linux and Mac. Here's an example of Mac.

~/acl2/acl2-git-scratch$ time fgrep --include='*.cert.out' -ri 'System definition file' .
./books/centaur/misc/tshell-tests.cert.out:; Warning: System definition file #P"/Users/kaufmann/acl2/acl2-git-scratch/books/quicklisp/bundle/software/cl-fad-20200610-git/cl-fad.asd" contains definition for system "cl-fad-test". Please only define "cl-fad" and secondary systems with a name starting with "cl-fad/" (e.g. "cl-fad/test") in that file.
[... and lots more]

Here's evidence for "and lots more" (not an exact count, because that regression isn't quite finished):

~/acl2/acl2-git-scratch/books$ fgrep --include='*.cert.out' -ri 'System definition file' . | wc -l
     229
~/acl2/acl2-git-scratch/books$