1

Centaur ACL2-Bridge へのバインディングを作成しようとしています。これまでのところ、次のシーケンスでブリッジを開始できます。

  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)

ご協力いただきありがとうございます！

4

2 に答える 2

0

ありがとう -- 私は ACL2 ブリッジの作成者ですが、あなたの質問と回答を見るまで、このバグがあることに気づきませんでした。これは簡単に修正できるはずなので、開発版で修正します。

于 2014-09-07T19:20:50.100 に答える