HoTT-coq XML forest parse error

[aa755]

Queries like Print/ SearchAbout
do not output an XML tree, but a forest.
This violates one of the assumptions XML parser library.

Soln: artificially add a root node before sending it off to the parser

[aa755]

Because there is little documentation of the protocol in the newer versions of Coq 8.4, snooping on Coqide/coqtop interaction seems to be the only option. The following command is a good start:

sudo strace -ff -e trace=read -e read=1,2 -p COQTOP_PID -s 10000 > log.txt

then grep "read(0" log.txt. Here is a snippet:

Process 11196 attached
read(0, "<call val="rewind" steps="1"/>", 65536) = 30
read(0, "<call val="setoptions">PrintingCoercions<option_value val="boolvalue"><bool val="false"/></option_value>PrintingNotations<option_value val="boolvalue"><bool val="true"/></option_value>PrintingExistentialInstances<option_value val="boolvalue"><bool val="false"/></option_value>PrintingMatchingSynth<option_value val="boolvalue"><bool val="true"/></option_value>PrintingImplicit<option_value val="boolvalue"><bool val="false"/></option_value>PrintingAll<option_value val="boolvalue"><bool val="false"/></option_value>PrintingUniverses<option_value val="boolvalue"><bool val="false"/></option_value>", 65536) = 1057
read(0, "<call val="goal"/>", 65536) = 18
read(0, "<call val="setoptions">PrintingCoercions<option_value val="boolvalue"><bool val="false"/></option_value>PrintingNotations<option_value val="boolvalue"><bool val="true"/></option_value>PrintingExistentialInstances<option_value val="boolvalue"><bool val="false"/></option_value>PrintingMatchingSynth<option_value val="boolvalue"><bool val="true"/></option_value>PrintingImplicit<option_value val="boolvalue"><bool val="false"/></option_value>PrintingAll<option_value val="boolvalue"><bool val="false"/></option_value>PrintingUniverses<option_value val="boolvalue"><bool val="false"/></option_value>", 65536) = 1057
read(0, "<call val="evars"/>", 65536) = 19
read(0, "<call val="hints"/>", 65536) = 19
read(0, "<call val="status"/>", 65536) = 20
read(0, "<call val="interp" id="0" verbose="">Require Import String.", 65536) = 66
read(0, "<call val="setoptions">PrintingCoercions<option_value val="boolvalue"><bool val="false"/></option_value>PrintingNotations<option_value val="boolvalue"><bool val="true"/></option_value>PrintingExistentialInstances<option_value val="boolvalue"><bool val="false"/></option_value>PrintingMatchingSynth<option_value val="boolvalue"><bool val="true"/></option_value>PrintingImplicit<option_value val="boolvalue"><bool val="false"/></option_value>PrintingAll<option_value val="boolvalue"><bool val="false"/></option_value>PrintingUniverses<option_value val="boolvalue"><bool val="false"/></option_value>", 65536) = 1057
read(0, "<call val="goal"/>", 65536) = 18
read(0, "<call val="setoptions">PrintingCoercions<option_value val="boolvalue"><bool val="false"/></option_value>PrintingNotations<option_value val="boolvalue"><bool val="true"/></option_value>PrintingExistentialInstances<option_value val="boolvalue"><bool val="false"/></option_value>PrintingMatchingSynth<option_value val="boolvalue"><bool val="true"/></option_value>PrintingImplicit<option_value val="boolvalue"><bool val="false"/></option_value>PrintingAll<option_value val="boolvalue"><bool val="false"/></option_value>PrintingUniverses<option_value val="boolvalue"><bool val="false"/></option_value>", 65536) = 1057
read(0, "<call val="evars"/>", 65536) = 19
read(0, "<call val="hints"/>", 65536) = 19
read(0, "<call val="status"/>", 65536) = 20
read(0, Process 11196 detached

Similarly, change read to write in the strace command to get the responses of coqtop to coqide.