Skip to content

Commit e232ef5

Browse files
SimonSchubertSimonSchubert
committed
Add commands
1 parent 3e24dd4 commit e232ef5

3 files changed

Lines changed: 244 additions & 0 deletions

File tree

‎assets/commands/algebruh.md‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
# TAGLINE
2+
3+
Classify arithmetic equality claims with independent proof checkers
4+
5+
# TLDR
6+
7+
**Check** whether an equality holds
8+
9+
```algebruh "[2 = 3]"```
10+
11+
**Prove** a claim from assumptions
12+
13+
```algebruh --assume "[a = c]" --assume "[c = b]" "[a = b]"```
14+
15+
**Compare** multiple interpretations (integers, reals, bit-vectors, modular)
16+
17+
```algebruh --interpret [int,real,bv8,mod:1] "[2 = 3]"```
18+
19+
**Declare** a function injective and check equality of arguments
20+
21+
```algebruh --injective [f] --assume "[f(a) = f(b)]" "[a = b]"```
22+
23+
**Run all checkers** and print a JSON report
24+
25+
```algebruh --all --json "[a = b]"```
26+
27+
**Emit** SMT-LIB and Z3 proof artifacts
28+
29+
```algebruh --emit [result] "[x + 0 = x]"```
30+
31+
**Check** which optional external solvers are available
32+
33+
```algebruh doctor```
34+
35+
# SYNOPSIS
36+
37+
**algebruh** [**--all**] [**--json**] [**--interpret** _LIST_] [**--assume** _EXPR_]... [**--injective** _NAME_]... [**--ai-command** _CMD_] [**--emit** _PREFIX_] _CLAIM_
38+
39+
**algebruh** **doctor** [**--json**]
40+
41+
# PARAMETERS
42+
43+
**--all**
44+
> Run additional checkers (cvc5, Carcara, Lean/Mathlib, Vampire, E when available), extra solver seeds, and sufficient-premise search. Prints every attempt.
45+
46+
**--json**
47+
> Print the complete report as JSON instead of human-readable text.
48+
49+
**--interpret** _LIST_
50+
> Comma-separated interpretation list. Default is integers (**int**). Values include **int**, **real**, **bv**_N_ / **sbv**_N_ (signed N-bit, N=1..256), **ubv**_N_ (unsigned), **mod:**_N_, **quot:**_N_, **equiv:**_N_, **f32**, **f64**, and **singleton**. Integer is always evaluated as a baseline.
51+
52+
**--assume** _EXPR_
53+
> Add an equality or disequality premise. May be repeated. Each assumption must contain exactly one **=**, **==**, or **!=**.
54+
55+
**--injective** _NAME_
56+
> Declare a unary function name as injective. May be repeated. Other function applications remain uninterpreted.
57+
58+
**--ai-command** _CMD_
59+
> Send the problem as JSON to _CMD_. The command's stdout must be a Lean tactic, which is accepted only after Lean kernel verification.
60+
61+
**--emit** _PREFIX_
62+
> Write SMT-LIB (**_PREFIX_.smt2**) and Z3 proof (**_PREFIX_.proof**) when a selected Z3 proof is available. Does not overwrite existing files.
63+
64+
_CLAIM_
65+
> Arithmetic equality or disequality to classify (for example **"2 = 3"** or **"a + 0 = a"**).
66+
67+
**doctor**
68+
> Report availability of optional external tools on **PATH**. Exit code 1 if any listed tool is missing. Accepts **--json**.
69+
70+
# DESCRIPTION
71+
72+
**algebruh** classifies arithmetic equality and disequality claims. Given a claim and optional assumptions, it reports whether the claim is proved, refuted, contingent, vacuous, or unknown, and can surface disagreements between independent checkers.
73+
74+
The default path links against the Z3 library and independently checks candidates with exact evaluation, equality saturation, bounded model search, and LRAT replay when applicable. With **--all**, it also tries external tools found on **PATH** (cvc5, Carcara, Lean with Mathlib, Vampire, E). External tools run under Bubblewrap and **prlimit** where available.
75+
76+
Expressions support integers, variable names, unary applications such as **f(x)**, parentheses, unary minus, **+**, **-**, **\***, **/**, **%**, **=**, **==**, and **!=**. Multiplication, division, and modulo bind tighter than addition and subtraction. Each claim or assumption must contain one equality or disequality; comparisons such as **<** and **>=** are not supported.
77+
78+
Outcome labels include **PROVED**, **REFUTED** (exit 0), **CONTINGENT**, **CONDITIONAL**, **VACUOUS**, **UNKNOWN**, **UNSAFE_AXIOM**, **CHECKER_BUG_CANDIDATE** (exit 1), and **REINTERPRETED** when a non-integer interpretation proves a claim that integers do not (exit 0). Input, sandbox, and solver errors use exit code 2.
79+
80+
Build requires Rust 1.85+, Cargo, pkg-config, and Z3 development libraries (or the project's **nix-shell**). Install by building **target/release/algebruh** and placing it on **PATH**.
81+
82+
# CAVEATS
83+
84+
Nonlinear arithmetic may return **UNKNOWN**. Division and modulo by zero follow Z3 semantics. User-defined equality is limited to modular **equiv:**_N_. Optional checkers must be installed separately; **algebruh doctor** reports what is available. **--emit** never overwrites existing artifact files.
85+
86+
# HISTORY
87+
88+
Algebruh is a Rust CLI by Sebastian Korotkiewicz for cross-checking arithmetic claims with Z3 and optional independent solvers (cvc5, Lean, and others). Distributed as source from GitHub.
89+
90+
# SEE ALSO
91+
92+
[z3](/man/z3)(1), [cargo](/man/cargo)(1)
93+
94+
# RESOURCES
95+
96+
```[Source code](https://github.com/skorotkiewicz/algebruh)```
97+
98+
<!-- verified: 2026-08-09 -->

‎assets/commands/index.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,7 @@ alacritty.md
161161
alembic.md
162162
alertmanager.md
163163
alex.md
164+
algebruh.md
164165
ali.md
165166
alias.md
166167
alien.md
@@ -8031,6 +8032,7 @@ tuned-adm.md
80318032
tuned.md
80328033
tunelp.md
80338034
tuptime.md
8035+
tura.md
80348036
turbo.md
80358037
turbostat.md
80368038
turm.md

‎assets/commands/tura.md‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
# TAGLINE
2+
3+
Open-source agent runtime harness with TUI and CLI
4+
5+
# TLDR
6+
7+
**Open** the interactive terminal UI
8+
9+
```tura```
10+
11+
**Start** the TUI with an initial prompt
12+
13+
```tura "[Inspect this repository]"```
14+
15+
**Run** a non-interactive gateway-backed prompt
16+
17+
```tura run "[Fix the failing test and verify it]"```
18+
19+
**Run** a one-shot prompt via the direct Rust CLI
20+
21+
```tura exec "[Summarize the architecture]"```
22+
23+
**List** configured LLM providers
24+
25+
```tura provider list```
26+
27+
**List** sessions
28+
29+
```tura session list --json```
30+
31+
**Resume** the latest session with a follow-up
32+
33+
```tura resume --last "[Continue and verify the fix]"```
34+
35+
# SYNOPSIS
36+
37+
**tura** [_global_options_] [_prompt_ | _command_ [_args_...]]
38+
39+
# PARAMETERS
40+
41+
**--gateway-url** _URL_
42+
> Use an explicit gateway instead of auto-starting or discovering one.
43+
44+
**--cwd** _PATH_
45+
> Workspace directory sent to the gateway. Defaults to the current directory.
46+
47+
**--initial-session** _ID_
48+
> Open the TUI on a specific session. Also read from **TURA_TUI_INITIAL_SESSION_ID**.
49+
50+
**--json**
51+
> Request JSON output where the selected command supports it.
52+
53+
**--verbose**
54+
> Print gateway request diagnostics to stderr.
55+
56+
**--plain** / **--rich**
57+
> Force plain/safe terminal rendering or rich rendering.
58+
59+
**--lang** **en**|**zh-CN**, **--language** **en**|**zh-CN**
60+
> Set CLI display language.
61+
62+
With no subcommand, **tura** opens the interactive TUI. If the first argument is not a known command, remaining text is treated as the initial TUI prompt.
63+
64+
# COMMANDS
65+
66+
**run** [_options_] _"prompt"_
67+
> Gateway-backed non-interactive prompt: create or reuse a session, stream until the turn completes, print the result. Options include **-m**/**--model**, **-a**/**--agent**, **--session**, **--output** text|json|ndjson, **--timeout**, **--stream**/**--no-stream**, **--bash**/**--zsh**/**--shel**.
68+
69+
**exec** [_options_] _"prompt"_
70+
> Direct Rust CLI one-shot runner (**tura_exec**). Reads prompt from stdin if omitted. Options include **-C**/**--cwd**, **-m**/**--model**, **-a**/**--agent**, **--json**, **--quiet**, **--sandbox**, **--goal**, **--bash**/**--zsh**/**--shll**.
71+
72+
**bash** | **zsh** | **shel** _"prompt"_
73+
> Aliases for **run** with the **command_run** shell surface forced.
74+
75+
**session** **list**|**show**|**update**|**abort** ...
76+
> Inspect and modify gateway sessions. **list** supports **--all** and **--json**.
77+
78+
**resume** [_SESSION_ID_ | **--last**] [_prompt_...]
79+
> Show a session, or append a follow-up prompt.
80+
81+
**config** **get**|**set**|**model-tier** ...
82+
> Read or patch workspace session config and model tiers.
83+
84+
**provider** **list**|**status**|**login**|**set-auth**|**logout** ...
85+
> List providers and manage local authentication (OAuth or API key). Credentials are not bundled; configure a provider before prompt commands.
86+
87+
**agent** **list**|**show**|**create**|**update**|**delete**|**model** ...
88+
> Work with the gateway agent registry (default agent id often **balanced**).
89+
90+
**persona** **list**|**show**|**create**|**update**|**delete** ...
91+
> Work with the gateway persona registry.
92+
93+
**project** **current**|**list**|**create**|**default** ...
94+
> Inspect or create gateway workspaces.
95+
96+
**file** **list**|**read**|**open**|**reveal** ...
97+
> Operate on files in the selected workspace via the gateway.
98+
99+
**command** **list**|**run** ...
100+
> List or execute registered gateway commands (not arbitrary shell).
101+
102+
**inspect** **status**|**path**|**sessions**|**messages** ...
103+
> Diagnostics for gateway and session state.
104+
105+
**completion** **bash**|**zsh**|**fish**
106+
> Print shell completion snippets.
107+
108+
**gateway** _METHOD_ _PATH_ [**-d** _JSON_]
109+
> Send one raw HTTP request through the CLI gateway client.
110+
111+
**register-cli** | **unregister-cli** | **doctor-cli-path**
112+
> npm package-entry helpers to register or check the release binary on **PATH**.
113+
114+
Related binaries: **tura_gateway** (local HTTP/SSE gateway), **tura_gui** (desktop client), **tura_exec**, **tura_router**, **tura_session_db** (runtime plumbing).
115+
116+
# DESCRIPTION
117+
118+
**tura** is an open-source agent runtime harness designed to complete long-horizon coding tasks with fewer model turns and tokens than typical tool-calling loops. Instead of exposing many fine-grained tools per step, it emphasizes a macro **command_run** tool so related shell, patch, build, and test actions can run in one structured turn, plus runtime context management tied to task state.
119+
120+
The primary entry point is the **tura** command: with no arguments it launches a terminal UI; **tura run** and **tura exec** provide non-interactive paths for scripts and CI-style prompts. A local gateway process coordinates sessions, agents, and providers. Install via npm (**tura-ai**) or from source with the project's install scripts; on first launch, configure an LLM provider and model before sending prompts.
121+
122+
Published benchmarks compare Tura agent configurations against other coding agents on long-horizon tasks; results and methodology are documented upstream. License is AGPL-3.0-or-later.
123+
124+
# CAVEATS
125+
126+
Requires a configured LLM provider; installation alone does not supply credentials. Behavior and available models depend on which providers you authenticate. Some subcommands need a running or auto-started gateway. Companion binaries (**tura_gateway**, **tura_gui**, router/session DB tools) are for service and desktop use, not everyday prompt entry. Spelling of shell surfaces differs slightly between TypeScript (**shel**) and Rust (**shll**) frontends.
127+
128+
# HISTORY
129+
130+
Developed by **Tura-AI** as an open-source agent harness with TUI, CLI, and optional GUI, emphasizing macro command execution and context control. Distributed on npm as **tura-ai** and on GitHub as **Tura-AI/tura**.
131+
132+
# SEE ALSO
133+
134+
[codex](/man/codex)(1), [aider](/man/aider)(1), [opencode](/man/opencode)(1), [npm](/man/npm)(1)
135+
136+
# RESOURCES
137+
138+
```[Source code](https://github.com/Tura-AI/tura)```
139+
140+
```[Homepage](https://turaai.net/)```
141+
142+
```[Documentation](https://github.com/Tura-AI/tura/blob/main/docs/SUMMARY.md)```
143+
144+
<!-- verified: 2026-08-09 -->

0 commit comments

Comments
 (0)