Menu
Use when a coding agent should clone, patch, set up, and supervise FrenzyMath Rethlas on a machine that already has OpenCode installed and configured.
Installer avec Codex ou Claude Copiez ce prompt, collez-le dans Codex, Claude ou un autre assistant, puis laissez-le vérifier la page du skill et l'installer pour vous.
Basé sur la classification professionnelle SOC
| name | rethlas-opencode-adapter |
| description | Use when a coding agent should clone, patch, set up, and supervise FrenzyMath Rethlas on a machine that already has OpenCode installed and configured. |
Use this skill when the user wants to deploy FrenzyMath Rethlas on a machine that already has OpenCode installed and configured.
Trigger this skill for requests such as:
The target workflow is:
agents/generation/data/.agents/generation/tests/run_example.sh with OpenCode.agents/generation/results/<problem_id>/blueprint_verified.md.Do not edit the user's global OpenCode configuration unless the user explicitly asks for provider/model setup.
Do not add test problems, unit tests, README edits, or generated caches as part of the adapter patch.
git diff after patching and before launching OpenCode with --auto.OPENCODE_MODEL unset when the user wants to use their existing OpenCode provider/model configuration.Set SKILL_DIR to the directory that contains this SKILL.md, then use:
ADAPTER_SCRIPT="$SKILL_DIR/scripts/apply_adapter.py"
When working inside Codex, resolve SKILL_DIR from the expanded skill path. When working from a copied skill directory, use that copied directory.
Check the local tools before patching:
git --version
python3 --version
opencode --version
If opencode --version fails, stop and ask the user to install or configure OpenCode first.
If python3 -m venv --help fails, stop and report that a Python venv-capable installation is required.
The adapter script changes only these paths inside the Rethlas clone:
agents/generation/tests/run_example.sh
agents/verification/api/server.py
agents/generation/.opencode/.gitignore
agents/generation/.opencode/AGENTS.md
agents/generation/.opencode/agent/rethlas-generation.md
agents/generation/.opencode/agent/rethlas-generation-no-search.md
agents/generation/.opencode/agent/subgoal-prover.md
agents/generation/.opencode/opencode.json
agents/verification/.opencode/.gitignore
agents/verification/.opencode/AGENTS.md
agents/verification/.opencode/agent/rethlas-verification.md
agents/verification/.opencode/opencode.json
From any working directory:
python3 "$ADAPTER_SCRIPT" \
--target /path/to/Rethlas \
--clone
If the Rethlas clone already exists:
python3 "$ADAPTER_SCRIPT" \
--target /path/to/Rethlas
For an existing clone with local edits, stop and ask the user before using --allow-dirty.
After patching, run these static checks from the Rethlas clone:
bash -n agents/generation/tests/run_example.sh
python3 -m py_compile agents/verification/api/server.py
python3 -m json.tool agents/generation/.opencode/opencode.json >/dev/null
python3 -m json.tool agents/verification/.opencode/opencode.json >/dev/null
Write the user's problem under agents/generation/data/. For display math in markdown files, use $$.
Example:
mkdir -p /path/to/Rethlas/agents/generation/data/user
$EDITOR /path/to/Rethlas/agents/generation/data/user/problem.md
The problem_id becomes the path under data/ without .md. For the example above, it is user/problem.
Verification side:
cd /path/to/Rethlas/agents/verification
python3 -m venv .venv
source .venv/bin/activate
python -m pip install --upgrade pip
python -m pip install -r requirements.txt
Generation side:
cd /path/to/Rethlas/agents/generation
python3 -m venv .venv
source .venv/bin/activate
python -m pip install --upgrade pip
python -m pip install -r mcp/requirements.txt
If the user asks to use uv, the equivalent commands are uv venv and uv pip install ....
Terminal 1:
cd /path/to/Rethlas/agents/verification
source .venv/bin/activate
VERIFY_EXECUTOR=opencode python -m uvicorn api.server:app --host 127.0.0.1 --port 8091
Terminal 2:
cd /path/to/Rethlas/agents/generation
source .venv/bin/activate
EXECUTOR=opencode PROBLEM_FILE=data/user/problem.md ./tests/run_example.sh
Leave OPENCODE_MODEL unset when the user wants to use the model already configured in OpenCode.
To override the model for this run:
EXECUTOR=opencode OPENCODE_MODEL=provider/model PROBLEM_FILE=data/user/problem.md ./tests/run_example.sh
During a run, supervise the outer process only:
blueprint_verified.md exists.The success artifact is:
/path/to/Rethlas/agents/generation/results/<problem_id>/blueprint_verified.md
If the runner exits without that file, report the exit code and the paths to the runner log directory and verification logs.
Route AI4Math automated mathematical research tasks to normalized skill packages in this repository.
Use when Codex needs to interactively deploy, configure, verify, or launch AI4Math Auto-Research with Agent Laboratory, including API-key handling, user research-topic intake, full local validation, and human review gates.
Use when Codex should act as a coding-agent-native mathematical problem discovery engine: turn fuzzy mathematical background, scattered notes, domain intuition, failed proof attempts, or immature theorem ideas into a ranked problem menu, conjecture lattice, evidence ledger, counterexample pressure, proof obligations, work orders, and a resumable research_state_packet. Use before theorem proving or formal verification when the user does not yet know which mathematical problem should be pursued.
Use when Codex should work as a coding-agent-native proof planning and review workflow: transform a candidate theorem, proof sketch, problem artifact, or proof_obligations into a proof blueprint, verifier-style report, repair hints, proof-obligation ledger patches, and a strict proof acceptance decision without treating API access as the default path.