chore: sync main with development

.github/workflows/check.yml

@@ -20,9 +20,26 @@ jobs:
     if: github.event_name == 'pull_request'
     runs-on: ubuntu-latest
     steps:
+      - name: Check branch strategy
+        run: |
+          TARGET="${{ github.base_ref }}"
+          SOURCE="${{ github.head_ref }}"
+          # Feature branches → development only
+          if [[ "$SOURCE" =~ ^(feat|fix|chore|docs|refactor)/ && "$TARGET" != "development" ]]; then
+            echo "::error::Feature branches must target development, not $TARGET."
+            exit 1
+          fi
+          # PRs to main → must come from development
+          if [[ "$TARGET" == "main" && "$SOURCE" != "development" ]]; then
+            echo "::error::PRs to main must come from development."
+            exit 1
+          fi
+          echo "✓ branch strategy OK: $SOURCE → $TARGET"
+
       - name: Check branch naming
         run: |
           SOURCE="${{ github.head_ref }}"
+          if [[ "$SOURCE" == "development" ]]; then exit 0; fi
           if [[ ! "$SOURCE" =~ ^(feat|fix|chore|docs|refactor)/ ]]; then
             echo "::error::Branch '$SOURCE' does not follow naming convention."
             echo "Must start with: feat/, fix/, chore/, docs/, or refactor/"

CLAUDE.md

@@ -10,7 +10,10 @@ enforcement lives in CI and the Lean type system, not here.
 - **No `import Mathlib`** — full import banned; Lean syntax linter
   `Util/Linter/ImportBan.lean` enforces at build time.
 - **Build green** — `lake build` must pass.
-- **Branch protection** — `main` protected; no direct push, PRs only.
+- **Branch protection** — `main` and `development` protected;
+  no direct push, PRs only.
+- **Branch strategy** — feature branches (`feat/`/`fix/`/`chore/`/
+  `docs/`/`refactor/`) → `development` → `main`. CI enforces.
 - **Branch naming** — branches must start with `feat/`/`fix/`/`chore/`/
   `docs/`/`refactor/`. CI enforces.
 - **PR title** — must match `type(scope): summary`. CI enforces.

lean/ProofAtlas/Util/Linter.lean

@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2026 MathNetwork. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: MathNetwork
+-/
+import ProofAtlas.Util.Linter.ImportBan
+import ProofAtlas.Util.Linter.MathTag
+import ProofAtlas.Util.Linter.DocstringRequired

lean/ProofAtlas/Util/Linter/DocstringRequired.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2026 MathNetwork. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: MathNetwork
+-/
+import Lean
+
+/-!
+# `linter.proofAtlasDocstringRequired`
+
+Enforces that every top-level `def`, `theorem`, `lemma`, `abbrev`,
+`structure`, `inductive`, `class`, or `instance` has a `/-- ... -/`
+docstring. This ensures doc-gen4 produces complete API documentation.
+
+Activated project-wide via `weak.linter.proofAtlasDocstringRequired`
+in the lakefile. To silence locally:
+
+    set_option linter.proofAtlasDocstringRequired false in
+    def myInternalHelper ...
+-/
+
+open Lean Elab Linter
+
+namespace ProofAtlas.Linter.DocstringRequired
+
+/-- The docstring-required linter option. -/
+register_option linter.proofAtlasDocstringRequired : Bool := {
+  defValue := false
+  descr := "Require `/-- ... -/` docstring on every public declaration."
+}
+
+/-- Docstring-required linter. Fires on top-level declaration commands
+that have no docstring at all. -/
+def docstringRequiredLinter : Linter where run := withSetOptionIn fun stx ↦ do
+  unless getLinterValue linter.proofAtlasDocstringRequired (← getLinterOptions) do return
+  unless stx.isOfKind ``Lean.Parser.Command.declaration do return
+  let docStx := stx[0][0][0]
+  unless docStx.isMissing do return
+  let some name := stx.getKind.components.getLast? | return
+  Linter.logLint linter.proofAtlasDocstringRequired stx
+    m!"declaration is missing a `/-- ... -/` docstring"
+
+initialize addLinter docstringRequiredLinter
+
+end ProofAtlas.Linter.DocstringRequired

lean/docbuild/lake-manifest.json

