API Overview

Core Methods

  • start(file, theorem): Begin a proof session

  • run(state, command): Execute tactics or commands

  • goals(state): Get current proof goals

  • premises(state): Get available premises/lemmas

Advanced Features

  • get_root_state(file): Get initial document state

  • state_equal(st1, st2, kind): Compare proof states

  • state_hash(state): Get state hash

  • toc(file): Get table of contents

  • ast(state, text): Parse command to AST (only with the dev version of coq-lsp)

  • ast_at_pos(file, line, char): Get AST at file position (only with the dev version of coq-lsp)

  • get_state_at_pos(file, line, char): Get proof state at position (only with the dev version of coq-lsp)

Working with Feedback

All commands return states with feedback containing Rocq messages:

state = client.run(state, "Search nat.")
for level, message in state.feedback:
    print(f"Level {level}: {message}")