0

在 ACL2 书籍目录中，每当我尝试构建或清理书籍时，都会收到一条错误消息，如下所示：

GNUmakefile:299: *** Books Sanity Check Failed. Stop.

如何避免此错误消息？

4

1 回答 1

0

发生此错误是因为 makefile 现在检查 acl2 make 是否认为您正在使用的目录与您当前所在的目录相同。解决方案是告诉 make 使用当前目录中的 acl2。您可以通过传入 ACL2 作为 make 的参数来实现这一点，例如：

make ACL2=~/sw/acl2-extra/saved_acl2 clean

于 2015-08-11T19:34:46.137 回答