@@ -0,0 +1,163 @@
+{"version": "1.2.0",
+ "packagesDir": "../.lake/packages",
+ "packages":
+ [{"type": "path",
+   "scope": "",
+   "name": "ProofAtlas",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "..",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "689fdeecf45e08cc048214680d40cfe2491be78b",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/subverso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "ce893b9042128037e2d3c0158b9567fab9fae268",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "ce893b9042128037e2d3c0158b9567fab9fae268",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b2958bc1a0e2db353d06d6c019cd3f8bb8a1163c",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "b2958bc1a0e2db353d06d6c019cd3f8bb8a1163c",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "293af9b2a383eed4d04d66b898d608d0a44b750f",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.98",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0-rc2",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0-rc2",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "bde4e24be7b1173e275adf0858ee9d4fc83beaac",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0-rc2",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/leansqlite",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a1d21d8b5f230205bb04c3bff479383f66802c0b",
+   "name": "leansqlite",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f8c99ff779ec217063545b3b191747c92e7fbfb3",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"}],
+ "name": "«proofatlas-docs»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

site/public/api/404.html

@@ -0,0 +1 @@
+<html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="./style.css"></link><link rel="icon" href="./favicon.svg"></link><link rel="mask-icon" href="./favicon.svg" color="#000000"></link><link rel="prefetch" href=".//declarations/declaration-data.bmp" as="image"></link><title>404</title><script defer="true" src="./mathjax-config.js"></script><script defer="true" src="https://cdnjs.cloudflare.com/polyfill/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="./";</script><script type="module" src="./jump-src.js"></script><script type="module" src="./search.js"></script><script type="module" src="./expand-nav.js"></script><script type="module" src="./how-about.js"></script><script type="module" src="./instances.js"></script><script type="module" src="./importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label><span>Documentation</span></h1><h2 class="header_filename break_within"><span class="name">404</span></h2><form id="search_form"><input type="text" name="q" autocomplete="off"></input>&#32;<button id="search_button" onclick="javascript: form.action='./search.html';">Search</button></form></header><main><h1>404 Not Found</h1><p>Unfortunately, the page you were looking for is no longer here. </p><div id="howabout"></div></main><nav class="nav"><iframe src="./navbar.html" class="navframe" frameBorder="0"></iframe></nav></body></html>

site/public/api/Init.html

@@ -0,0 +1,3 @@
+<html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="./style.css"></link><link rel="icon" href="./favicon.svg"></link><link rel="mask-icon" href="./favicon.svg" color="#000000"></link><link rel="prefetch" href=".//declarations/declaration-data.bmp" as="image"></link><title>Init</title><script defer="true" src="./mathjax-config.js"></script><script defer="true" src="https://cdnjs.cloudflare.com/polyfill/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="./";</script><script>const MODULE_NAME="Init";</script><script type="module" src="./jump-src.js"></script><script type="module" src="./search.js"></script><script type="module" src="./expand-nav.js"></script><script type="module" src="./how-about.js"></script><script type="module" src="./instances.js"></script><script type="module" src="./importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label><span>Documentation</span></h1><h2 class="header_filename break_within"><span class="name">Init</span></h2><form id="search_form"><input type="text" name="q" autocomplete="off"></input>&#32;<button id="search_button" onclick="javascript: form.action='./search.html';">Search</button></form></header><nav class="internal_nav"><p><a href="#top">return to top</a></p><p class="gh_nav_link"><a href="https://github.com/leanprover/lean4/blob/d024af099ca4bf2c86f649261ebf59565dc8c622/src/Init.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="./Init/BinderNameHint.html">Init.BinderNameHint</a></li><li><a href="./Init/BinderPredicates.html">Init.BinderPredicates</a></li><li><a href="./Init/ByCases.html">Init.ByCases</a></li><li><a href="./Init/CbvSimproc.html">Init.CbvSimproc</a></li><li><a href="./Init/Control.html">Init.Control</a></li><li><a href="./Init/Conv.html">Init.Conv</a></li><li><a href="./Init/Core.html">Init.Core</a></li><li><a href="./Init/Data.html">Init.Data</a></li><li><a href="./Init/Dynamic.html">Init.Dynamic</a></li><li><a href="./Init/Ext.html">Init.Ext</a></li><li><a href="./Init/Grind.html">Init.Grind</a></li><li><a href="./Init/GrindInstances.html">Init.GrindInstances</a></li><li><a href="./Init/Guard.html">Init.Guard</a></li><li><a href="./Init/Hints.html">Init.Hints</a></li><li><a href="./Init/Internal.html">Init.Internal</a></li><li><a href="./Init/LawfulBEqTactics.html">Init.LawfulBEqTactics</a></li><li><a href="./Init/MacroTrace.html">Init.MacroTrace</a></li><li><a href="./Init/Meta.html">Init.Meta</a></li><li><a href="./Init/MetaTypes.html">Init.MetaTypes</a></li><li><a href="./Init/MethodSpecsSimp.html">Init.MethodSpecsSimp</a></li><li><a href="./Init/Notation.html">Init.Notation</a></li><li><a href="./Init/NotationExtra.html">Init.NotationExtra</a></li><li><a href="./Init/Omega.html">Init.Omega</a></li><li><a href="./Init/Prelude.html">Init.Prelude</a></li><li><a href="./Init/PropLemmas.html">Init.PropLemmas</a></li><li><a href="./Init/RCases.html">Init.RCases</a></li><li><a href="./Init/ShareCommon.html">Init.ShareCommon</a></li><li><a href="./Init/SimpLemmas.html">Init.SimpLemmas</a></li><li><a href="./Init/Simproc.html">Init.Simproc</a></li><li><a href="./Init/SizeOfLemmas.html">Init.SizeOfLemmas</a></li><li><a href="./Init/Sym.html">Init.Sym</a></li><li><a href="./Init/Syntax.html">Init.Syntax</a></li><li><a href="./Init/System.html">Init.System</a></li><li><a href="./Init/Tactics.html">Init.Tactics</a></li><li><a href="./Init/TacticsExtra.html">Init.TacticsExtra</a></li><li><a href="./Init/Task.html">Init.Task</a></li><li><a href="./Init/Try.html">Init.Try</a></li><li><a href="./Init/Util.html">Init.Util</a></li><li><a href="./Init/WF.html">Init.WF</a></li><li><a href="./Init/WFComputable.html">Init.WFComputable</a></li><li><a href="./Init/WFTactics.html">Init.WFTactics</a></li><li><a href="./Init/While.html">Init.While</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-Init" class="imported-by-list"></ul></details></div></nav><main>
+</main>
+<nav class="nav"><iframe src="./navbar.html" class="navframe" frameBorder="0"></iframe></nav></body></html>