• 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

    Command

    Commands that the client sends to the bridge.

    Each client is expected to send discrete commands that will be processed individually.

    The command format is identical to the message format, and is meant to be very easy for the client to generate. Clients should typically flush the stream after printing their command to ensure that the server gets the input.

    The type of the command governs how the server should send the result back to the client. The currently supported command types are:

    • LISP -- send only the first return value, and just use prin1 to encode it.
    • LISP_MV -- send all of the return values, essentially by doing prin1 on the multiple-value-list of the result.
    • JSON -- send the json-encoding of the first return value. Note that this encoder only handles good ACL2 objects.
    • JSON_MV -- send the json-encoding of the multiple-value-list of the result. Note that this encoder only handles good ACL2 objects.

    Adding other types would be trivial. For instance, it might be useful to add pretty-printing.