acl2 - ACL2 Bridge 工作线程抛出未定义函数异常

Question

我正在尝试编写与 Centaur ACL2-Bridge 的绑定。到目前为止，我可以按照以下顺序启动桥接：

现在，发送命令会产生错误：

Bridge: bridge-worker-1: Uncaught error in worker thread: 
  Undefined function ACL2::HL-HSPACE-INIT called with arguments () .

也许这是一个编译错误，或者是系统中的一个错误，我还不确定。 acl2 --version产量Version 1.10-dev-r16020M-trunk (DarwinX8664)

谢谢你的帮助！

score 2 · Accepted Answer

2

事实证明，您必须在 ACL2(h) 扩展中运行 bridge 才能获得预期的行为。

于 2014-02-21T19:02:41.123 回答

score 0 · Accepted Answer

谢谢——我是 ACL2 桥的作者，直到我看到你的问题和答案，我才意识到它有这个错误。应该很容易解决这个问题，我将在开发版本中这样做。

2 回答 2