ACL2橋工作線程拋出未定義的函數異常

Question

我想寫一個綁定到Centaur ACL2橋。到目前爲止，我可以先從以下順序橋：

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橋的作者，我沒有意識到它有這個錯誤，直到我看到你的問題和答案。解決這個問題應該很容易，我會在開發版本中這樣做。