• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Std/io
    • Oslib
    • Bridge
      • Json-encoding
      • Security
      • Command
      • In-main-thread
      • Message
      • Start
      • Bindings
      • Stop
      • Try-in-main-thread
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bridge

Start

Start an ACL2 Bridge server.

Warning: don't even think about starting an ACL2 Bridge until you have read about security.

Unix Domain Socket Examples (recommended):

(bridge::start "./my-socket")
(bridge::start "/tmp/my-socket")

TCP/IP Socket Examples (very scary -- see security!!!):

(bridge::start nil)     ;; Listen on TCP/IP port 55432
(bridge::start 12345)   ;; Listen on TCP/IP port 12345

Additional keyword options:

• :stack-size -- stack size for worker threads (in bytes)
• :tstack-size -- temporary stack size for worker threads (in bytes)
• :vstack-size -- value stack size for worker threads (in bytes)

Definitions and Theorems

Function: start-fn

(defun start-fn
    (socket-name-or-port-number stack-size tstack-size vstack-size)
 (declare (xargs :guard t)
          (ignorable socket-name-or-port-number
                     stack-size tstack-size vstack-size))
 (cw
  "Under-the-hood definition of bridge::start-fn not installed?~%"))