What is the edit_id or editId in the XML protocol?

Developing the Rocq Prover
1

Hi all, I am looking into the coqidetop xml protocol and find the editId in the Add command quite confusing. Does anyone knows the intended meaning and how should XML protocol clients handle this id?

FYI, an Add command is a record of type:

Add(command: string, editId: integer, stateId: integer, verbose: boolean, bp: integer, line_nb: integer, bol_pos: integer)

I know that Coqtail is build on top of the XML protocol so I read its source code to understand the intended meaning and usage. However, I found the following comments in xmlInterface.py, clearly showing that the plugin author did not have any idea on it neither :stuck_out_tongue:
It seems clients do not have to take care of edit id.

    # Overrides add() from 8.5
    def add(
        self,
        cmd: str,
        state: int,
        encoding: str = "utf-8",
    ) -> Tuple[str, Optional[bytes]]:
        """Create an XML string to advance Coqtop.
        Args:
          cmd: string - The command to evaluate
          edit_id: int - The current edit id ?
          state_id: CoqStateId - The current state id
          verbose: bool - Verbose output
          bp: int - Byte offset of phrase in script
          line_nb: int - Line number of phrase in script
          bol_pos: int - Byte offset for beginning of line
        """
2

edit_id is no longer used and hasn’t been for several years. Removing the field from the XML message is tricky–all clients would have to change at once OR the protocol would have to support both old and new message formats for a while (not easy with the current design). Clients can pass any integer for this field.

The server code that processes this message is here. Observe that eid isn’t referenced.

Documentation for the protocol is here. It may not be entirely complete or accurate in all the details.