mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
3044f36df7
Actions taken from 5-agent audit sweep (audit date 2026-05-26): AGENTS.md / docs sync: - root AGENTS.md: add scripts/qc-flag and lean_expert_agent to Nested Contracts - All 6 nested AGENTS.md files: append Cross-References section pointing to root for Post-Interaction Workflow, Programming Choice Flow, Do Not Sweep, Git Remote Hygiene (Lean, Infra, text-to-cad, docs, qc-flag, lean_expert_agent) - 6-Documentation/docs/AGENTS.md: cross-ref also lists AVMIsa.Emit sole output boundary and Compiler surface blessing Lean build baseline: - 0-Core-Formalism/lean/Semantics/AGENTS.md: update blessed Compiler Surface header to commit 49f0dfb3; correct job count to 3311 (lake build Compiler) ARCHITECTURE.md: - §7 repo table: add RRC.Emit, AVMIsa.Emit, RRC.Corpus278 to Lean/Semantics entry - New §7.1 Compiler Surface: documents 3-root pipeline and sole output boundary - §4 Data Flow: annotate output with AVMIsa.Emit sole-boundary note TODO_MAP.md: - Phase A6: add 3 new Lean deliverables (Corpus278, RRC.Emit, AVMIsa.Emit); update status/result with Compiler build baseline; refine next action Build: Compiler 3311 jobs, 0 errors (no Lean changes). Generated with Devin (https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
47 lines
2.4 KiB
Markdown
47 lines
2.4 KiB
Markdown
# QC Flagger — AGENTS.md
|
||
|
||
## Purpose
|
||
Automated code quality inspection for Lean files, implementing the Lean Expert Agent's 7-check inspection protocol.
|
||
|
||
## Usage
|
||
|
||
```bash
|
||
# Run on a single file
|
||
python3 scripts/qc-flag/lean_qc_flagger.py path/to/file.lean
|
||
|
||
# Run on a directory (recursive)
|
||
python3 scripts/qc-flag/lean_qc_flagger.py path/to/dir/
|
||
|
||
# Save reports
|
||
python3 scripts/qc-flag/lean_qc_flagger.py path/to/file.lean --json report.json --markdown report.md
|
||
|
||
# Shell wrapper (saves dated reports to scripts/qc-flag/reports/)
|
||
bash scripts/qc-flag/run_qc_flag.sh path/to/file.lean
|
||
bash scripts/qc-flag/run_qc_flag.sh path/to/dir/ --verbose
|
||
```
|
||
|
||
## Protocol Coverage
|
||
|
||
| # | Check | Implementation |
|
||
|---|-------|----------------|
|
||
| 1 | Structural Health | theorem/def/eval/sorry counts, empty theorems, tautologies, unused imports, `set_option` suppressions |
|
||
| 2 | Naming Conventions | PascalCase files/types, camelCase functions/theorems, banned prefixes/suffixes |
|
||
| 3 | Q16_16 Compliance | Float usage in hot-path code. Historical contamination sites at `BraidCross.lean:49,50,84` and `BraidStrand.lean:57,71` are the canonical fixed-point constructor template. Flag any `ofFloat` outside JSON/sensor boundary shims. |
|
||
| 4 | Proof Quality | defs without companion theorems, `.get!` without `.isSome`, native_decide coverage |
|
||
| 5 | Dependency Analysis | Unused imports, circular and transitive circular dependencies |
|
||
| 6 | Compression Theorem Pair | Every module defining a compression path MUST provide both `eigensolid_convergence` (crossing loop stabilizes) and `receipt_invertible` (receipt bijectively reconstructs original including zero/gap/timing dimensions). Flag missing pairs. |
|
||
| 7 | AGENTS.md Compliance | Root `AGENTS.md` Compression First Principles apply to all Lean code. Check that no compute path uses `ofFloat` and that receipt dimensions are explicitly captured (C, σ, k, ε_seq, t, ∅_scars). |
|
||
|
||
## Output
|
||
|
||
- **JSON**: structured per-file results with issue details
|
||
- **Markdown**: human-readable report with summary table and issue tables
|
||
- **Exit code**: 0 if all files pass, 1 if any file has ERROR-severity issues
|
||
|
||
## Cross-References
|
||
|
||
See root `AGENTS.md` for:
|
||
- **Post-Interaction Workflow** (mandatory 5-step session-end procedure)
|
||
- **Programming Choice Flow** (Lean owns decisions; Python owns I/O)
|
||
- **Do Not Sweep** rules (no broad `git add .`)
|
||
- **Git Remote Hygiene**
|