Crate agda_mode

Accessing Agda’s interaction mode via command line. This library is created for agda-tac. It works with stable rust starting from 1.39.0.

This crate will work only with master-branch Agda until Agda 2.6.1 is released. Tracking issues for the feature are agda#4183 and agda#4209, both work for JSON now.

Basic usage

Invoke ReplState::start and await the REPL to be available. That’s the wrapper of the Agda REPL’s state.

Then you may:

• Invoke ReplState::reload_file to reload the current file
• Invoke ReplState::command to send a command to Agda
• Invoke ReplState::response to await for the next response from Agda.
  • Note that Agda sends json to agda-mode. The deserialized json type is Resp.

There are more utilities to access Agda, checkout the library documentation to see all of them.

Implementation notes

This crate deserialize json via serde_json, and do async process io handling via tokio.

Modules

• agda
  Invoke Agda in command line and interact with it via stdio.
• base
  Common types (used in both input/output to Agda).
• cmd
  Agda commands (input to Agda).
• debug
  Debugging utilities.
• hs
  Haskell interaction utilities.
• pos
  Position types, used in both resp & cmd.
• resp
  Response data types (output of Agda).