Separate compilation automatically benefits multi-core by processing several files at once (make -j 2)
Parsing proof scripts --- challenges!
What is the point?
Answer: used for indentation, folding/outlining, also semantic information for undo
It marks up document as spans, so tells end points for sending commands
Can attach additional meta information either during the parse or during execution
Manage state of metainformation alongside state of elements
Need to outdate meta info appropriately as well, of course
Xavier Leroy: one of the best things he did was to implement separate compilation in OCaml
Message model --- needs discussion
Potentially unlimited amount of output for a single command
Notes about skipping proofs:
Pierre Courbineu's declarative mode for Coq allows to pass over incomplete places in proofs and issues a warining that gets shown in yellow by the interface
We could implement this in the broker by skipping or backing out in case of errors