Autoformalization agent configuration by Valentin889 · Pull Request #18 · LindenRegex/Warblre

Valentin889 · 2026-05-18T06:47:53Z

Agent Configuration and Documentation

This PR introduces the agentic pipeline for autoformalizing ECMAScript regex proposals into the Warblre Rocq mechanization. It adds OpenCode agent definitions, MCP configuration, the audit tool, and documentation.

What This PR Adds

1. OpenCode Agents (`.opencode/agents/`)

Six agents that form the pipeline, each with description.md and prompt.md:

Agent	Role
`annotate_rocq`	Reads ECMA proposal diffs and inserts spec comments (`(>> ... <<)`) into `.v` files.
`implement_from_comments`	Implements Rocq definitions and algorithms below existing spec comments. May use `Admitted.` to compile.
`fix_audit_batch`	Orchestrates `fix_audit_entry` sequentially.
`fix_proofs`	Scans for `Proof. Admitted.` and synthesizes proof scripts using rocq-mcp
`filter_audit`	Cleans JSON audit, keeping only entries with concrete mismatches.

2. Server Configuration (`.opencode/`)

opencode.json — OpenCode workspace config pointing to the rocq-mcp server for interactive proof checking
AGENTS.md — Reference for all agents, their inputs/outputs, and invocation syntax

3. Audit Tool (`utils/autoformalization/audit/`)

comment_code_audit.py — Audit script
config.json, prompts.json, environment.yml — Model config, few-shot prompts, and conda environment
HTML report generation — from_json_to_html.py turns audit JSONs into reports

4. Pipeline Documentation

utils/autoformalization/README.md — Complete guide covering:
- Installation (OpenCode CLI, EPFL RCP provider, rocq-mcp)
- The 6-step pipeline workflow
- Agent invocation examples
- Verification checklist
utils/autoformalization/audit/README.md — Guide for the audit tool

This agent only write the comment for a proposal

Update description.md

KacperFKorban

My main comment is that we would like to have something that is one-click. It seems like there is a lot of steps that have to be done. And most of them can be automated (fairly) easily.

Disclaimer: I didn't try doing the setup myself, just did a review

KacperFKorban · 2026-06-01T14:43:23Z

