Search code examples
acl2

ACL2 Bridge worker thread throws undefined function exception


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!


Solution

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