Regula rule reference

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

Rule index🔗

Every rule the linter can emit, generated from its typed registry. The filters work without JavaScript. What every rule shares is on how rules are enforced.

All 22 registered rules
IDRuleCategoryReported in
RG1001Project logical axioms are forbiddensubreason project-axiomFoundationdeclarationEditorProjectSingle fileDocs examples
RG1002Proof holes are forbiddensubreason holeFoundationdeclarationEditorProjectSingle fileDocs examples
RG1003Unknown transitive axioms are forbiddensubreason unknown-axiomFoundationdeclarationEditorProjectSingle fileDocs examples
RG1004Compiler-trusting proofs require separate classificationsubreason compiler-trustingFoundationdeclarationEditorProjectSingle fileDocs examples
RG1005Transitive axioms must fit the selected profilesubreason label-exceeds-claimFoundationdeclarationEditorProjectSingle file
RG1006Unsafe and partial declarations require exact helper authenticationsubreason escape-hatchDeclarationdeclarationEditorProjectSingle fileDocs examples
RG1007Executable contracts require supported closed evidencesubreason executable-contractExecutiondeclarationEditorProjectSingle fileDocs examples
RG2001The declared Lean environment must be availablesubreason environmentEnvironmentprojectProjectSingle file
RG2002Configuration must classify the complete Lake surfacesubreason configurationConfigurationprojectEditorProjectSingle file
RG2003Claimed source must elaborate warning-freesubreason source-buildElaborationprojectProjectSingle file
RG2004Owned coverage must match the exact Lake inventorysubreason coverageCoverageprojectProjectSingle file
RG2005Required admission and source evidence must be completesubreason admissionAdmissionprojectEditorProjectSingle fileDocs examples
RG2006Claimed targets must build with the community configurationsubreason community-configurationConfigurationprojectProject
RG3001Execution closure must have no unresolved pathssubreason execution-unresolvedExecutionexecution rootProjectSingle file
RG3002Checked execution requires admitted correspondencesubreason execution-trusted-boundaryExecutionexecution rootProjectSingle file
RG4001Documentation fences must have a valid classificationsubreason fence-structureDocumentationdocumentation fenceDocs examples
RG4002Positive examples require warning-free elaboration and admissionsubreason positive-exampleDocumentationdocumentation fenceDocs examples
RG4003Negative examples require completed intended rejectionsubreason negative-exampleDocumentationdocumentation fenceDocs examples
RG4004Teaching examples require authenticated compiler classificationsubreason trusted-exampleDocumentationdocumentation fenceDocs examples
RG5001Claimed modules need a leading module docstring and no repeated importsubreason module-documentationDocumentationmoduleEditorProject
RG5002Registered public material declarations require docstringssubreason material-documentationDocumentationregistered material declarationEditorProject
RG5003Registered public material declarations require an Intent sectionsubreason material-intentDocumentationregistered material declarationEditorProject
No registered rule matches the selected filters. Use Reset to show every rule.