+            "command": [
+                "/Users/valentinschneeberger/miniconda3/envs/coq-proof/bin/rocq-mcp"
+            ],
+            "environment": {
+                "ROCQ_WORKSPACE": "/Users/valentinschneeberger/epfl/masterProject/warblre",
+                "ROCQPATH": "_build/default/mechanization",
+                "ROCQ_COQC_BINARY": "/Users/valentinschneeberger/.opam/default/bin/coqc",
+                "ROCQ_PET_BINARY": "/Users/valentinschneeberger/.opam/default/bin/pet",


These should be relative or replaced by a template that can be easily replaced

KacperFKorban · 2026-06-01T14:50:47Z

+```
+annotate_rocq  ──►  implement_from_comments  ──►  audit  ──►  fix_audit_batch  ──►  fix_proofs
+```


There should be a single script that runs all of those in the correct order. Or it can even be a meta prompt.

KacperFKorban · 2026-06-01T14:54:41Z

Please add a high level description of what this script does (preferably near the top of the file)

KacperFKorban · 2026-06-01T14:58:51Z

+
+### 6.4 Step 3 — Audit
+
+Run the audit tool on the files that changed in `mechanization/spec/`.


We want more fine-grained control– to audit only the definitions that were changed. (Maybe just the things present in git diff additions)

KacperFKorban · 2026-06-01T14:59:27Z

+
+```bash
+cd utils/autoformalization/audit
+python comment_code_audit.py


This should document the full call with all necessary parameters

KacperFKorban · 2026-06-01T15:02:29Z

+| `annotate_rocq` | Reads an ECMA proposal diff and inserts specification comments (`(*>> … <<*)`) into Rocq `.v` files. **Comments only — never writes code.** |
+| `implement_from_comments` | Implements the Rocq definitions,Fixpoints and algorithms that correspond to the spec comments added by `annotate_rocq`. |
+| `implement_proposal` | End-to-end implementation of a proposal (syntax + semantics + tests) in one shot. |
+| `run_local_audit` | Runs the audit tool **only on uncommitted changes**, restricting analysis to modified definitions for fast feedback. |
+| `filter_audit` | Cleans raw audit results, keeping only entries that report concrete syntactic mismatches or missing steps. |
+| `fix_audit_entry` | Fixes a **single** audited Coq snippet based on the reported issues and commits if the build passes. |
+| `fix_audit_batch` | Orchestrates `fix_audit_entry` over many snippets **sequentially** (one at a time). |
+| `fix_proofs` | Scans the entire mechanization for `Proof. Admitted.`, synthesizes missing proof scripts using `rocq-mcp` and existing patterns, and verifies with `dune build`. |
+| `test262_converter` | Converts a **whole** Test262 branch into a fresh OCaml expect-test file (`tests/tests/Test262_<Feature>.ml`). |
+| `fix_test262_batch` | Orchestrates conversion of all JS test files in a branch by calling `fix_test262_file` sequentially. |
+| `fix_test262_file` | Generates complete OCaml expect-tests for a **single** JavaScript test file from Test262. |


Some of these aren't in this PR e.g. implement_proposal, run_local_audit

KacperFKorban · 2026-06-01T15:03:10Z

+### 8.2 How to Add a New Agent
+
+To extend the pipeline with a new agent:
+
+1. **Create the agent directory**
+   ```bash
+   mkdir -p .opencode/agents/<agent-name>
+   ```
+
+2. **Add the files**
+
+   - **`description.md`** — Short summary (1 paragraph) of what the agent does, its inputs/outputs, and constraints. OpenCode uses this to decide when to invoke the agent.
+   - **`prompt.md`** — Detailed system prompt that the LLM will follow when the agent is called. Include task description, constraints, step-by-step workflow, output format, and error-handling rules.
+
+3. **Invoke it**
+   Once the folder exists, the agent is automatically available in OpenCode via:
+   ```
+   @<agent-name> <your prompt>
+   ```
+
+> **Tip:** Follow the style of existing agents. Keep prompts concrete, give examples where possible, and always state whether the agent is allowed to modify code, run builds, or commit changes.


This doesn't seem specific to warblre

KacperFKorban · 2026-06-01T15:04:30Z

+- [ ] `dune build @all` succeeds without errors
+- [ ] `dune test` passes
+- [ ] `rocqchk` validates the compiled libraries
+- [ ] No `Admitted.` proofs remain
+- [ ] Code follows the repository naming conventions
+- [ ] Spec comments reference the correct ECMAScript sections


Can we have a simple script that performs most of these checks?

KacperFKorban · 2026-06-01T15:06:30Z

+
+- [ ] `dune build @all` succeeds without errors
+- [ ] `dune test` passes
+- [ ] `rocqchk` validates the compiled libraries


I've never used rocqchk, does it check something more than dune build would?

Valentin889 added 9 commits May 8, 2026 20:20

Update gitignore for proposal and macos DS_Store

5c725b0

Add anotation agent

9b8d182

This agent only write the comment for a proposal

Add filtering agent

f8b0512

Update description.md

Add agent to use the generated audit and apply it

373864f

Add agent to fix proofs

1502cbf

Add agent that implement the code from the proposal

541a034

Agent configuration

be5ee2f

Add audit tool

ee3d524

Add full documentation

c0fde15

Valentin889 self-assigned this May 18, 2026

Add vsrocq

1f577a7

KacperFKorban reviewed Jun 1, 2026

View reviewed changes

Create diff_audit.py

09faf94

Valentin889 force-pushed the vs/autoformalization/agent-config branch from bcc61a3 to 09faf94 Compare June 25, 2026 13:50

Navigation Menu

Uh oh!

Autoformalization agent configuration - #18

Autoformalization agent configuration#18
Valentin889 wants to merge 11 commits into
mainfrom
vs/autoformalization/agent-config

Valentin889 commented May 18, 2026

Uh oh!

KacperFKorban left a comment

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

KacperFKorban Jun 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants


		### 6.4 Step 3 — Audit

		Run the audit tool on the files that changed in `mechanization/spec/`.

Uh oh!

Conversation

Valentin889 commented May 18, 2026

Agent Configuration and Documentation

This PR introduces the agentic pipeline for autoformalizing ECMAScript regex proposals into the Warblre Rocq mechanization. It adds OpenCode agent definitions, MCP configuration, the audit tool, and documentation.

What This PR Adds

1. OpenCode Agents (.opencode/agents/)

2. Server Configuration (.opencode/)

3. Audit Tool (utils/autoformalization/audit/)

4. Pipeline Documentation

Uh oh!

KacperFKorban left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

1. OpenCode Agents (`.opencode/agents/`)

2. Server Configuration (`.opencode/`)

3. Audit Tool (`utils/autoformalization/audit/`)