I'm trying to write a binding to the Centaur ACL2-Bridge. So far, I can start the bridge with the following sequence:
cd books
sudo acl2
acl2 !> (include-book centaur/bridge/acl2/top)
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!
It turns out you have to run bridge in the ACL2(h) extension to get the expected behavior.