Regula rule reference

This page documents Regula 0.8.0. The latest release is Regula 0.11.1: this page in Regula 0.11.1.

RG4001: Documentation fences must have a valid classification🔗

  • Category Documentation
  • Scope documentation fence
  • Subreason fence-structure

A Markdown file in the checked documentation tree has a malformed Lean fence classification: an orphan, misplaced, duplicated or misspelled marker, an invalid expected-error pattern, or an unclosed fence.

What to do. Put each lean-fail or lean-trusted-compiler marker immediately before the lean fence it classifies, with a valid pattern, and close every fence.

Requirement
Each lean-fail or lean-trusted-compiler marker sits immediately before the lean fence it classifies, and every fence is closed.
Reported in
Docs examples
Enforcement
Strict, like every rule: see how rules are enforced.

Checked example🔗

Violating input

✗ Rejecteddocs/Example.mdsource examples/rules/RG4001/Violation.md
```lean
/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl
```
<!-- lean-fail: unknown identifier -->

Findings of the violating run

RG4001 error violation documentation example

Subject <example>/docs at project <example>/docs

Example.md:7: marker is not immediately adjacent to a ```lean fence

Correction

Change to docs/Example.md
  ⋯ 3 unchanged lines
  Reflexivity for every natural number. -/
  theorem reflexive (n : Nat) : n = n := rfl
  ```
- <!-- lean-fail: unknown identifier -->
✓ Passesdocs/Example.mdsource examples/rules/RG4001/Fixed.md
```lean
/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl
```

The correction removes the orphan marker; the positive reflexivity fence is unchanged.

Checked by a documentation fence audit of <example>/docs: violating run rejected, corrected run completed.

How to fix it🔗

  1. Move the marker so no blank line or other content separates it from its fence.

  2. Delete orphan markers, or add the fence they were meant to classify.

  3. Use the exact marker spelling; write non-Lean sketches with another fence language.

Why it matters🔗

A misspelled or misplaced marker must not silently turn a negative example into a positive one or hide a fence from checking. Fail-closed structure keeps every documented Lean claim checked as intended.

What triggers it🔗

The documentation scanner classifies every Lean fence in every Markdown file of the selected tree. An unmarked lean fence is positive; an immediately adjacent <!-- lean-fail: PATTERN --> makes the next fence negative; <!-- lean-trusted-compiler --> marks a teaching example. Anything else that looks like a marker, or a structural error, is rejected with applicability fence-structure.

The pattern grammar is small: | separates alternatives, .* separates ordered literal fragments, and an optional leading (?s) is accepted for compatibility; other regex syntax is rejected.

What a passing result establishes🔗

Every Lean fence in the checked tree has exactly one valid classification.

It does not establish:

  • That the prose around a fence describes it faithfully (R-DOC).

It leaves these review obligations open: R-QUALIFY, R-DOC.

Configuration and exceptions🔗

The checked tree is the documentation tree the audit selects (docs/ for lake exe docFenceAudit). There is no per-fence opt-out.

This rule is a documentation-mode rule; it is not reported by the per-declaration editor linter.

Limitations and unsupported cases🔗

Only Markdown structure is checked here; elaboration results belong to RG4002–RG4004.

Sources🔗

Normative clauses
standard §7.7 Check Lean Documentation Verbatim
Checklist rows
DOC-03
Detector, policy and proof sources
lean/Regula/Checker/Documentation.lean, lean/Regula/Checker/Diagnostics.lean, lean/RegulaPolicy/Pattern.lean
Proved linkage
Acceptance side only: an accepted run satisfies RegulaPolicy.DocumentOK. The fence scanner is not proved.