ACL2桥工作线程抛出未定义的函数异常

Question

我正在尝试写一个绑定到半人马座ACL2 2-桥。到目前为止，我可以从以下顺序开始这座桥：

1. cd books
2. sudo acl2
3. acl2 !> (include-book centaur/bridge/acl2/top)
4. acl2 !> (bridge::start "Users/Brian/Desktop/acl2server")

现在，在上面发送一个命令会产生错误：

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)

谢谢你的帮忙!

Answer 1

结果是，您必须在ACL2(h)扩展中运行桥才能获得预期的行为。

Answer 2

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