The PISA protocol

PISA supports communication over gRPC. Once the server is hosted, it can be communicated with the following protocol:

(Words starting with $ are not literal syntax, but variables)

• Parse the current file.
  • Input: "PISA extract data"
  • Output: The parsed file in the following format

  "${STATE_STRING_1}<\STATESEP>${STEP_STRING_1}<\STATESEP>${PROOF_LEVEL_1}<\TRANSEP>..."

• Parse a certain piece of proof text.
  • Input: "\<parse text\> $text"
  • Output: The parsed text in the following format

  "${STEP_STRING_1}\<SEP\>${STEP_STRING_2}\<SEP\>${STEP_STRING_3}\<SEP\>..."

• Get all the possible definitions of the theorem with the given name, for the top level state “default” (requires initialisation).
  • Input: "\<get all definitions\> ${theorem_name}"
  • Output: Every single line is a possible definition of the theorem