Plugin breaks on Coq 8.19 rather than report protocol error
I recently upgraded to Coq 8.19 for a project, and when trying to use the plugin I expected to get a standard protocol error due to the bump in protocol version. (This Coq version also comes with some optional additional XML info, see here.)
Instead, I found that the plugin simply succeeded on startup after exchanging some messages with the Coq server, and then broke when I tried to use it, with the following error:
Error detected while processing function 320[13]..function 320[3]..302:
line 8:
E716: Key not present in Dictionary: "zones"
Adding the protocol version to the list of supported versions fixes the above error and allows the plugin to work normally.
Here's an example log with g:coq_debug = 'xermj'
:
j|start | coqidetop -main-channel stdfds -async-proofs on -Q <files>
j|started | process 3009 run channel 0 open
r|call | about
x|send | <call val="About"><unit/></call>
j|send | Vim(call):E631: ch_sendraw(): Write failed
j|failed |
j|start | coqidetop.opt -main-channel stdfds -async-proofs on -Q <files>
j|started | process 3010 run channel 1 open
r|call | about
x|send | <call val="About"><unit/></call>
x|recv | <value val="good"><coq_info><string>8.19.0</string><string>20230413</string><string>n/a</string><string>n/a</string></coq_info></value>
x|item | ['value', {'val': 'good'}, ['coq_info', {}, ['string', {}, '8.19.0'], ['string', {}, '20230413'], ['string', {}, 'n/a'], ['string', {}, 'n/a']]]
m|message | {'type': 'good', 'content': [['coq_info', {}, ['string', {}, '8.19.0'], ['string', {}, '20230413'], ['string', {}, 'n/a'], ['string', {}, 'n/a']]]}
r|good | {'version': '8.19.0', 'release': 'n/a', 'protocol': '20230413', 'success': 1, 'compile': 'n/a'}
x|recv | <feedback object="state" route="0"><state_id val="1"/><feedback_content val="workerstatus"><pair><string>proof:0:0</string><string>Idle</string></pair></feedback_content></feedback>
x|item | ['feedback', {'route': '0', 'object': 'state'}, ['state_id', {'val': '1'}], ['feedback_content', {'val': 'workerstatus'}, ['pair', {}, ['string', {}, 'proof:0:0'], ['string', {}, 'Idle']]]]
m|message | {'kind': 'workerstatus', 'type': 'feedback', 'state_id': '1', 'content': [['pair', {}, ['string', {}, 'proof:0:0'], ['string', {}, 'Idle']]]}