Agda Mode Telemetry

Idea: record how Agda proofs actually get written.

Every command you run, every response Agda sends back, and the state of the buffer after each step, saved to a SQLite database next to your Agda file as you work. The extension sits alongside agda-mode and writes the same format as its Emacs sibling, agda-mode-telemetry. Sessions from either editor replay with the same tools.

Quick start

1. Install Agda and this extension (agda-mode comes with it):

   code --install-extension kiranandcode.agda-mode-telemetry
   

2. Open an .agda file and load it with C-c C-l.

That's it. Agda telemetry in the status bar means the session is being recorded to .agda-telemetry.db in the same directory.

Features

• Records as you prove: C-c C-l, C-c C-c, C-c C-SPC, C-c C-r, …

• Share a session as Markdown. Click Agda telemetry in the status bar, then Copy session trace.

• Export everything as a zip. Agda Telemetry: Export Telemetry… bundles a consistent copy of every database in the workspace, ready to send to whoever is collecting them.

• Replay with the Emacs tools. telemetry-replay.py and telemetry-extract.py from agda-mode-telemetry read the databases as they are.

• Pause and resume from the same menu, or set "agdaTelemetry.enabled": false.

What gets recorded

Three tables in .agda-telemetry.db. The full schema is in the Emacs README.

Snapshots are your code. Nothing leaves your machine unless you export or copy it.

Installation

Needs VS Code 1.101 or later, which ships the node:sqlite the extension writes with. There are no native modules to build.

Differences from Emacs

The extension listens on the log channel agda-mode exports (exports.channels.log) and does what agda2-telemetry.el does with advice. Commands are logged under the name of the agda2-mode command that does the same thing, and responses under the Emacs handler they come from. Three things differ:

• responses.args_text is JSON, not an s-expression, since VS Code only sees responses after agda-mode has parsed them. For example, agda2-give-action is [0,"GiveNoParen"].
• agda-mode reports a response once its handler has finished, so a response whose handler runs a command comes after that command's responses. After a case split, agda2-make-case-action follows the reload's responses. Emacs logs it first.
• col counts characters, where Emacs counts display width.

Development

npm install
npm run build         # dist/extension.js
npm run test:unit     # mapping, formats, zip, traces
npm run test:e2e      # real VS Code + agda-mode + agda; needs agda on PATH
npm run package       # agda-mode-telemetry-<version>.vsix

To release, run npm version patch && git push --follow-tags. The release workflow attaches the .vsix to a GitHub release and publishes to the Marketplace and Open VSX. The GIFs above are recorded by the demo workflow under Xvfb with ffmpeg. Re-run it from the Actions tab after changing the UI.

Project structure