STM - siegebell/vscoq GitHub Wiki

Sentences: each command sent to CoqTop is a "sentence"; they are typically terminated by ".\s" (followed by whitespace or EOF). Examples: "Lemma a: True.", "(* asdf *) Qed.", "auto; reflexivity." In practice, the command sentences sent to CoqTop are terminated at the "." and start with any previous whitespace. Each sentence is assigned a unique stateId after being sent to Coq (via Add). States:

• Processing: has been received by Coq and has no obvious syntax error (that would prevent future parsing)
• Processed:
• InProgress:
• Incomplete: the validity of the sentence cannot be checked due to a prior error
• Complete:
• Error: the sentence has an error error

State ID 0 is reserved as 'null' or 'default' state. (The 'query' command suggests that it might also refer to the currently-focused state, but I have not tested this yet). The first command should be added to state ID 0. Queries are typically performed w.r.t. state ID 0.