Modules

A module is a folder of files plus a short manifest. Templates, skills and assistants are all modules; the word you see depends on what the folder holds.

One shape, three words

Every workspace starts empty. Modules put things in it: a paper in a venue's style, a search skill, a verifier that checks claims when you select them. Underneath, all of these are the same object. The name the gallery shows is decided by what the module contains.

You see	What the module holds	Example
`Template`	Documents and style files, no trigger	ICML 2026, Cambridge thesis, Lean Blueprint
`Skill`	One SKILL.md, no trigger	zbMATH search, Paperclip literature
`Assistant`	A skill plus a trigger that runs it	Claim verification, Formalize, Goal loop

Everything is a file

Whatever a module adds to a workspace is a file you can open, edit, or delete. Starter documents, class files, the prebuilt PDF, setup.sh, AGENTS.md, skills/<id>/SKILL.md. There is no hidden configuration that changes behaviour without a file behind it. Instructions to the agent live in AGENTS.md, one per folder, all of them read. Selected-text actions live in the frontmatter of the skill they run.

The manifest

Four sections. Nothing else.

manifest.yaml

name: Lean Blueprint
goal: Keep your paper and its Lean proof in step.

contents:               # files in this folder, and other modules
  modules: [lean4]
  open: main.tex        # what the editor opens first

on_install:             # one-time actions when the module lands
  say: "main.tex is your paper. Formalization.lean is the same math ..."
  run: bash setup.sh

needs:                  # what the sandbox must already have
  - lean4

triggers:               # present only on assistants
  - on: select
    label: Formalize
    skill: lean-blueprint
    prompt: Formalize only the selected statement ...

contents is the folder itself plus any modules it includes. on_install runs once: an opening message in chat, a setup command, a repository to clone. needs names ground the module relies on. triggers turns a module into an assistant.

Triggers

A skill says how. A trigger says when. Each trigger starts a chat with the skill loaded and the settings it names.

Trigger	Fires when	Used by
`ask`	You mention it in chat. The default for every skill.	Every skill
`select`	You select text and click the button.	Claim verification, Formalize
`compile`	A LaTeX or Lean compile fails.	Compilation
`change`	A watched file changes, such as a theorem statement.	Autoformalization
`schedule`	A cron time arrives.	Weekly review
`chain`	The previous chat ends, so the next one starts.	Goal loop

Triggered chats are tagged with the assistant that started them, so you can see what each one did and cost, and switch it off. Assistants that play a supporting role post their findings as suggestions and comments on the document, not as chat.

Modules of modules

A module can include other modules. A math setup is a template that includes Lean 4, the claim-verification assistant, the autoformalization assistant and the compilation assistant. Someone writing a biology paper takes claim verification alone. Included modules land in their own folders; the including module owns the root. Two levels are shown in the UI, any depth is allowed in the data.

The ground

Some things are not files in the workspace: Python, Node, Lean 4 and Mathlib in the sandbox, the TeX Live worker that compiles LaTeX. This is the ground. Every sandbox has it. A module declares what ground it needs; the sandbox image bakes it in or the module's setup.sh installs it on first use. Nothing to remove, because nothing lives in your files.

Add, remove, edit

Add copies the module's files in, records which module brought each one, runs on_install, and registers its triggers. Add from the gallery to start a workspace.

Remove deletes the files the module brought and unregisters its triggers. A file you edited since is kept and you are asked. Swapping venues is remove ICML, add NeurIPS: the style files change, your main.tex stays.

Edit is editing files. Change the prompt in a skill, the cron in a schedule, the protocol in a loop. The module in the catalog is a copy; yours is yours.

Worked examples

Module	Contents	On install	Needs	Triggers
`ICML 2026`	main.tex, references.bib, main.pdf, the icml-2026 style module	opening message	TeX Live	none
`zbMATH search`	skills/zbmath/SKILL.md	none	none	ask
`Claim verification`	skills/claim-verification/SKILL.md	none	none	select
`Lean Blueprint`	main.tex, Formalization.lean, status.md, blueprint.sty, one skill, the lean4 module	message, bash setup.sh	Lean 4	select (Formalize)
`Goal loop`	AGENTS.md (locked), goal.md, tasks.md, attempts.md	set cheap model	none	chain, schedule fallback

Browse every module in the gallery; one click opens a workspace with it inside. Selected-text triggers, skills and templates work as described; compile, change and chain triggers, and remove with ownership, are in progress.