ari — a nicer workflow for Harmonic's Aristotle

ari wraps the official aristotle CLI (aristotlelib) with the workflow we actually want when pointing Aristotle at a Lean project:

• Clean uploads. ari submit stages a gitignore-aware copy of the project (tracked + untracked-non-ignored files) and hard-excludes .git/, .lake/, lake-packages/ — so you never ship gigabytes of build artifacts.
• Your work and Aristotle's work never mix. If the project is a git repo and dirty, ari commits your work first (checkpoint before Aristotle run). When results come back, they are applied and committed as-is in their own commit, with Aristotle credited per Harmonic's convention: Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>.
• Results as a diff, not a tarball. ari pull downloads the result archive, extracts it, applies adds/updates onto your project (never deletes), and shows you the diff — like the Aristotle web UI does. Aristotle's boilerplate (README.md citation blurb, lake-manifest.json from its server-side build) is skipped whenever your project already has its own.
• No lost jobs. Submission never uses --wait (its long-lived stream drops on long proof searches). ari watch polls show instead; ctrl-c is always safe, the job keeps running server-side.
• No id juggling. The last project id is remembered in <project>/.aristotle/state.json (kept out of git via .git/info/exclude), so ari status, ari watch, ari pull, ari continue need no arguments.

Install

uv tool install --from /home/leo/devel/aristotle-cli ari   # or: uv tool install -e .
export ARISTOTLE_API_KEY=...

Requires the real aristotle CLI on PATH (uv tool install aristotlelib), or point ARI_ARISTOTLE_BIN at it.

Usage

cd my-lean-project

# fire and forget
ari submit "Prove theorem Foo.bar in Src/Foo.lean by replacing its sorry"
ari status                # wraps `aristotle show` with the remembered id
ari watch --pull          # poll until done, then apply + diff + commit

# or in one shot
ari submit --prompt-file task.txt --watch

# follow-ups on the same server-side project
ari continue "Also prove Foo.baz" --watch
ari continue --mode ask "Why did you introduce lemma helper_aux?" --watch

# inspect without committing
ari pull --no-commit      # applies + stages + shows diff, leaves it uncommitted

ari list                  # your projects, newest first
ari tasks                 # tasks in the current project
ari cancel                # cancel the running task

The result archive is kept at .aristotle/downloads/<project-id>.tar.gz for inspection.

What a result commit looks like

aristotle: Prove theorem Foo.bar in Src/Foo.lean by replacing its sorry

Aristotle project: 8b1f4e2a-…

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>

Follow-up fixes of your own go in separate commits — the Aristotle commit is always exactly what the server returned.

Development

uv sync
uv run pytest            # unit + offline e2e against tests/fake_aristotle.py