regression failure

0 views
Skip to first unread message

David M Russinoff

unread,
Dec 7, 2025, 9:01:42 PM (2 days ago) Dec 7
to acl2-...@googlegroups.com
I tried to make regression and got this:

make[1]: *** No rule to make target `projects/rac/examples/imul/imul.lisp', needed by `projects/rac/examples/imul/imul.cert'.

There is no imlu.lisp.  I don't understand why it wants to make imul.cert.  How can I tell it not to do that?

Matt Kaufmann

unread,
Dec 7, 2025, 10:43:26 PM (2 days ago) Dec 7
to acl2-...@googlegroups.com
The latest ACL2 on github does seem to include that file:

cyan:/projects/acl2/acl2% ls -l books/projects/rac/examples/imul/imul.lisp
-rw-rw-r-- 1 kaufmann acl2 7089 Mar 10 2019 books/projects/rac/examples/imul/imul.lisp
cyan:/projects/acl2/acl2%

So I don't know what to suggest. Perhaps it would be simplest for you
to clone a fresh ACL2 distribution and try again.

On the other hand, if you've deliberately deleted that book, then
perhaps the problem is that some other book still includes it.

-- Matt
David M Russinoff <druss...@gmail.com> writes:

> [1:text/plain Hide]
> --
> --
> ACL2-books help:
> To post new messages: acl2-...@googlegroups.com
> To unsubscribe: acl2-books-...@googlegroups.com
> More options: http://groups.google.com/group/acl2-books?hl=en
>
> ---
> You received this message because you are subscribed to the Google Groups "acl2-books" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/acl2-books/CA%2BQYs9EWvadBHarBmNJS%3DpsY4%2Bz%2BGhEw8y0N3qx3E%3D1EtQNS-A%40mail.gmail.com.
>
> [2:text/html Show Save:noname (3kB)]
Reply all
Reply to author
Forward
0 new messages