ACL2 Bridge worker thread throws undefined function exception

Question

I'm trying to write a binding to the Centaur ACL2-Bridge. So far, I can start the bridge with the following sequence:

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

Having that now, sending a command over produces the error:

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

Perhaps this is a compilation error, or a bug in the system, I'm not yet sure. acl2 --version yields Version 1.10-dev-r16020M-trunk (DarwinX8664)

Thanks for your help!

Answer 1

It turns out you have to run bridge in the ACL2(h) extension to get the expected behavior.

Answer 2

Thanks -- I'm the author of the ACL2 bridge, and I did not realize that it had this bug until I saw your question and answer. It should be easy to fix this, and I'll do so in the development version.