Plugins

A plugin adds to the app:

tools that compute;
Python libraries for your scripts;
Lean libraries for your Lean.

Install one from the Plugins panel, or add your own from a folder.

The catalogue

Only licences free for any use.

Tools: SymPy and SciPy. Each answer comes with a Lean file that checks it.
Python: NetworkX, pandas, scikit-learn, statsmodels, Bokeh, CVXPY and more.
Lean: CSLib, LeanCert, CompPoly, Velvet, Physlib, StatLib, Foundation, GameTheory.

Turn a plugin off to pause it. Uninstall removes it.

Your own plugin

A plugin is a folder with roomtoprove-plugin.json:

JSON

{
  "id": "org.example.my-plugin",
  "name": "My plugin",
  "version": "0.1.0",
  "licence": "MIT",
  "description": "What it does, in one sentence.",
  "tools": {
    "command": ["python3", "server.py"],
    "runtime": { "python": ">=3.10", "requires": ["sympy>=1.13"] }
  }
}

Choose From a folder… to add it. Any licence is fine for your own.

Tools

A tool runs apart from the app, with no network. It speaks the Model Context Protocol: JSON lines over standard input and output.

An answer can carry:

Field	Means
`answer`	the result
`tex`	how it reads, in TeX
`lean`	a Lean file that proves it
`checks`	what that file checks
`unchecked`	what it does not

The app says checked by Lean only when the file has no error and no sorry.

Python libraries

JSON

{ "id": "org.example.graphs", "name": "Graphs", "version": "1.0.0",
  "licence": "BSD-3-Clause", "python": { "packages": ["networkx"] } }

Each package is checked before it is kept.

Lean libraries

Your own library can stay private, in a folder of the plugin:

JSON

{ "id": "org.example.my-lean", "name": "My Lean library", "version": "0.1.0",
  "licence": "LicenseRef-Private",
  "lean": [{ "name": "MyLib", "path": "MyLib", "modules": ["MyLib"] }] }

A public one names its git address and version instead.

The app builds it once, in the sandbox.
A small library takes seconds. CSLib takes about a minute.
Then your drafts can import it.