• 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

    Message

    Messages that the bridge sends to the client program.

    We send all output to the client in discrete messages. The message format is very simple. It is easy for a client to reliably parse, and doesn't require us to think about character encoding. Informally, the format is:

    type len[newline]
    contents[newline]

    To make this extremely clear: we first print the type, then a space, then the len, then a newline character, then the contents, then another newline character.

    The type here is a label that describes what kind of message this is. It matches [A-Z][A-Z0-9_]*. That is, it starts with an uppercase alphabetic character, and then contains only uppercase alphabetic, numeric, and underscore characters.

    The len says how many characters are in contents. It matches [0-9]+, i.e., it is a base-10 natural number.