问题标签 [acl2]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
perl - 构建 ACL2 书籍时，如何摆脱有关“幻数...”的错误
为 ACL2 构建书籍时，出现以下错误。我该如何摆脱它？
sbcl - 在 SBCL 上编译 ACL2 时，如何避免低级调试器崩溃？
在 SBCL 上编译 ACL2 时，如何避免低级调试器崩溃？这是我在 Linux 上使用 SBCL 1.2.3 编译时收到的错误消息：
acl2 - 了解标签错误
我正在尝试理解错误消息，以便我可以考虑修复它。解决以下错误的正确方法是什么？我应该去添加:oslib, :quicklisp, 和:quicklisp.osicat里面的包含书籍books/oslib/rmtree.lisp吗？我的包含书表格错了吗？
indexing - ACL2 中的排序映射
我必须在 ACL2 中使用排序的映射/索引结构。目前我有以下内容：
有没有其他方法可以更有效地做到这一点？
acl2 - 为什么 cert.pl 抱怨 ttags
在认证 ACL2 书籍时，我经常收到以下错误消息：
怎么了？
acl2 - 使用 ACL2 撤消 emacs 中的只读区域
在使用 ACL2 时，我在 emacs 中遇到了一些奇怪的击键咒语，我的缓冲区中的一个区域变成了只读的。什么会导致这种情况？如何取消将区域标记为只读？
acl2 - 确定当前正在通过 ACL2 认证的书籍
如何查看给定机器上当前正在通过 ACL2 认证的书籍？我知道我可以查看输出并弄清楚这一点，但这需要付出不小的努力。
acl2 - ACL2 退出代码 137 是什么意思？
ACL2 退出代码 137 是什么意思？输出如下所示：
acl2 - 如何跟踪 ACL2 重写器？
如何跟踪 ACL2 重写器？我真的很想知道证明者内部发生了什么。寻找此类信息是可取的，还是我应该遵循“方法”？
acl2 - 如何修复 ACL2 书籍健全性检查失败？
在 ACL2 书籍目录中，每当我尝试构建或清理书籍时，都会收到一条错误消息，如下所示：
GNUmakefile:299: *** Books Sanity Check Failed. Stop.
如何避免此错误消息？