Collect.lean

module

public import Lean
public import Lean.DeclarationRange
public import Lean.Meta.Instances
public import Lean.Util.Sorry
public import Lake.CLI.Main
public import Lake.Load.Workspace
public import MD4Lean
public import VersoManual
public import VersoManual.Markdown
public import MeaningGraph
public import Characterization
public import ChallengeGen
public import Referee.Formalization
public import Referee.Claims

@[expose] public section

/-!
# Collecting the exposed declarations of a project

Walks a compiled project's environment and builds one `DeclInfo` per exposed declaration:
signature, docstring, source location and snippet, kind, and dependency lists.

The dependency analysis itself lives in `MeaningGraph` — a standalone module that knows nothing
about this tool's output. This file only decides *which* dependency edges Referee follows
(`meaningDeps` for what a declaration means and rests on, `closureDeps` for the wider extraction
closure) and attaches the results to `DeclInfo`.
-/

open Lake
open Lean
open Lean.Meta
open Verso.Doc
open Verso.Genre
open Manual

namespace Referee

open Verso.Output Html
open MeaningGraph
open ChallengeGen

/-- CLI options used to configure site generation. Shared across the `collect`,
`extract`, `build-site`, and `all` subcommands; each one only consults the fields relevant
to it. -/
structure Cli where
  rootPrefix : Option Name := none
  repoUrl : Option String := none
  siteUrl : Option String := none
  siteTitle : Option String := none
  outputDir : Option String := none
  excludeLibs : Array Name := #[]
  /-- Path to the collected-data JSON file: written by `collect`, read by `extract` and
  `build-site`. -/
  dataPath : Option String := none
  /-- Single input file, used by the `highlight-file` worker subcommand. -/
  inputPath : Option String := none
  /-- Maximum number of worker processes to run at once. Defaults to the CPU count. -/
  jobs : Option Nat := none
  /-- Packages the reader is told to take on trust (`--trust`), each standing for itself *and
  everything it depends on*: trusting `mathlib` trusts `batteries` and `aesop` with it, because
  Mathlib's own correctness already rests on them.

  A render-time flag, like `--repo-url`: the same `data.json` can be rendered with different trust
  sets, which is the point — "what if I have not audited LML" should not need re-importing the
  project. -/
  trustedPackages : Array Name := #[]
  /-- Draw declarations from *audited* packages in the graph's upstream band as well as unaudited
  ones (`--show-trusted-upstream`).

  Off by default, and the default is the interesting judgement. Drawing them answers "what is this
  statement about", but on a Mathlib-backed project it is a median of 21 nodes and a p90 of 53 per
  page — a band several times the size of the project structure underneath it, restating something
  the declaration's own code block at the top of the page already shows, with types on hover. What
  the band is *for* is the part no other view has: the packages nobody has vouched for. Those are
  always drawn.

  Kept as a flag rather than removed because the capability is cheap to carry — the data is collected
  either way — and because on a project whose upstream is small the answer could go the other way. -/
  showTrustedUpstream : Bool := false
  /-- An earlier `collect` output to diff the current one against (`--baseline`).

  A render-time flag for the same reason `--trust` is one: the comparison is a pure function of the
  two JSON files, so a reader can ask "what changed since v0.2" without re-importing anything. With
  none given, the site says nothing about revisions at all. -/
  baselinePath : Option String := none
  /-- What to call the baseline on the page (`--baseline-label`). Defaults to the file name. -/
  baselineLabel : Option String := none
  /-- A `semantic_hash export` JSONL file to read declaration hashes from (`--hashes`).

  A `collect`-time input rather than a render-time flag, unlike `--trust` and `--baseline`: the
  hashes are a property of the compiled environment, so they belong in `data.json` beside every
  other thing derived from it. Optional — without it every hash is `none` and the revision diff
  compares text, exactly as it did before the field existed. -/
  hashesPath : Option String := none
  /-- The provenance ledger (`--provenance`): written and updated by the `provenance` subcommand,
  read by `build-site`.

  One file for both directions, because the ledger is append-only: each run folds the current
  revision into whatever is already there. A render-time flag for `build-site`, gated exactly as
  `--baseline` is — without it the site says nothing about when anything changed. -/
  provenancePath : Option String := none
  /-- What to call this revision in the ledger (`--ref`). Defaults to `git describe --tags
  --always`, which prefers a tag and falls back to a short sha. -/
  revisionRef : Option String := none
  /-- Whether to re-check the decoded data's closure invariants on load (`--no-verify` turns it
  off). On by default: it is the guard on the one part of the pipeline `MeaningGraph`'s proofs do
  not cover, the `intern`/`resolve` round trip. Turning it off is for repeated renders of a file
  already checked once — it grew 73× across a 5.5× step in library size, so at Mathlib scope it is
  minutes of re-verifying a file that has not changed. -/
  verifyIntegrity : Bool := true
  /-- Restrict the build to the results the project puts forward and what their *statements* rest
  on (`--claims-only`). See `Referee.Claims` for where the list of results comes from.

  Read by `collect`, which is where the scope is decided, and recorded in `data.json` so that
  `build-site` can frame the site without re-deciding it. Unlike `--trust` or `--baseline` this
  cannot be varied over one collected file, because the file no longer holds what a wider build
  would need — which is the point of it. -/
  claimsOnly : Bool := false
  /-- Build the site for one declaration (`--only DECL`).

  Exactly `--claims-only` with a claim set of this one declaration: the same scope rule, and the
  same site, so everything its statement rests on gets a page too. Rendering only the named
  declaration was the first design and it was wrong — a claim's page is mostly the dependency graph
  under it, and a graph whose nodes have no pages strands the reader on a summary panel when what
  they want is the card. -/
  onlyDecl : Option Name := none
  /-- Declarations to treat as the project's main results (`--claim NAME`), overriding whatever
  `formalization.yaml` or a Comparator setup says. Repeatable.

  For a project with neither metadata document, and for the case where you disagree with the one it
  has. Ignored unless `--claims-only` or `--only` asked for a scoped build. -/
  claimNames : Array Name := #[]
  /-- Where to look for Comparator configs (`--comparator DIR`), when they are not where the
  metadata points and not in a directory the shallow scan finds. -/
  comparatorDir : Option String := none
  /-- Whether `build-site` renders one chapter at a time instead of the whole library in one Verso
  invocation (`--per-chapter`).

  Verso builds the entire document tree before streaming any page out, so a monolithic render's
  peak memory tracks the library — measured at 14.95 GB for 28,251 declarations and projected past
  150 GB for Mathlib. Per-chapter rendering bounds the peak by the largest chapter instead, at the
  cost of a stitching pass afterwards: the global artifacts Verso derives from the whole tree
  (sidebar, `xref.json`, the `find` page, hover data) are merged from the per-chapter runs. -/
  perChapter : Bool := false
deriving Repr

/-- The kind label shown to a reader, which is finer-grained than `DeclKind`.

Lean records `lemma` and `theorem` as the same kind, and some declarations written with `instance`
elaborate to theorems, so `DeclKind.label` alone would show a `lemma` as "Theorem". A reader
comparing the site against the source should see the keyword the author actually wrote. -/
def displayKindLabel (kindLabel : String) (isLemma isInstanceDecl : Bool) : String :=
  if isInstanceDecl then "Instance"
  else if isLemma then "Lemma"
  else kindLabel

/-- Source file location (path and line range) for a declaration. -/
structure SourceInfo where
  relPath : String
  absPath : System.FilePath
  line : Nat
  endLine : Nat
deriving Repr, ToJson, FromJson

/-- Data container for LinkInfo. -/
structure LinkInfo where
  label : String
  href? : Option String := none
deriving Repr, ToJson, FromJson

/-- Data container for DeclCardData.

No name field: the card is the only one on its page, and the page's title is the declaration's
name. -/
structure DeclCardData where
  anchorId : String
  kindLabel : String
  isLemma : Bool := false
  isInstanceDecl : Bool := false
  tags : Array String := #[]
deriving Repr, ToJson, FromJson, Inhabited

/-- One row of a declaration index: the listing used for module contents, the claims and trust
pages, and a declaration's dependency closures. -/
structure DeclIndexEntry where
  name : String
  href : String
  /-- The label shown to the reader (`displayKindLabel`). -/
  kind : String
  /-- `definition` / `lemma` / `theorem`, matching the sidebar's visibility toggles. -/
  group : String
  /-- Project declarations in its closure, where that is worth showing. -/
  deps : Option Nat := none
  /-- An extra fact about this row, shown after the kind and dependency count. Empty for most
  listings; used by the specification page to say how many properties a definition has. -/
  note : String := ""
  dependsOnSorry : Bool := false
deriving Repr, ToJson, FromJson, Inhabited

/-- Data container for DeclIndexData. -/
structure DeclIndexData where
  entries : Array DeclIndexEntry
deriving Repr, ToJson, FromJson, Inhabited

/-- One row of the claims listing.

The listing is rendered *here* rather than by `audit.js`, unlike everything else on that page,
because a row carries the declaration's docstring and the docstring has to be real markdown — the
same `docBlocks` the declaration's own card renders, through the same Verso pipeline, so that code
spans, emphasis and math look the way they look everywhere else. A client building rows from JSON
can only be handed text, and text is what it looked like.

What the browser still owns is the *state* on the row: coverage, verdict, and the button. Those
arrive as empty slots that `audit.js` fills and refills, which is also why the rows survive a
verdict change untouched — nothing is rebuilt, two spans are rewritten. -/
structure ClaimRow where
  name : String
  href : String
  /-- Project declarations in its statement closure. Shown until the browser replaces it with how
  many of them the reader has accepted, so a reader without JavaScript still gets the number. -/
  deps : Nat := 0
  dependsOnSorry : Bool := false
  /-- How many of the enclosing block's contents are this row's docstring. The rows share one flat
  array of contents — a block extension gets its children as a list, not as a tree — so each says
  how many of them are its own, and the renderer walks the two in step. -/
  docLength : Nat := 0
deriving Repr, ToJson, FromJson, Inhabited

/-- Data container for ClaimListData. The block's contents are every row's docstring blocks
concatenated, divided up by `ClaimRow.docLength`. -/
structure ClaimListData where
  rows : Array ClaimRow
deriving Repr, ToJson, FromJson, Inhabited

/-- One row of a specification listing: on a definition's page a theorem offered as part of its
specification, on a theorem's page a definition the theorem specifies.

Unlike `DeclIndexEntry` this carries the statement and the author's comment, because that is the
whole point of the listing: a reader should be able to judge whether the properties pin the
definition down without following a single link. -/
structure SpecRow where
  name : String
  /-- Empty when the declaration at the other end is not exposed and so has no page of its own. -/
  href : String := ""
  /-- The label shown to the reader (`displayKindLabel`). -/
  kind : String
  /-- The author's note on why this belongs in the specification. Empty when they wrote none. -/
  comment : String := ""
  /-- The statement, source form. Empty where the row is a bare link. -/
  signature : String := ""
deriving Repr, ToJson, FromJson, Inhabited

/-- Data container for SpecListData. -/
structure SpecListData where
  entries : Array SpecRow
deriving Repr, ToJson, FromJson, Inhabited

/-! ## The statement, taken apart

A theorem's type is one telescope of binders, and to a reader who cannot yet parse a Mathlib-style
statement it is a wall in which the objects, the structure assumed on them, the hypotheses and the
claim all look alike. `StatementAnatomy` is that telescope split by the role each binder plays,
computed at `collect` time inside the binder's own context so that every type prints with the
author's variable names. The grouping that turns it into a reading order — each object with the
typeclass assumptions made on it — is `StatementAnatomy.grouped`, kept pure so it can be tested. -/

/-- The role one binder of a statement plays for a reader. -/
inductive BinderRole where
  /-- An object the statement is about: a type, a function, an element, a measure. -/
  | object
  /-- Structure assumed on one of those objects: an instance binder such as `[MeasurableSpace Ω]`
  or `[IsProbabilityMeasure μ]`, or any binder whose type is a class — `{mΩ : MeasurableSpace Ω}`
  is structure on `Ω` however the author chose to bind it. -/
  | typeclass
  /-- A proposition assumed: any other binder whose type is a `Prop`. -/
  | hypothesis
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- One piece of a pretty-printed type: a run of text, and the constant it names when the pretty
printer says the run is a constant token. What lets every constant in a binder's type carry its own
hover, the way each token of highlighted code does. -/
structure TypePiece where
  text : String := ""
  const : Name := .anonymous
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- Merges runs of plain text, so a type has as few pieces as it has constants. -/
def coalescePieces (pieces : Array TypePiece) : Array TypePiece :=
  pieces.foldl (init := #[]) fun acc p =>
    if p.text.isEmpty then acc
    else match acc.back? with
    | some last =>
      if last.const.isAnonymous && p.const.isAnonymous then
        acc.pop.push { last with text := last.text ++ p.text }
      else acc.push p
    | none => acc.push p

/-- Cuts the pieces to `limit` characters in all, ending with the ellipsis `clipTo` uses. A piece
cut in the middle loses its constant: half a name is not a hover target. -/
def clipPieces (limit : Nat) (pieces : Array TypePiece) : Array TypePiece := Id.run do
  let mut out : Array TypePiece := #[]
  let mut used := 0
  for p in pieces do
    let len := p.text.length
    if used + len ≤ limit then
      out := out.push p
      used := used + len
    else
      return out.push { text := (p.text.take (limit - used)).toString ++ "…" }
  return out

/-- One binder of a statement's telescope, with what a reader needs in order to place it. -/
structure StatementBinder where
  /-- The binder's name as the author wrote it; empty for an anonymous one (`P → Q`, `[inst : …]`). -/
  name : String := ""
  role : BinderRole := .object
  /-- Whether the object is itself a type — `Ω : Type u_1`, `p : Prop` — rather than an element, a
  function or a measure. Types are listed first: everything else in the statement lives in one. -/
  isType : Bool := false
  /-- `{x}` or `⦃x⦄`: not written where the theorem is used, but inferred from the other arguments. -/
  implicit : Bool := false
  /-- The binder's type, pretty-printed in the context of the binders before it. -/
  type : String := ""
  /-- The same text split at its constants, for a hover on each; see `TypePiece`. -/
  pieces : Array TypePiece := #[]
  /-- The head constant of that type when it has one, looking through leading `∀`s: the class of a
  typeclass binder, the predicate or relation of a hypothesis. What a gloss can be looked up for. -/
  head : Name := .anonymous
  /-- The earlier binders this one's type mentions, as indices into the telescope, in order of first
  occurrence. What attaches `[MeasurableSpace Ω]` to `Ω`. -/
  mentions : Array Nat := #[]
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- One field of a structure or class, for the parts view of its page: the body of a structure is
its fields, and a field's own docstring is what a reader wants on hover. -/
structure StatementField where
  name : String := ""
  /-- The field's type, in the context of the parameters and the fields before it. -/
  type : String := ""
  /-- The same text split at its constants; see `TypePiece`. -/
  pieces : Array TypePiece := #[]
  /-- The head constant of that type, for a hover when the field has no docstring of its own. -/
  head : Name := .anonymous
  /-- The field's docstring, as written on it. -/
  doc : String := ""
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- A statement split into its binders and its conclusion — or a definition into its parameters, its
result type and its body. `isProp` says which reading applies: a theorem's conclusion is a claim, a
definition's is the type of what it produces. -/
structure StatementAnatomy where
  binders : Array StatementBinder := #[]
  /-- The conclusion — a theorem's claim, or a definition's result type — pretty-printed in the
  context of every binder. -/
  conclusion : String := ""
  /-- The conclusion's head constant when it has one, looking through leading `∀`s. -/
  conclusionHead : Name := .anonymous
  /-- The conclusion split at its constants; see `TypePiece`. -/
  conclusionPieces : Array TypePiece := #[]
  /-- Whether the conclusion is a proposition. False for a definition, whose conclusion is the type
  of its value, and whose `body` or `fields` then say what that value is. -/
  isProp : Bool := true
  /-- A definition's value, in the context of its parameters. Empty for a theorem — its proof is not
  part of what it says — and for anything else without one worth showing. -/
  body : String := ""
  /-- The body split at its constants; see `TypePiece`. -/
  bodyPieces : Array TypePiece := #[]
  /-- A structure's or class's fields, in the context of its parameters. -/
  fields : Array StatementField := #[]
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- An object of a statement together with the typeclass assumptions attached to it. -/
structure AnatomyObject where
  /-- Its index in the telescope. -/
  index : Nat
  binder : StatementBinder
  instances : Array StatementBinder := #[]
deriving Repr, BEq, Inhabited

/-- `StatementAnatomy.grouped`: the reading order of a statement. -/
structure AnatomyGroups where
  /-- The objects that are types, in telescope order, each with the structure assumed on it. -/
  types : Array AnatomyObject := #[]
  /-- Every other object, in telescope order, each with the structure assumed on it. -/
  objects : Array AnatomyObject := #[]
  /-- Typeclass binders attached to no object: their types mention none, or only hypotheses. -/
  loose : Array StatementBinder := #[]
  hypotheses : Array StatementBinder := #[]
deriving Repr, BEq, Inhabited

/-- Groups a statement's binders for reading: each object with the typeclass assumptions on it, then
the hypotheses.

A typeclass binder attaches to the *last-introduced* object its type mentions. `[MeasurableSpace Ω]`
mentions only `Ω`; `[Module R M]` mentions `R` and `M` and goes under `M`, the thing it is structure
on, rather than under the ring it is structure over. One mentioning no object at all —
`[DecidableEq ℕ]`, or `[Fact p]` for a hypothesis `p` — is kept rather than dropped, since it is
still assumed. -/
def StatementAnatomy.grouped (a : StatementAnatomy) : AnatomyGroups := Id.run do
  let mut groups : AnatomyGroups := {}
  -- Telescope index ↦ where the object went — `true` for `types`, `false` for `objects` — and its
  -- position there.
  let mut rowOf : Std.HashMap Nat (Bool × Nat) := {}
  for i in [:a.binders.size] do
    let b := a.binders[i]!
    match b.role with
    | .object =>
      if b.isType then
        rowOf := rowOf.insert i (true, groups.types.size)
        groups := { groups with types := groups.types.push { index := i, binder := b } }
      else
        rowOf := rowOf.insert i (false, groups.objects.size)
        groups := { groups with objects := groups.objects.push { index := i, binder := b } }
    | .hypothesis =>
      groups := { groups with hypotheses := groups.hypotheses.push b }
    | .typeclass =>
      let target? := b.mentions.foldl (init := (none : Option Nat)) fun acc j =>
        if rowOf.contains j then some (max (acc.getD j) j) else acc
      match target?.bind (fun j => rowOf.get? j) with
      | some (true, row) =>
        groups := { groups with types := groups.types.modify row fun o =>
          { o with instances := o.instances.push b } }
      | some (false, row) =>
        groups := { groups with objects := groups.objects.modify row fun o =>
          { o with instances := o.instances.push b } }
      | none =>
        groups := { groups with loose := groups.loose.push b }
  return groups

/-- One piece of a type as `Block.anatomy` renders it: text, and the tip it is a hover for. -/
structure AnatomyPiece where
  text : String := ""
  /-- The `AnatomyTip.head` this piece opens on hover, or empty for plain text. -/
  head : String := ""
deriving Repr, ToJson, FromJson, Inhabited

/-- One typeclass assumption of `Block.anatomy`, with what the site could find out about its class. -/
structure AnatomyInstanceRow where
  name : String := ""
  type : String := ""
  /-- `type` split at its constants, each a hover of its own; empty falls back to `type`. -/
  pieces : Array AnatomyPiece := #[]
  /-- The class, shown only when there is a gloss or a link to hang it on. -/
  head : String := ""
  /-- The class's page, when the project declares it. -/
  href : String := ""
  /-- One sentence about the class, from its docstring. -/
  gloss : String := ""
deriving Repr, ToJson, FromJson, Inhabited

/-- One object or hypothesis of `Block.anatomy`, or its conclusion. -/
structure AnatomyRow where
  name : String := ""
  type : String := ""
  /-- `type` split at its constants, each a hover of its own; empty falls back to `type`. -/
  pieces : Array AnatomyPiece := #[]
  implicit : Bool := false
  head : String := ""
  href : String := ""
  gloss : String := ""
  /-- For an object: the typeclass assumptions attached to it. -/
  instances : Array AnatomyInstanceRow := #[]
deriving Repr, ToJson, FromJson, Inhabited

/-- What a hover on a row of `Block.anatomy` shows for its head constant: the constant, its
signature, its whole docstring, and its page when the project declares it. One per head constant
per page — rows point at it by name — so a class assumed on five objects ships its docstring once. -/
structure AnatomyTip where
  head : String := ""
  signature : String := ""
  doc : String := ""
  href : String := ""
deriving Repr, ToJson, FromJson, Inhabited

/-- The payload of `Block.anatomy`: `StatementAnatomy.grouped` with the glosses and tips resolved. -/
structure AnatomyData where
  types : Array AnatomyRow := #[]
  objects : Array AnatomyRow := #[]
  loose : Array AnatomyInstanceRow := #[]
  hypotheses : Array AnatomyRow := #[]
  /-- The claim, or a definition's result type; `isProp` says which. -/
  conclusion : AnatomyRow := {}
  isProp : Bool := true
  /-- A definition's value, shown under its result type. -/
  body : String := ""
  /-- `body` split at its constants; empty falls back to `body`. -/
  bodyPieces : Array AnatomyPiece := #[]
  /-- A structure's fields, shown under its result type; each row's hover is the field's docstring. -/
  fields : Array AnatomyRow := #[]
  tips : Array AnatomyTip := #[]
deriving Repr, ToJson, FromJson, Inhabited

/-- The gloss for `head`, or nothing if this page has already shown one for it. -/
def glossOnce (seen : Std.HashSet String) (head gloss : String) :
    String × Std.HashSet String :=
  if head.isEmpty || gloss.isEmpty then (gloss, seen)
  else if seen.contains head then ("", seen)
  else (gloss, seen.insert head)

/-- `glossOnce` over a list of rows and the instances nested in each, in reading order. -/
def dedupeRows (seen : Std.HashSet String) (rows : Array AnatomyRow) :
    Array AnatomyRow × Std.HashSet String := Id.run do
  let mut seen := seen
  let mut out : Array AnatomyRow := #[]
  for row in rows do
    let (gloss, seen') := glossOnce seen row.head row.gloss
    seen := seen'
    let mut instances : Array AnatomyInstanceRow := #[]
    for inst in row.instances do
      let (g, s) := glossOnce seen inst.head inst.gloss
      seen := s
      instances := instances.push { inst with gloss := g }
    out := out.push { row with gloss, instances }
  return (out, seen)

/-- Keeps the first gloss for each head constant, in reading order, and blanks the rest. Under the
first of five measurable spaces "a space equipped with a σ-algebra" is an explanation; under all five
it is noise. Links survive repeats, being one word each. -/
def AnatomyData.dedupeGlosses (data : AnatomyData) : AnatomyData := Id.run do
  let (types, seen₁) := dedupeRows {} data.types
  let (objects, seen₂) := dedupeRows seen₁ data.objects
  let mut seen := seen₂
  let mut loose : Array AnatomyInstanceRow := #[]
  for inst in data.loose do
    let (g, s) := glossOnce seen inst.head inst.gloss
    seen := s
    loose := loose.push { inst with gloss := g }
  let (hypotheses, seen₃) := dedupeRows seen data.hypotheses
  let (g, seen₄) := glossOnce seen₃ data.conclusion.head data.conclusion.gloss
  let (fields, _) := dedupeRows seen₄ data.fields
  return { data with
    types, objects, loose, hypotheses, fields
    conclusion := { data.conclusion with gloss := g } }

/-- One of the three declarations a characterization is made of, as rendered: the predicate, a
theorem that the definition satisfies it, or a theorem that nothing else does.

Carries the statement for the same reason `SpecRow` does, and more urgently. A characterization is
checked for *shape* and not for content, so the only thing that tells a reader whether it says
anything is the property's own body and the relation the uniqueness theorem stops at — both of
which are here. -/
structure CharPartRow where
  /-- `Property`, `Existence` or `Uniqueness`, as shown to the reader. -/
  role : String
  name : String
  /-- Empty when the declaration is not exposed and so has no page of its own. -/
  href : String := ""
  /-- The label shown to the reader (`displayKindLabel`). -/
  kind : String := ""
  /-- The author's note, from the attribute. Empty when they wrote none. -/
  comment : String := ""
  /-- On a uniqueness row, the relation it establishes, as written in its conclusion. Empty
  otherwise. -/
  relation : String := ""
  /-- The statement, source form. -/
  signature : String := ""
deriving Repr, ToJson, FromJson, Inhabited

/-- One characterization of a definition, as rendered. -/
structure CharRow where
  /-- The characterizing predicate, for the header sentence. -/
  property : String
  /-- The relations its uniqueness theorems establish, as written. Empty when there are none. -/
  relations : Array String := #[]
  /-- Whether a theorem states that the definition satisfies the property. -/
  hasExistence : Bool := false
  /-- Whether a theorem states that the property determines its subject.

  Kept apart from `hasExistence` rather than collapsed into one "complete" flag because the two
  gaps read differently and the card has to say which one it is: existence without uniqueness is a
  specification wearing a characterization's clothes, and uniqueness without existence is a claim
  about a property that may hold of nothing at all. -/
  hasUniqueness : Bool := false
  /-- The relations' own definitions, deduplicated, in the order the uniqueness theorems introduce
  them.

  Without these the banner names the claim's conclusion and does not say what it *is*:
  `Indistinguishable μ A ⟨M⟩` reads as reassurance whether it means "agree a.s. at every time" or
  something far weaker, and the reader cannot tell which without leaving the page. Since the
  relation is the one part of a characterization that is reported rather than checked, showing it
  is not a convenience.

  Empty for a relation from the toolchain — `=` and `↔` need no introduction, and printing
  `{α : Sort u} → α → α → Prop` where the point is to explain something would be noise. -/
  relationDefs : Array CharPartRow := #[]
  /-- The property, then the existence theorems, then the uniqueness theorems. -/
  parts : Array CharPartRow := #[]
deriving Repr, ToJson, FromJson, Inhabited

/-- Data container for `Block.charList`. -/
structure CharListData where
  entries : Array CharRow
deriving Repr, ToJson, FromJson, Inhabited

/-- One row of the Browse table: every exposed declaration, with the columns a reader sorts and
filters on. Deliberately light — no docstring or statement — since every row of the library rides
along in a single page. -/
structure BrowseRow where
  name : String
  href : String
  /-- Reader-facing kind (`displayKindLabel`). -/
  kind : String
  /-- `definition` / `lemma` / `theorem`, matching the sidebar's visibility toggles. -/
  group : String
  module : String
  chapter : String
  /-- Project declarations in its closure. -/
  deps : Nat
  /-- Distinct constants outside the project its closure bottoms out in. -/
  ext : Nat
  dependsOnSorry : Bool
  /-- Rests on an axiom beyond `Classical.choice`/`propext`/`Quot.sound`. -/
  extraAxioms : Bool
  /-- Theorems declared to be part of this declaration's specification. `none` for anything a
  specification cannot be about (see `DeclInfo.isDefinitionLike`), which is what lets the table
  distinguish "no specification" from "not the sort of thing that has one". -/
  specs : Option Nat := none
  /-- How it changed since the baseline (`ChangeKind.slug`), or `none` when the site was built
  without `--baseline`. The column and its filter exist only in the `some` case, so a site with no
  baseline is exactly the site it was before the field existed. -/
  change : Option String := none
  /-- What this declaration means now (`meaningKeyOf`), so the Verdict column can mark an
  acceptance recorded against a different meaning. Empty on a build without semantic hashes. -/
  meaning : String := ""
  /-- The revision at which its meaning last changed, or `none` without a provenance ledger — which
  is what makes the column and its sort disappear on a site that has none. -/
  changedRef : Option String := none
  /-- The date of that revision, `YYYY-MM-DD`, which is also what the column sorts on: it orders
  correctly as a string, and it is what a reader scans for. -/
  changedDate : String := ""
deriving Repr, ToJson, FromJson, Inhabited

/-- Data container for BrowseData. -/
structure BrowseData where
  rows : Array BrowseRow
  /-- The project name, which is the audit state's storage key.

  Carried here because the Verdict column needs it and this page has no other audit payload: the
  script that owns that state cannot look up a verdict without knowing which project's state to
  read, and it is deliberately the only thing that knows. -/
  project : String := ""
deriving Repr, ToJson, FromJson, Inhabited

/-- Which voice a stretch of text is in, and how to say so.

Nearly every word on this site is *derived*: the tool read the compiled library and wrote a label, a
count or a sentence about what it found. A few are not — someone wrote them, and a reader deciding
how much to believe needs to know which is which before reading, not after.

`voice` is the writer: `authors` for anything taken verbatim from the project (docstrings, module
docs, the README), `reader` for the reader's own notes. It is a string rather than an enumeration
because the list is open — an interpretation generated by a model is the next one, and it must be
addable without every consumer of this payload learning about it.

`label` is what the tool says the block is, in the tool's own voice, above the quoted text. Empty
where the block is one of many — a listing row, a hover, a one-sentence gloss — and the typeface
carries the attribution on its own. -/
structure VoiceData where
  voice : String
  label : String := ""
deriving Repr, ToJson, FromJson, Inhabited

/-- Data container for DetailsData. -/
structure DetailsData where
  summary : String
  /-- Rendered already open. The default is shut, which is what a fold is usually for; a chapter on
  the claims listing is the other case — folding it is for putting a chapter you are done with out
  of the way, not for hiding the page's contents until asked. -/
  startsOpen : Bool := false
  /-- Marks a fold whose summary is a heading rather than a control, so it can be styled as one. -/
  headingLevel : Option Nat := none
deriving Repr, ToJson, FromJson, Inhabited

/-- Data container for GraphNode. -/
structure GraphNode where
  id : String
  label : String
  kind : String
  status : String
  groupKey : String
  moduleName : String
  href : String
  /-- True for the declaration whose page this graph is on, so the reader can see at a glance
  which node the picture is about. False everywhere on the whole-repository graph. -/
  focus : Bool := false
  /-- The declaration's statement, source form, for the summary the graph shows under a clicked
  node until that node's own card arrives. -/
  signature : String := ""
  /-- The declaration's docstring, as written. Empty when it has none. -/
  doc : String := ""
  /-- What this declaration means now (`meaningKeyOf`), so the graph can mark the nodes a reader
  has accepted *without* marking the ones they accepted an earlier version of.

  The verdict itself lives in the browser and is never collected; only the key it has to be checked
  against travels with the node. Empty on a build without semantic hashes, which switches the
  staleness half of the check off exactly as it is switched off everywhere else. -/
  meaning : String := ""
  /-- The upstream package this node comes from, or `""` for a project declaration.

  Set on exactly the nodes that belong in the upstream *band* rather than in the dependency rows.
  They are all sinks — nothing in the graph precedes them — so they would otherwise pile into the top
  row and make it several thousand pixels wide; `graph.js` lays them out as a wrapped band grouped by
  this field instead. `status` says whether the package is audited (`"trusted"`/`"untrusted"`). -/
  upstream : String := ""
  /-- The package's depth in the workspace dependency graph (`packageRanks`), which is the order the
  band stacks in: a package sits above one that depends on it, so the band reads the same way the
  dependency rows below it do. -/
  upstreamRank : Nat := 0
  /-- Drawn without following its own dependencies, so nothing above it in the picture is its.

  A graph is normally closed downwards — every node's dependencies are drawn — and a reader is
  entitled to assume it. A view that stops somewhere on purpose (a characterization stops at the
  definition and its theorems) breaks that assumption, and an unmarked node whose parents happen to
  be absent is indistinguishable from one that rests on nothing. So the node is marked, the key
  explains the mark, and clicking it says so in as many words. -/
  unexpanded : Bool := false
deriving Repr, ToJson, FromJson

/-- Data container for GraphEdge. -/
structure GraphEdge where
  source : String
  target : String
deriving Repr, ToJson, FromJson

/-- A second node set for the same picture, offered to the reader as a switch.

The one case there is: a definition that carries a characterization rests, *as a claim*, on far less
than it rests on as a construction — building a stochastic integral is work, and recognising one is
a property and a relation. The two views answer "what do I have to accept to believe this was built"
and "what do I have to read to know what it is", and only drawing both makes the gap visible. -/
structure GraphView where
  /-- The switch's label. Short: it sits in a row of buttons. -/
  label : String
  /-- One sentence above the picture saying what this node set is and what it leaves out. Shown only
  while the view is selected, since it describes this view rather than the graph. -/
  note : String := ""
  /-- What to say when the reader clicks a node this view stopped at (`GraphNode.unexpanded`). Held
  on the view rather than on each node because it is one fact about where this view cuts, and
  writing it into every cut node would repeat the same sentence across the payload. -/
  unexpandedNote : String := ""
  nodes : Array GraphNode
  edges : Array GraphEdge
  /-- `edges` interned against `nodes`; see `GraphData.edgeIx`. -/
  edgeIx : Array Nat := #[]
  /-- The graph's nodes as `SiteContext.nodeIndex` numbers, positionally, when every one of them
  could be reduced to a number; `nodes` is then empty and the client rebuilds it from the shared
  tables. A node that no table can restore — an upstream constant the current flags do not ship —
  leaves the whole view in the `nodes` form instead, since a mixed encoding would cost more to say
  than it saves.

  Flat rather than an array of objects because after thinning a node *is* its number: writing
  `{"ix":12043}` spends thirteen bytes to say six, and there are thousands of them on a page. -/
  nodeIx : Array Nat := #[]
  /-- Positions in `nodeIx` of the focus node, and of the nodes a view stopped at — the two facts a
  thinned node still carries. Held as positions rather than as flags per node so that the common
  case, one focus and nothing cut, costs one number and one empty array. -/
  focusIx : Array Nat := #[]
  unexpandedIx : Array Nat := #[]
deriving Repr, ToJson, FromJson

/-- Data container for GraphData. -/
structure GraphData where
  nodes : Array GraphNode
  edges : Array GraphEdge
  /-- What a node stands for, singular. Used in the graph's own explanatory text, so that a graph
  of modules does not describe itself as a graph of declarations. -/
  unit : String := "declaration"
  /-- The project's own name, which labels the first of its dependency rows the way each upstream
  package labels the first row of its block. -/
  projectName : String := ""
  /-- The switch's label for `nodes`/`edges` themselves, which are always the first view. Empty when
  `views` is, and then no switch is drawn at all: a picture with one view needs no name for it. -/
  viewLabel : String := ""
  /-- The note for the first view, on the same terms as `GraphView.note`. -/
  viewNote : String := ""
  /-- The views offered *besides* `nodes`/`edges`. Empty on every graph but a characterized
  definition's, which is why the first view is left in place rather than folded into this array —
  the payload rides in every page and the common case must not pay for the rare one. -/
  views : Array GraphView := #[]
  /-- Chapter slugs whose declaration tables this graph's project nodes are looked up in; see
  `thinGraphNodes`. The page loads one `<script src>` per entry, and a node carrying only an `id`
  is meaningless without them, so this is emitted even though nothing draws it. -/
  tables : Array String := #[]
  /-- `edges`, interned: each consecutive pair is a source and a target index into `nodes`.

  An edge written out is two full declaration names — around 90 bytes for what a pair of small
  integers says, and there are more edges than nodes on any graph worth drawing. Interned, the same
  edge is about 6. Flat rather than an array of pairs because a JSON array of two-element arrays
  spends two brackets and a comma per edge on saying "pair" again.

  `edges` holds whatever could not be interned — an edge whose endpoint the graph never listed as a
  node, which `transitiveReduce` already tolerates — so the two are read together and neither is
  authoritative alone. -/
  edgeIx : Array Nat := #[]
  /-- The graph's nodes as `SiteContext.nodeIndex` numbers, positionally, when every one of them
  could be reduced to a number; `nodes` is then empty and the client rebuilds it from the shared
  tables. A node that no table can restore — an upstream constant the current flags do not ship —
  leaves the whole view in the `nodes` form instead, since a mixed encoding would cost more to say
  than it saves.

  Flat rather than an array of objects because after thinning a node *is* its number: writing
  `{"ix":12043}` spends thirteen bytes to say six, and there are thousands of them on a page. -/
  nodeIx : Array Nat := #[]
  /-- Positions in `nodeIx` of the focus node, and of the nodes a view stopped at — the two facts a
  thinned node still carries. Held as positions rather than as flags per node so that the common
  case, one focus and nothing cut, costs one number and one empty array. -/
  focusIx : Array Nat := #[]
  unexpandedIx : Array Nat := #[]
deriving Repr, ToJson, FromJson

/-- Drops the fields whose value carries no information, recursively.

Lean's derived `ToJson` writes every field, default or not, so a thinned node still spelled out
`"label":"","kind":"","status":""` and so on — around 120 bytes of nothing per node, which is most
of what thinning it saved. Every default in `GraphData`, `GraphNode`, `GraphEdge` and `GraphView` is
the empty string, `false`, `0` or the empty array, so dropping exactly those is what `FromJson` puts
back, and the round trip is unchanged.

`graph.js` reads these fields through `||` — an absent field and an empty one have always been the
same thing to it — so nothing on the other side has to know which of the two it got. -/
partial def compactJson : Json → Json
  | .obj fields =>
    let kept := fields.foldl (init := ([] : List (String × Json))) fun acc k v =>
      let v := compactJson v
      let empty :=
        v == Json.str "" || v == Json.bool false || v == Json.num 0 || v == Json.arr #[]
      if empty then acc else (k, v) :: acc
    Json.mkObj kept.reverse
  | .arr items => .arr (items.map compactJson)
  | j => j

/-- One end of a specification link, as written with the `@[specifies]` attribute of the
`Characterization` package: the declaration at the other end and the author's note on why the
theorem belongs in the specification (empty when they wrote none).

Used in both directions — on a theorem the `name` is the definition being specified, on a
definition it is a theorem specifying it — because both ends want the same comment. -/
structure SpecLink where
  name : Name
  comment : String := ""
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- A uniqueness theorem of a characterization, with the relation it stops at.

The relation is the whole load-bearing part and the reason it is carried as text rather than as a
name: `Characterization` reads it off the theorem's conclusion as written (`x = y`, `f =ᵐ[μ] g`,
`IsoRel a b`), which is what a reader needs to see, while the head constant is only good for
grouping. A characterization up to a coarse relation says correspondingly less, and nothing but
showing the relation can convey that. -/
structure CharUniqueness where
  name : Name
  /-- The relating conclusion as written, with the theorem's own variable names. -/
  relation : String := ""
  /-- Its head constant (`Eq`, `Filter.EventuallyEq`, …), anonymous when there is none. -/
  relationHead : Name := .anonymous
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- One characterization claimed for a definition, as written with the `@[characterization]`
attribute of the `Characterization` package: a predicate, the theorems saying the definition
satisfies it, and the theorems saying nothing else does.

Stronger than a `SpecLink` in exactly one way that matters to a reader, and it is worth being
precise about which. `@[specifies]` is an unchecked claim; the shapes here *are* checked — the
predicate really is a predicate on the definition's type, the existence theorem really states that
the definition satisfies it, the uniqueness theorem really relates two objects that satisfy it. What
is still not checked is whether the predicate says anything worth saying. So a complete bundle is
evidence, not proof, and the site has to print the property and the relation rather than merely
report that they exist. -/
structure CharBundle where
  /-- The characterizing predicate. -/
  property : Name
  /-- The author's note on the property, from the attribute. Empty when they wrote none. -/
  comment : String := ""
  /-- The theorems stating that the definition satisfies `property`, in declaration order. -/
  existence : Array Name := #[]
  /-- The theorems stating that `property` determines its subject, in declaration order. -/
  uniqueness : Array CharUniqueness := #[]
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- Whether both halves of the claim are present. A property with an existence theorem and no
uniqueness theorem says no more than a `@[specifies]` annotation does — the definition has the
property, and so, for all this says, might anything else. -/
def CharBundle.isComplete (b : CharBundle) : Bool :=
  !b.existence.isEmpty && !b.uniqueness.isEmpty

/-- The link from one of a characterization's three declarations back to the claim it is part of.

The reverse index of `characterizedBy`, computed by `attachCharacterizes`, and the reason a reader
who lands on `IsEntropy.unique` is told what it is for rather than left with a lemma about a
predicate. -/
structure CharPartLink where
  /-- The definition characterized. -/
  target : Name
  /-- The characterizing predicate. -/
  property : Name
  /-- `property`, `existence` or `uniqueness`. -/
  role : String
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- Fully collected metadata for one exposed declaration. -/
structure DeclInfo where
  name : Name
  moduleName : Name
  modulePath : String
  groupKey : String
  kind : DeclKind
  displaySignature : String
  expandedSignature : String
  docBlocks : Array (Block Manual)
  /-- The docstring as written, before markdown parsing. `docBlocks` is the rendered form and is
  the right thing for a page; this is kept for the places that need plain text, such as the
  dependency graph's node data, which is built as JSON rather than as Verso blocks. -/
  docText? : Option String := none
  proofText? : Option String
  source? : Option SourceInfo
  /-- True if the declaration was written with the `lemma` keyword (a `theorem` alias used in
  Mathlib to mark less central results). -/
  isLemma : Bool := false
  /-- True if the declaration was written with the `instance` keyword but was not classified as
  `.instance` by `declKindOf`. -/
  isInstanceDecl : Bool := false
  /-- True if the declaration comes from an `alias` command. Unlike a real theorem, its body is kept
  verbatim during extraction (`alias … := target`) rather than replaced by `sorry`, so its transitive
  closure must follow value dependencies (the alias target), not just type dependencies. -/
  isAlias : Bool := false
  /-- True if `sorryAx` occurs anywhere in the declaration's transitive closure — whether the
  `sorry` is its own or inherited from something it rests on. Computed with `Lean.collectAxioms`,
  so it sees through compiler-generated helpers and into upstream libraries alike. -/
  dependsOnSorry : Bool := false
  /-- True if this declaration's *own* type or body contains a `sorry`. `dependsOnSorry` without
  `hasOwnSorry` means the gap is inherited, and the site has to point at where it actually is
  rather than blame this declaration for it. -/
  hasOwnSorry : Bool := false
  /-- Every axiom the declaration's closure rests on, i.e. what `#print axioms` reports. Beyond
  `Classical.choice`/`propext`/`Quot.sound` these are assumptions a reader is being asked to
  grant, so they are reported rather than collapsed into a flag. -/
  axioms : Array Name := #[]
  /-- For a theorem carrying `@[specifies …]`: the definitions its author declared it to be part of
  the specification of, in the order written.

  Almost everything else on `DeclInfo` is derived from the environment; this is not. It is the
  author's editorial claim about which properties pin a definition down, read back from the
  environment extension the `Characterization` package writes, and there is no way to infer it.
  Empty for every declaration of a project that does not use that package — which is why nothing
  downstream treats its absence as an error. The named definition need not be exposed, or even
  belong to this project. -/
  specifies : Array SpecLink := #[]
  /-- For a definition: the exposed theorems that carry `@[specifies thisDeclaration …]`, in
  declaration order. The reverse index of `specifies`, computed by `attachSpecifiedBy`. -/
  specifiedBy : Array SpecLink := #[]
  /-- For a definition: the characterizations its author claims for it — the strictly stronger
  claim that a property does not merely hold of it but *determines* it, up to a stated relation.

  Read from the same `Characterization` extension as `specifies`, and empty for a project that does
  not use the attribute. Both theorems of a characterization also register as `@[specifies]`
  annotations, so everything here is visible in `specifiedBy` too; this field is what lets the site
  tell a definition that has been pinned down from one that has merely been described. -/
  characterizedBy : Array CharBundle := #[]
  /-- For a declaration that is one of the three parts of a characterization: which claims it
  belongs to and in what role. The reverse index of `characterizedBy`, computed by
  `attachCharacterizes`. -/
  characterizes : Array CharPartLink := #[]
  /-- The upstream packages this declaration *directly* references, after `attachUpstreamPackages`
  has propagated them along the project's own dependency edges.

  "Directly" is the important word: these are the packages some constant of the declaration's
  project-level closure names, not the full set it rests on. The site closes them over the Lake
  dependency graph to get that — see the note on upstream packages above for why the two agree.

  Follows `meaningDeps`: a theorem contributes what its *statement* mentions, not what its proof
  calls. An upstream proof is not a trust dependency — the kernel rechecked it, and anything left
  unproved in it surfaces as a `sorry` or an extra axiom, both of which `axioms` already reports
  transitively. What cannot be checked for you is an upstream *definition* your statement is about. -/
  upstreamPackages : Array Name := #[]
  /-- The declaration's rename-invariant *semantic* hash, read from a `semantic_hash export` file
  (`collect --hashes`). Fixed-width hex, so it reads as an identifier rather than as a number
  someone might compare with `<`.

  Structural over the elaborated `Expr`, and — the property everything downstream rests on —
  **deep**: a referenced constant contributes *its* hash rather than its name, so this changes when
  the meaning of anything in the declaration's closure changes, upstream included. Invariant to
  renaming, to binder names, to `mdata`, and to how anything pretty-prints.

  `none` for a project collected without `--hashes`, and for any declaration the export did not
  cover; `Referee.Diff` falls back to comparing text per declaration, so absence degrades rather
  than breaks. -/
  semanticHash? : Option String := none
  /-- The same hash with theorem bodies hidden, so a theorem hashes by its *proposition*: proof
  subterms contribute the hash of the proposition they prove rather than of the term.

  This is `meaningDeps` computed at the `Expr` level by an independent implementation — a theorem's
  proof-irrelevant hash depends on its statement's closure and on nothing its proof merely calls —
  which is why the revision diff can use it directly as "did the meaning move". The pair
  (`semanticHash?` differs, this one does not) is exactly a proof-only change. -/
  proofIrrelHash? : Option String := none
  deps : Array Name
  typeDeps : Array Name := #[]
  /-- `deps` with the proofs inside the value skipped: what the declaration's statement and *data*
  rest on. See `MeaningGraph.dataValueConstants` for why a bundled structure instance's proof fields
  are not part of its meaning, and `meaningDeps` for where this is used.

  Differs from `deps` only for `def`/`abbrev`/`instance`; equal to it for everything else. -/
  dataDeps : Array Name := #[]
  usedBy : Array Name := #[]
  /-- The transitive closure of `closureDeps`, topologically ordered. **Derived, not stored**: since
  format version 12 `collect` leaves this empty and `CollectedData.withClosures` recomputes it from
  the direct edges on every load. Measured on `Mathlib.Analysis`, materialized closures were 69.9%
  of `data.json` and the reason `collect` could not fit in memory at whole-Mathlib scale; the
  direct edges they are derived from were 12.6%. -/
  transDeps : Array Name := #[]
  /-- The transitive closure of `meaningDeps`, topologically ordered, as `transDeps` is of
  `closureDeps`. Kept separate rather than replacing `transDeps` because `ChallengeGen` seeds each
  standalone file's `keep` set from `transDeps`, and a file whose kept tactic bodies lost the lemmas
  they call would no longer compile.

  Derived on load exactly as `transDeps` is; see there. -/
  dataTransDeps : Array Name := #[]
  /-- The statement taken apart by binder role — see `StatementAnatomy` — for a declaration whose
  conclusion is a proposition, and `none` for everything else. -/
  anatomy? : Option StatementAnatomy := none
deriving Repr, ToJson, FromJson

/-- The kind label to show for this declaration; see `displayKindLabel`. -/
def DeclInfo.displayKind (decl : DeclInfo) : String :=
  displayKindLabel decl.kind.label decl.isLemma decl.isInstanceDecl

/-- Whether this declaration is the kind of thing a specification can be *about*: something whose
meaning is chosen rather than proved.

Drives every "definitions without a specification" count, so what it excludes matters as much as
what it includes. Theorems are excluded because their meaning is their statement. Axioms are
excluded because an axiom *is* an assumption and the trust page already reports it as one.
Instances are excluded because a library has a great many of them, they are overwhelmingly
plumbing, and listing each one as an unspecified definition would bury the definitions that
actually want a specification. -/
def DeclInfo.isDefinitionLike (decl : DeclInfo) : Bool :=
  !decl.isInstanceDecl &&
    match decl.kind with
    | .definition | .structure | .typeclass | .inductive | .opaque => true
    | .theorem | .axiom | .instance => false

/-- Whether this is one of the library's *claims*: a result written with the `theorem` keyword
rather than `lemma`.

The one piece of editorial intent the tool cannot derive — Lean records both keywords as the same
kind — so it is read from the author's own signal and taken at face value. See `claimsOf` in
`Website/Site.lean` for what rests on it and why a derived rule was rejected. -/
def DeclInfo.isClaim (decl : DeclInfo) : Bool :=
  decl.kind == .theorem && !decl.isLemma && !decl.isInstanceDecl

/-- Whether a declaration's *body* is part of what it means, as opposed to being a proof the kernel
has already checked.

The same rule `meaningDepsOf` applies to dependency edges, applied here across revisions instead:
changing a definition's body changes the meaning of every statement about it, while changing a
theorem's proof changes nothing a reader has to re-read. An `alias` counts as a definition for this
purpose for the reason recorded on `DeclInfo.isAlias` — its body is kept verbatim. -/
def DeclInfo.bodyIsMeaning (decl : DeclInfo) : Bool :=
  decl.kind != .theorem || decl.isAlias

/-- Exposed declarations grouped by Lean module. -/
structure ModuleInfo where
  name : Name
  path : String
  groupKey : String
  decls : Array DeclInfo
  docBlocks : Array (Block Manual) := #[]
deriving Repr, ToJson, FromJson

/-- Modules grouped by top-level chapter key. -/
structure GroupInfo where
  key : String
  modules : Array ModuleInfo
deriving Repr, ToJson, FromJson

/-! ## Upstream packages

The project is not the whole of what a reader is asked to trust. `AlphaRAR` rests on
`LeanMachineLearning`, which rests on `mathlib`, and a referee may well have audited one and not the
other. Nothing else on the site says so: every measure here stops at the project boundary and
treats everything beyond it as given.

What is and is not a trust dependency upstream is worth being precise about, because the obvious
answer is wrong. An upstream *proof* needs no trust at all: the kernel rechecked it, and anything
left unproved in it arrives as a `sorry` or an extra axiom, both of which `axioms` and
`dependsOnSorry` already report transitively — through upstream packages included. So a theorem
whose proof calls a `LeanMachineLearning` lemma has learned nothing it needs to take on faith from
that call.

What does need trust is an upstream *definition* that a statement is about. If a theorem's statement
mentions `Learning.IsAlgEnvSeq`, then what the theorem *means* depends on that definition being the
intended one, and no proof anywhere settles that — it is the same gap `@[specifies]` exists to
record, one package up. That is why the edges followed here are `meaningDeps`: a theorem contributes
its statement, everything else contributes its body too, since a definition's body is its meaning.

What is recorded is deliberately package-granular rather than constant-granular, and the reason is
cost. `Lean.collectAxioms` gets away with a full closure walk per declaration only because axioms
for imported constants are precomputed in an environment extension, so the walk stops at the project
boundary; a genuine walk into Mathlib, 784 times over, is not affordable. Package granularity is
also *sound* to close transitively, which is what makes the cheap version correct rather than merely
cheap: a constant can only reference what its own package imports, so if a declaration's closure
reaches package `Q`, then `Q` is reachable in the Lake dependency graph from a package the
declaration references directly. Recording the directly-referenced packages and closing over the
Lake graph at render time therefore cannot miss a dependency — the direction that matters, since
under-reporting here would mean telling a reader they do not rest on code they do.
-/

/-- A package of the target's Lake workspace, as much of it as the audit needs.

`Lean` is the pseudo-package standing for the toolchain (`Init`, `Std`, `Lean`, `Lake`), which
belongs to no Lake package. Modelling it as one keeps module attribution uniform — it is matched by
root prefix like any other — and gives the trust graph a root to bottom out in. -/
structure PackageInfo where
  name : Name
  /-- Direct dependencies, by name, as declared in the workspace. -/
  deps : Array Name := #[]
  /-- The library roots the package declares, which is how a module is attributed to it. -/
  roots : Array Name := #[]
  /-- True for the project being exposed, which is never "upstream" of itself. -/
  isProject : Bool := false
  /-- True for the `Lean` pseudo-package. Always trusted: it is the compiler that checked
  everything else, so trusting it is not a choice a site can offer. -/
  isToolchain : Bool := false
deriving Repr, BEq, ToJson, FromJson, Inhabited

/-- An upstream constant a project statement names, with enough of it to be read in place.

These are the nodes a declaration's graph bottoms out in, and until now they were drawn with nothing
but their name: the graph showed the name again where a signature belongs and a canned sentence
where the docstring belongs. A reader asking "is this statement about the definition I think it is"
— the question the whole site exists to serve — could not answer it without leaving for another
site. The signature and docstring come straight out of the imported environment, which already has
both.

Not attached to `DeclInfo`: one upstream constant is named by many declarations, so this is a table
keyed by name, emitted once. -/
structure ExternalDeclInfo where
  name : Name
  /-- The package it comes from, as `PackageInfo.name`. -/
  package : Name
  /-- The module declaring it, for the graph's provenance line. -/
  moduleName : Name
  /-- Its pretty-printed type. -/
  signature : String
  /-- What it *says*, beyond the shape of its arguments: a definition's value, or a structure's
  fields. Empty for a theorem, whose type already is its statement, and for anything with no body to
  show.

  Without this the graph answers the wrong question for a definition. `Filter.Tendsto`'s type is
  `(α → β) → Filter α → Filter β → Prop`, which says it takes a function and two filters and yields a
  proposition — every argument reading as a hypothesis, and no hint that it *means* `map f l₁ ≤ l₂`.
  Since the whole point of these nodes is "is this the definition I think it is", the type alone
  cannot answer it. -/
  value : String := ""
  /-- Its docstring, or `""` when it has none — the graph distinguishes the two. -/
  doc : String := ""
  /-- Its own meaning edges, restricted to *its own package*, so the graph can draw an unaudited
  package's internal structure rather than a flat row of names. Empty unless the package was expanded
  (`CollectedData.expandedPackages`). Edges leaving the package are deliberately absent: they would
  reach either the project — which depends on the package, not the reverse — or a further package,
  whose own expansion is a separate question. -/
  deps : Array Name := #[]
deriving Repr, ToJson, FromJson, Inhabited

/-! ## Interning: sharing the collected data's repeated subtrees

The serialized data is dominated by repetition, and overwhelmingly in one field. Measured on
`brownian-motion` (1808 declarations, 67 MB): `DeclInfo.docstringBlock?` is 56.6 MB of the 73.5 MB
`decls` array — 77% — and inside it 19.2 MB is repeated JSON field names while 11.0 MB is the
docstrings of upstream constants, inlined once per *mention*: 54,778 occurrences of 1,014 distinct
strings, with `MeasurableSpace`'s docstring stored 2,770 times.

None of that is information. `intern` replaces every repeated subtree with an index into a table
carried alongside the data. On that project: **67.2 MB → 21.5 MB** (3.1×).

The reason this is worth a format change rather than just compressing the file — which would do
better on bytes, 13× — is that it shrinks the data *in memory* too, and memory is the wall a large
library hits first. `resolve` rebuilds each table entry exactly once, so every reference to it yields
the same `Json` value rather than a copy, and the sharing survives decoding wherever a field is a
`String` (`getStr?` hands back the existing object). Rendering the same site from the interned and
un-interned forms of one file, measured:

|  | file | peak RSS | wall |
|---|---|---|---|
| un-interned | 67.2 MB | 1022 MB | 13.9 s |
| interned | 21.5 MB | **532 MB** | 12.8 s |

Byte-identical output, half the memory, and slightly faster despite the extra pass — parsing a third
as much JSON more than pays for resolving it. Gzip would give neither of the last two.
-/

/-- The reserved object key marking a reference into the subtree table: `{"$i": 12}`.

A single character keeps the marker at nine bytes, which matters because references are the most
numerous thing in the encoded form. No Lean structure field or `Name` component can produce it, but
`intern` checks rather than assuming (see `usesInternKey`). -/
def internKey : String := "$i"

/-! ### Recursing over `Json` without `partial`

The three functions below walk a `Json` tree. Every recursive call is on a strict subterm, but Lean
cannot see that on its own: `Json` is a *nested* inductive whose object case holds a
`Std.TreeMap.Raw`, and folding over that tree hands the termination checker a value with no evidence
tying it to the tree. `Array` and `List` ship `sizeOf_lt_of_mem`; the tree containers do not. That
single gap is why every recursion over `Json` in Lean core — `beq'`, `hash'`, `render`, `compress` —
is `partial`.

The two lemmas here close it, and the walks below are therefore ordinary total definitions with
equations a proof can use. That matters because this is the on-disk format: `Proofs/Collect.lean`
proves that `resolve` inverts `intern`, which is not a statement one can even *make* about a
`partial def`. -/

/-- Values stored in a tree map are strict subterms of it, over the structural flattening
`toListModel` that core defines for verification. No well-formedness hypothesis: this is about the
tree's shape, not its ordering. -/
theorem sizeOf_lt_of_mem_toListModel {m : Std.DTreeMap.Internal.Impl String (fun _ => Json)}
    {p : (_ : String) × Json} (h : p ∈ m.toListModel) : sizeOf p.2 < sizeOf m := by
  induction m with
  | leaf => simp at h
  | inner sz k v l r ihl ihr =>
    rw [Std.DTreeMap.Internal.Impl.toListModel_inner] at h
    rcases List.mem_append.mp h with h' | h'
    · have := ihl h'; simp; omega
    · rcases List.mem_cons.mp h' with rfl | h''
      · simp; omega
      · have := ihr h''; simp; omega

/-- The same for the public `toList`, which is what the walks below iterate. This is the fact
`decreasing_by` needs in every object case. -/
theorem objPairs_sizeOf {fields : Std.TreeMap.Raw String Json} {p : String × Json}
    (h : p ∈ fields.toList) : sizeOf p.2 < sizeOf fields := by
  obtain ⟨⟨impl⟩⟩ := fields
  rw [Std.TreeMap.Raw.toList, Std.DTreeMap.Raw.Const.toList,
    Std.DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map] at h
  obtain ⟨q, hq, rfl⟩ := List.mem_map.mp h
  have := sizeOf_lt_of_mem_toListModel hq
  simp at this ⊢
  omega

/-- True if any object in `j` already uses `internKey`.

`intern` refuses to encode such a document, because a payload object of exactly that shape would be
indistinguishable from a reference and would decode to something else entirely. Nothing Referee
serializes can produce the key, so this is a guard against a future field, not a live case. -/
def usesInternKey (j : Json) : Bool :=
  match j with
  | .obj fields => fields.toList.attach.any fun p => p.1.1 == internKey || usesInternKey p.1.2
  | .arr elems => elems.attach.any fun e => usesInternKey e.1
  | _ => false
termination_by sizeOf j
decreasing_by
  · have := objPairs_sizeOf p.2; simp; omega
  · have := Array.sizeOf_lt_of_mem e.2; simp; omega

/-- Smallest compressed size, in bytes, a subtree must reach before it is worth interning.

Chosen by measurement, not reasoning: the size/threshold curve is not monotonic, because interning
small nodes shrinks their parents, which makes *those* collide with each other in turn. On
`brownian-motion` the whole 10–20 range sits on one plateau at 3.17× and the cliff is at 22, where
the token objects that make up the bulk of a signature stop qualifying:

| threshold | 14 | 20 | 22 | 32 | 64 |
|---|---|---|---|---|---|
| factor | 3.17× | 3.18× | 2.95× | 2.40× | 2.14× |

20 is the top of the plateau, which is where the same file size comes with the fewest table entries
(76k rather than 80k) and so the least work in both `internAux` and `resolve`. Below about 10 nothing
can pay for itself anyway: a reference is nine bytes. -/
def internMinSize : Nat := 20

/-- Encoder state: the table in construction, and the reverse index that makes a repeat an O(1)
lookup rather than a scan.

The index is keyed on the *already-interned* node, so `Json`'s recursive `BEq`/`Hashable` only ever
walk a node's own fields plus its children's nine-byte references — never a whole subtree. That is
what keeps the pass linear in the document rather than quadratic in its depth. -/
structure InternState where
  table : Array Json := #[]
  index : Std.HashMap Json Nat := {}

/-- Interns one node, bottom-up: children first, then the node itself if it is large enough to pay
for a reference.

Because children are interned before their parent, every reference inside table entry `i` points to
an index below `i`. `resolve` relies on that ordering to rebuild the table in one forward pass. -/
def internAux (j : Json) (st0 : InternState) : Json × InternState :=
  let (node, st) : Json × InternState :=
    match j with
    | .arr elems =>
      let (out, st) := elems.attach.foldl (init := ((#[] : Array Json), st0))
        fun (acc : Array Json × InternState) e =>
          let (e', st') := internAux e.1 acc.2
          (acc.1.push e', st')
      (Json.arr out, st)
    | .obj fields =>
      -- `toList` is ascending by key, the order the previous `fields.foldl` produced; `out` is built
      -- reversed and handed to `mkObj`, which re-sorts, so the object is unchanged either way.
      let (out, st) := fields.toList.attach.foldl (init := (([] : List (String × Json)), st0))
        fun (acc : List (String × Json) × InternState) p =>
          let (v', st') := internAux p.1.2 acc.2
          ((p.1.1, v') :: acc.1, st')
      (Json.mkObj out, st)
    | leaf => (leaf, st0)
  -- A leaf is never tabled. `internMinSize` excludes every number and boolean, and a string long
  -- enough to qualify is already shared by the parse rather than copied per occurrence.
  let isComposite := match node with | .arr _ | .obj _ => true | _ => false
  if !isComposite || node.compress.length < internMinSize then
    (node, st)
  else
    match st.index[node]? with
    | some i => (Json.mkObj [(internKey, toJson i)], st)
    | none =>
      let i := st.table.size
      (Json.mkObj [(internKey, toJson i)],
        { table := st.table.push node, index := st.index.insert node i })
termination_by sizeOf j
decreasing_by
  · have := Array.sizeOf_lt_of_mem e.2; simp; omega
  · have := objPairs_sizeOf p.2; simp; omega

/-- Replaces every repeated subtree of `j` with a reference into a table, returning the table and the
rewritten document. Returns an empty table and `j` unchanged when `usesInternKey` says the document
could not be decoded unambiguously. -/
def intern (j : Json) : Array Json × Json :=
  if usesInternKey j then
    (#[], j)
  else
    let (root, st) := internAux j {}
    (st.table, root)

/-- Substitutes references in `j` against an already-resolved table.

A reference is an object whose only field is `internKey` carrying a whole number in range; anything
else is real data and is rebuilt field by field. An out-of-range index is left alone rather than
raising, which is what lets a document with an empty table round-trip unchanged. -/
def resolveAgainst (resolved : Array Json) (j : Json) : Json :=
  match j with
  | .arr elems => .arr (elems.attach.map fun e => resolveAgainst resolved e.1)
  | .obj fields =>
    let ref? : Option Nat := do
      let .num n ← fields.get? internKey | none
      guard (n.exponent == 0)
      guard (n.mantissa ≥ 0)
      let i := n.mantissa.toNat
      guard (i < resolved.size)
      pure i
    match ref? with
    | some i => resolved[i]!
    | none =>
      Json.mkObj <| (fields.toList.attach.foldl (init := (#[] : Array (String × Json)))
        fun acc p => acc.push (p.1.1, resolveAgainst resolved p.1.2)).toList
  | leaf => leaf
termination_by sizeOf j
decreasing_by
  · have := Array.sizeOf_lt_of_mem e.2; simp; omega
  · have := objPairs_sizeOf p.2; simp; omega

/-- Rebuilds a document `intern` encoded, resolving each table entry exactly once so that every
reference to it yields the *same* `Json` value.

That single-allocation property is the point, not merely the smaller file: the decoded tree shares
its repeated subtrees by pointer instead of holding a copy per occurrence. The forward pass is sound
because `internAux` tables children before parents, so entry `i` only ever references entries below
`i`, which are already resolved when it is reached. -/
def resolve (table : Array Json) (j : Json) : Json :=
  let resolved := table.foldl (init := (#[] : Array Json)) fun acc entry =>
    acc.push (resolveAgainst acc entry)
  resolveAgainst resolved j

/-! ## The thin tier

A scoped build drops 93–98% of the library, and two analyses would notice if the dropped
declarations vanished entirely rather than thinning: the extraction closure a minimal file inlines
along, and the `sorry` chain that explains a finding. Both need names and edges; neither needs a
signature, a docstring, an anatomy or a line of source.

So they get a record that cannot be rendered. That is deliberate and is why this is a separate array
rather than a partly-filled `DeclInfo`: a thin record that reached a page would draw an empty card,
and keeping the two types apart makes that impossible instead of merely unlikely.

Measured, this tier is one declaration on `colt-2026-83` and none on `alpha-rar`. It is a
correctness backstop, not a carrier of bulk. -/

/-- A declaration a scoped build keeps the edges of but renders nothing for. -/
structure ThinDecl where
  name : Name
  moduleName : Name
  kind : DeclKind
  /-- Needed because `closureDepsOf` and `meaningDepsOf` both branch on it. -/
  isAlias : Bool := false
  deps : Array Name := #[]
  typeDeps : Array Name := #[]
  /-- Whether the `sorry` is this declaration's own, which is where a chain stops. -/
  hasOwnSorry : Bool := false
  /-- Whether one is anywhere beneath it, which is what makes it a possible link in a chain. -/
  dependsOnSorry : Bool := false
deriving Repr, ToJson, FromJson, Inhabited

/-- How a `data.json` was scoped, so a later run can tell whether it is comparing like with like.

`--baseline` is the reason this is stored rather than inferred. A scoped file compared against a
full-scope one reports every dropped declaration as removed — 1864 false "this was deleted" rows on
`colt-2026-83` — and the only thing that can catch it is the two files saying how they were made. -/
structure CollectionScope where
  /-- `""` for a full build, `"claims"` for `--claims-only`, `"single"` for `--only`. -/
  mode : String := ""
  /-- The declarations the scope was seeded from, in order. Part of the identity of the scope: two
  `--claims-only` builds of different claim sets are not comparable either. -/
  seeds : Array String := #[]
deriving Repr, ToJson, FromJson, Inhabited, BEq

/-- Whether this build kept the whole library. -/
def CollectionScope.isFull (scope : CollectionScope) : Bool := scope.mode.isEmpty

/-- What to call the scope in a sentence. -/
def CollectionScope.label (scope : CollectionScope) : String :=
  if scope.mode == "claims" then "claims-only"
  else if scope.mode == "single" then "single-declaration"
  else "full"

/-- Format version of `CollectedData`. Bump whenever `DeclInfo` or `CollectedData` gains or
changes a field, so that `build-site` fails with an actionable message rather than a field-level
decode error when handed a JSON file written by an older `collect`.

- 1: initial
- 2: adds `DeclInfo.hasOwnSorry` and `DeclInfo.axioms`
- 3: adds `DeclInfo.docText?`
- 4: adds `DeclInfo.specifies` and `DeclInfo.specifiedBy`
- 5: adds `CollectedData.packages` and `DeclInfo.upstreamPackages`
- 6: adds `DeclInfo.semanticHash?` and `DeclInfo.proofIrrelHash?`
- 7: adds `DeclInfo.dataDeps` and `DeclInfo.dataTransDeps`
- 8: replaces `CollectedData.externalPackages` with `externalDecls`, which carries the signature and
  docstring of each upstream constant as well as its package
- 9: adds `ExternalDeclInfo.value`/`deps` and `CollectedData.expandedPackages`, the internal
  structure of the upstream packages small enough to walk
- 10: adds `DeclInfo.characterizedBy` and `DeclInfo.characterizes`
- 11: wraps the document in an `InternedData` envelope, sharing its repeated subtrees (see `intern`).
  No field of `CollectedData` changed; what changed is how it is written and read
- 12: stops storing `DeclInfo.transDeps` and `DeclInfo.dataTransDeps`; every consumer recomputes
  them from the direct edges via `CollectedData.withClosures` on load. No field was removed, so a
  version-11 file still decodes — its stored closures are simply ignored in favor of the recomputed
  ones, which is why `minReadableDataVersion` stays at 11. The bump exists for the other direction:
  an older binary handed a version-12 file must refuse it rather than silently render the empty
  closures it carries.
- 13: adds `CollectedData.formalization?`, the project's own `formalization.yaml` — the first input
  that is neither the compiled environment nor derived from it. Absent for every project that has no
  such file, which is why `minReadableDataVersion` stays at 11: an older file decodes with the field
  at its `none` default, which is exactly right for a project that had none
- 14: adds `DeclInfo.anatomy?`, the statement split by binder role for the card's "in parts" view.
  Optional for the same reason, so `minReadableDataVersion` stays at 11; an older file renders
  without the section -/
def collectedDataVersion : Nat := 16

/-- The oldest data-format version the current binary can read. Version 11 remains readable because
the only change in 12 is that closures are no longer stored, and this binary recomputes them from
the direct edges regardless of what the file carries — so an old `--baseline` keeps working. -/
def minReadableDataVersion : Nat := 11

/-- The full result of the `collect` subcommand's analysis, persisted as JSON so `extract`
and `build-site` can run without re-importing the target project. `moduleOrder` and
`moduleDocs` are flattened to arrays (rather than `Std.HashMap`) purely for JSON-friendliness;
reconstruct the map at the consuming end. -/
structure CollectedData where
  version : Nat := collectedDataVersion
  rootPrefix : Name
  decls : Array DeclInfo
  moduleOrder : Array (Name × Nat)
  moduleDocs : Array (Name × Array (Block Manual))
  readmeText : Option String
  /-- The project's `formalization.yaml`, when it has one: the Palomar registry's metadata document,
  read for the results the project itself puts forward as the point of it.

  The one field here that is not derived from the compiled environment. It is collected rather than
  read at render time for the same reason `readmeText` is — `build-site` runs from `data.json` alone
  and never sees the project directory — and it is an `Option` rather than a default-empty record so
  that "the project has no such file" and "the file declares no main results" stay distinguishable:
  the first means the Claims page does not apply, the second that it has nothing to say. -/
  formalization? : Option Formalization := none
  /-- The workspace's packages and their dependency edges, the graph `--trust` closes over. -/
  packages : Array PackageInfo := #[]
  /-- The packages with code actually loaded in the imported environment. See `loadedPackagesOf`:
  this is what stops a declared-but-unused dependency from being reported as trusted-or-not. -/
  loadedPackages : Array Name := #[]
  /-- The upstream constants project statements name, with what a reader needs in order to read one:
  its package, its module, its signature and its docstring. See `externalDeclsOf`. -/
  externalDecls : Array ExternalDeclInfo := #[]
  /-- The upstream packages whose internal structure was collected, i.e. those whose closure fitted
  inside `maxExpandedPackage`. Their declarations carry `ExternalDeclInfo.deps` and are drawn as a
  layered block; everything else is drawn as the flat surface it always was. -/
  expandedPackages : Array Name := #[]
  /-- How this file was scoped. Defaulted, so a file from before the field existed reads as the
  full build it was. -/
  scope : CollectionScope := {}
  /-- The results the project puts forward, when something named them. Read at `collect` time for
  the same reason `formalization?` is: `build-site` runs from this file alone and never sees the
  project directory. Present on a full build too, where it drives the Claims page and nothing
  else. -/
  claims? : Option ClaimSet := none
  /-- Exposed declarations *before* scoping. The number a scoped site needs in order to say what it
  left out, and the one thing a scoped file cannot recompute. Zero on a full build, where
  `decls.size` is already the answer. -/
  libraryDeclCount : Nat := 0
  /-- The declarations a scoped build keeps the edges of and renders nothing for; see `ThinDecl`.
  Always empty on a full build. -/
  thinDecls : Array ThinDecl := #[]
deriving ToJson, FromJson

/-- What `collect` actually writes: a `CollectedData` with its repeated subtrees hoisted into
`interned` and replaced by references. See `intern` for why.

`version` is duplicated here rather than only inside `data` so that `loadCollectedData` can reject a
stale file by reading one top-level field, without decoding — or even resolving — the rest. -/
structure InternedData where
  version : Nat := collectedDataVersion
  /-- The shared subtree table. Entry `i` may reference only entries below `i`. Empty when interning
  was skipped, in which case `data` is an ordinary `CollectedData` document. -/
  interned : Array Json := #[]
  data : Json
deriving ToJson, FromJson

/-- Serializes `data`, interned. -/
def encodeCollectedData (data : CollectedData) : Json :=
  let (interned, root) := intern (toJson data)
  toJson { interned, data := root : InternedData }

/-- Inverse of `encodeCollectedData`. Separated from the file reading so it can be round-trip tested
without touching the disk. -/
def decodeCollectedData (json : Json) : Except String CollectedData := do
  let envelope : InternedData ← fromJson? json
  fromJson? (resolve envelope.interned envelope.data)

/-- Command-line usage text shown for invalid arguments. -/
def usage : String :=
  String.intercalate "\n" [
    "Usage: lake exe referee [SUBCOMMAND] [options]",
    "",
    "Subcommands:",
    "  collect              Import the target project and write collected declaration data as JSON.",
    "  extract              Read collected data and write standalone per-declaration .lean files.",
    "  extract-flat         Same, but rendered from the compiled environment instead of from",
    "                       source: unreadable but far more robust, as a fallback for files",
    "                       `extract` cannot make compile. Writes to <output>/html-multi/",
    "                       extracted-flat.",
    "  highlight-extracted  Elaborate each extracted minimal .lean file and write its highlighting,",
    "                       plus whether it compiles, to <output>/extracted-highlighting. Requires",
    "                       `extract` to have run first.",
    "  provenance           Fold this revision into the provenance ledger: when each declaration's",
    "                       meaning last changed, and where its source was last edited. Needs a git",
    "                       working tree and semantic hashes, but no Lean environment.",
    "  build-site           Read collected data and render the Verso HTML site (no Lean env",
    "                       needed).",
    "  all                  Run collect, extract, and build-site in one process, without a JSON",
    "                       round-trip (default when no subcommand is given, for backward",
    "                       compatibility). Does not include `highlight-extracted`.",
    "",
    "  highlight-file is the internal worker behind `highlight-extracted`; it processes a",
    "  single file and is not meant to be invoked directly.",
    "",
    "Options:",
    "  --root PREFIX        Root module prefix to expose (default: first root library)",
    "  --repo-url URL       GitHub repo URL used for issue/source links",
    "  --site-url URL       Deployed site base URL, used to link the minimal Lean files into the",
    "                       live.lean-lang.org web editor",
    "  --title TITLE        Site title override",
    "  --output DIR         Output directory passed to Verso",
    "  --exclude-lib NAME   Exclude a root library when importing the target project",
    "  --data PATH          Collected-data JSON file: written by `collect`, read by `extract`",
    "                       and `build-site`",
    "  --jobs N             Worker processes to run at once in `highlight-extracted`",
    "                       (default: CPU count)",
    "  --no-verify          Skip the integrity re-check of the collected data on load",
    "  --trust PKG          Treat this upstream package, and everything it depends on, as",
    "                       audited. Repeatable. Anything left untrusted is reported on the",
    "                       trust page and on the pages of the declarations that rest on it",
    "  --show-trusted-upstream",
    "                       Also draw declarations from audited packages in each graph's upstream",
    "                       band. Off by default: unaudited packages are always drawn, and they",
    "                       are what the band exists to show",
    "  --baseline PATH      An earlier `collect` output to compare against. Adds a Changes page,",
    "                       a badge on every declaration, and a Browse column saying what a",
    "                       reader of that revision has to read again. Omit it and the site says",
    "                       nothing about revisions",
    "  --baseline-label S   What to call the baseline on the page (default: its file name)",
    "  --hashes PATH        JSONL written by `semantic_hash export`, giving each declaration a",
    "                       rename-invariant semantic hash. Read by `collect` and stored in the",
    "                       data file, where it becomes the key the revision diff compares on",
    "                       instead of pretty-printed types. Optional",
    "  --provenance PATH    The provenance ledger: when each declaration's meaning last changed,",
    "                       and in which revision. Written and extended by `provenance`, read by",
    "                       `build-site`. Optional; without it the site says nothing about when",
    "                       anything changed",
    "  --ref NAME           What to call this revision in the ledger (default: git describe)",
    "  --claims-only        Build only the results the project puts forward (formalization.yaml's",
    "                       status.main_results, or a Comparator setup) and the declarations their",
    "                       statements rest on. Read by `collect`, recorded in the data file",
    "  --only DECL          Build the site for this one declaration: --claims-only with a claim",
    "                       set of one, so everything its statement rests on gets a page too",
    "  --claim NAME         Treat NAME as a main result, instead of whatever the project's",
    "                       metadata says. Repeatable. Needs --claims-only or --only",
    "  --comparator DIR     Where the Comparator configs are, when neither formalization.yaml nor",
    "                       a shallow scan of the project root finds them",
    "  --per-chapter        Render the site one chapter at a time, bounding `build-site`'s peak",
    "                       memory by the largest chapter instead of the whole library, then stitch",
    "                       the global artifacts together",
    "  --input FILE         Internal: the file `highlight-file` should process",
  ]

/-- Parses CLI arguments into `Cli`, or returns a usage error. -/
def parseArgs : List String → Except String Cli
  | [] => .ok {}
  | "--root" :: root :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with rootPrefix := some root.toName }
  | "--repo-url" :: url :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with repoUrl := some url }
  | "--site-url" :: url :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with siteUrl := some url }
  | "--title" :: title :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with siteTitle := some title }
  | "--output" :: out :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with outputDir := some out }
  | "--exclude-lib" :: lib :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with excludeLibs := cfg.excludeLibs.push lib.toName }
  | "--data" :: path :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with dataPath := some path }
  | "--input" :: path :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with inputPath := some path }
  | "--jobs" :: n :: rest => do
      let some n := n.toNat?
        | .error s!"--jobs expects a number, got: {n}"
      let cfg ← parseArgs rest
      pure { cfg with jobs := some n }
  | "--trust" :: name :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with trustedPackages := cfg.trustedPackages.push name.toName }
  | "--show-trusted-upstream" :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with showTrustedUpstream := true }
  | "--baseline" :: path :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with baselinePath := some path }
  | "--baseline-label" :: label :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with baselineLabel := some label }
  | "--hashes" :: path :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with hashesPath := some path }
  | "--provenance" :: path :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with provenancePath := some path }
  | "--ref" :: name :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with revisionRef := some name }
  | "--per-chapter" :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with perChapter := true }
  | "--claims-only" :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with claimsOnly := true }
  | "--only" :: decl :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with onlyDecl := some decl.toName }
  | "--claim" :: name :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with claimNames := cfg.claimNames.push name.toName }
  | "--comparator" :: dir :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with comparatorDir := some dir }
  | "--no-verify" :: rest => do
      let cfg ← parseArgs rest
      pure { cfg with verifyIntegrity := false }
  | flag :: _ =>
      .error s!"Unknown or incomplete option: {flag}\n\n{usage}"

/-- Helper for slugify. -/
def slugify (s : String) : String :=
  let pushChar (acc : String) (ch : Char) : String :=
    if ch.isAlphanum then
      acc.push (if ch.isUpper then ch.toLower else ch)
    else if acc.isEmpty || acc.back == '-' then
      acc
    else
      acc.push '-'
  let slug := s.foldl pushChar ""
  -- `pushChar` already drops leading and consecutive separators, but a separator emitted for a
  -- trailing non-alphanumeric run would dangle at the end, so strip any trailing `-`.
  let slug := String.ofList (slug.toList.reverse.dropWhile (· == '-')).reverse
  if slug.isEmpty then "item" else slug

/-- Helper for humanizeWord. -/
def humanizeWord (s : String) : String :=
  if s.isEmpty then
    s
  else
    let rec go (chars : List Char) (prevLower : Bool) (acc : String) :=
      match chars with
      | [] => acc
      | ch :: rest =>
          let insertSpace := prevLower && ch.isUpper
          let acc := if insertSpace then acc.push ' ' else acc
          go rest ch.isLower (acc.push ch)
    go s.toList false ""

/-- Computes module TailComponents. -/
def moduleTailComponents (rootPrefix moduleName : Name) : List String :=
  let root := nameComponents rootPrefix
  let full := nameComponents moduleName
  full.drop root.length

/-- Computes group KeyOfModule. -/
def groupKeyOfModule (rootPrefix moduleName : Name) : String :=
  match moduleTailComponents rootPrefix moduleName with
  | first :: _ => first
  | [] => rootPrefix.toString

/-- Computes module PathOf. -/
def modulePathOf (rootPrefix moduleName : Name) : String :=
  let tail := moduleTailComponents rootPrefix moduleName
  match tail with
  | [] => moduleName.toString
  | _ => String.intercalate "." tail

/-- Maps a declaration name to a pure-ASCII identifier that is unique across declarations, for use
as an explicit Verso cross-reference tag.

`anchorIdOf` keeps non-ASCII characters, which is right for filenames and anchors but not for
Verso tags: when a declaration page does not provide its own tag, Verso derives one from the title
and non-ASCII characters do not survive that derivation. `induction_on`, `induction_on₂` and
`induction_on₃` therefore derived the *same* tag and the build failed with a duplicate-tag error.
Encoding every character outside `[A-Za-z0-9]` as `_xHEX_` keeps the mapping injective and the
result ASCII. -/
def asciiTagOf (name : Name) : String :=
  name.toString.foldl (init := "") fun acc c =>
    if c.isAlphanum then acc.push c
    else acc ++ s!"_x{String.ofList (Nat.toDigits 16 c.toNat)}_"

/-! ### Page tags

Verso keys every part by its `tag`, and two parts claiming the same one leaves one of them without
an external ID — reported at render time as `No external ID for <title>`, naming one of the two and
giving no hint that a collision is what happened.

The three kinds of page can genuinely want the same tag, because a project may name a file after the
definition it introduces. Mathlib does this everywhere: with `--root Mathlib.Logic`, the file
`Mathlib/Logic/Denumerable.lean` sits directly under the root, so it is its own chapter *and* its own
module, and it defines `Denumerable` — chapter, module and declaration all claiming `Denumerable`.
`Mathlib.Order` has 31 such cases and `Mathlib.Logic` 6, while `brownian-motion`, `alpha-rar` and
`LeanMachineLearning` have none between them: every one of their files lives in a subdirectory, so
chapter, module and declaration are always three different strings.

Prefixing by kind makes the collision impossible rather than unlikely. Within a kind the names are
already unique — chapter keys, module names and (via `asciiTagOf`) declaration names.

These are *not* the page's `file`, which is what its URL is built from and which was already distinct
in every case. Changing a tag therefore moves no page and breaks no link. -/

/-- Cross-reference tag of a chapter page. See *Page tags*. -/
def chapterTagOf (groupKey : String) : String := s!"chapter-{groupKey}"

/-- Cross-reference tag of a module page. See *Page tags*. -/
def moduleTagOf (moduleName : Name) : String := s!"module-{moduleName}"

/-- Cross-reference tag of a declaration page. See *Page tags*. -/
def declTagOf (name : Name) : String := s!"decl-{asciiTagOf name}"

/-- Cross-reference tag of a declaration's standalone-file page. See *Page tags*. -/
def minimalFileTagOf (name : Name) : String := s!"minimal-{asciiTagOf name}"

/-- Percent-encodes `s` (as UTF-8) for use in a URL path, escaping every byte outside the RFC 3986
unreserved set (`A-Za-z0-9` and `-_.~`). -/
def percentEncode (s : String) : String := Id.run do
  let hexDigit (n : Nat) : Char :=
    if n < 10 then Char.ofNat (0x30 + n) else Char.ofNat (0x41 + (n - 10))
  let unreserved (n : Nat) : Bool :=
    (n ≥ 0x41 && n ≤ 0x5A) || (n ≥ 0x61 && n ≤ 0x7A) || (n ≥ 0x30 && n ≤ 0x39)
      || n == 0x2D || n == 0x5F || n == 0x2E || n == 0x7E
  let mut out : Array Char := #[]
  for b in s.toUTF8.toList do
    let n := b.toNat
    if unreserved n then
      out := out.push (Char.ofNat n)
    else
      out := ((out.push '%').push (hexDigit (n / 16))).push (hexDigit (n % 16))
  return String.ofList out.toList

/-- A link to the live Lean web editor (live.lean-lang.org), pre-loaded (via its `#url=` parameter)
with the extracted standalone file for `name` served from the deployed site at `base`. -/
def leanEditorUrl (base : String) (name : Name) : String :=
  let sep := if base.endsWith "/" then "" else "/"
  s!"https://live.lean-lang.org/#url={base}{sep}extracted/{percentEncode (anchorIdOf name)}.lean"

/-- Helper for joinInlines. -/
def joinInlines (xs : List (Array (Inline Manual))) (sep : Array (Inline Manual)) : Array (Inline Manual) :=
  match xs with
  | [] => #[]
  | x :: rest => rest.foldl (fun acc item => acc ++ sep ++ item) x

/-- Drops lines that consist solely of a raw HTML tag (e.g. `<div align="center">` or `</div>`),
since `MD_FLAG_NOHTML` causes MD4Lean to render such lines as literal text instead of ignoring
them. -/
def stripHtmlOnlyLines (doc : String) : String :=
  let isHtmlOnlyLine (line : String) : Bool :=
    let trimmed := line.trimAscii
    trimmed.startsWith "<" && trimmed.endsWith ">" && !trimmed.startsWith "<!--"
  String.intercalate "\n" ((doc.splitOn "\n").filter (!isHtmlOnlyLine ·))

/-- Converts markdown text into `Block Manual` nodes. -/
def markdownToBlocks (doc : String) : Array (Block Manual) :=
  let doc := stripHtmlOnlyLines doc
  match MD4Lean.parse doc (MD4Lean.MD_DIALECT_GITHUB ||| MD4Lean.MD_FLAG_LATEXMATHSPANS ||| MD4Lean.MD_FLAG_NOHTML) with
  | none => #[.para #[.text doc]]
  | some parsed =>
      parsed.blocks.foldl
        (fun acc block =>
          match Verso.Genre.Manual.Markdown.blockFromMarkdown' block (handleHeaders := Verso.Genre.Manual.Markdown.strongEmphHeaders') with
          | .ok out => acc.push out
          | .error _ => acc.push (.para #[.text doc]))
        #[]

/-- Reads a file when present, returning `none` when missing. -/
def readFileIfExists (path : System.FilePath) : IO (Option String) := do
  if ← path.pathExists then
    return some (← IO.FS.readFile path)
  return none

/-- Reads the project's `formalization.yaml`, when it has one.

A parse failure is a warning and not an error. The file sits beside the library rather than inside
it, and refusing to build the site because one field of it is malformed would trade the whole report
for one page of it — so the site is built without a Claims page and the reason goes to the console,
where the author is the person who can act on it. -/
def readFormalization (projectDir : System.FilePath) : IO (Option Formalization) := do
  let some raw ← readFileIfExists (projectDir / "formalization.yaml")
    | return none
  match Formalization.parse raw with
  | .ok form => return some form
  | .error message =>
    IO.eprintln s!"warning: formalization.yaml could not be read ({message}); the site will have \
      no Claims page"
    return none

/-- Pretty-prints ExprString. -/
def ppExprString (env : Environment) (e : Expr) : IO String := do
  let ctx : PPContext := { env := env, opts := {} }
  return toString (← ctx.runMetaM (Meta.ppExpr e))

set_option compiler.checkMeta false in
/-- Builds the same `Block.docstring` value that `{docstring name}` would produce inside
a `#doc` page, by directly invoking Verso's signature/declaration-type computation. Returns
`none` if this fails for the given declaration (e.g. unsupported declaration shapes).

The pretty-printing context opens the declaration's own namespace and all of its ancestors, so
that `scoped` notation declared in those namespaces (e.g. order notation for a structure defined
there) is used instead of falling back to raw instance/projection names.

`Block.Docstring.DeclType.ofName` and `Signature.forName` are `meta` in Verso: they are meant to
run while a `#doc` page elaborates. This tool calls them from the compiled executable instead, so
the module system's phase check has to be switched off for this one definition. Both are ordinary
`LEAN_EXPORT` symbols in Verso's library, so the call links and runs normally. -/
def mkDocstringBlock? (env : Environment) (name : Name) : IO (Option (Block Manual)) := do
  let options := Options.empty.setBool `pp.fieldNotation false
  let coreCtx : Core.Context := { fileName := "<referee>", fileMap := default, options }
  let openDecls := (namespaceAncestors name.getPrefix).map (OpenDecl.simple · [])
  let act : MetaM (Block Manual) := do
    let declType ← Block.Docstring.DeclType.ofName name
    let sig ← (Signature.forName name : Elab.TermElabM Signature).run' {}
    pure <| .other (Block.docstring name declType sig none #[]) #[]
  try
    let block ← (act.run' {}).toIO'
      { coreCtx with currNamespace := name.getPrefix, openDecls } { env := env }
    pure (some block)
  catch _ =>
    pure none

/-- Extracts a declaration's source snippet from an already-loaded array of the file's lines. -/
def sliceSourceSnippet (lines : Array String) (src : SourceInfo) : String :=
  let startIdx := src.line - 1
  let endIdx := min src.endLine lines.size
  let selected := (List.range (endIdx - startIdx)).map fun i => lines[startIdx + i]!
  String.intercalate "\n" selected

/-- Computes declaration Keyword. -/
def declKeyword : DeclKind → String
  | .theorem => "theorem"
  | .definition => "def"
  | .opaque => "opaque"
  | .structure => "structure"
  | .typeclass => "class"
  | .inductive => "inductive"
  | .axiom => "axiom"
  | .instance => "instance"

/-- The signature to show when a declaration has no usable source of its own: its pretty-printed
type, introduced by the keyword it was written with.

`isLemma` matters because the fallback is exactly what an *attribute-generated* declaration gets —
`to_dual` and `to_additive` leave the generated sibling with a source range covering only the
attribute — and rendering `theorem foo : …` inside a card labelled "Lemma" contradicts the label. -/
def displaySignatureFallback (kind : DeclKind) (name : Name) (expandedSignature : String)
    (isLemma : Bool := false) : String :=
  let keyword := if isLemma && kind == .theorem then "lemma" else declKeyword kind
  s!"{keyword} {name.getString!} : {expandedSignature}"

/-- Helper for stringContains. -/
def stringContains (haystack needle : String) : Bool :=
  (haystack.splitOn needle).length > 1

/-- Scans one line of an `@[…]` attribute that is still open, given the bracket `depth` reached so
far and whether the scan is inside a string literal.

Returns `.inl (depth, inString)` if the attribute is still unclosed at the end of the line, or
`.inr remainder` with what follows the `]` that closed it.

Counting depth, and tracking string literals, is what makes this correct rather than a search for
the first `]`: an attribute argument can contain a bracket (`@[specifies f "the a[i] case"]`), and
one that closes early would leave the tail of the attribute glued to the front of the statement. -/
def scanAttributeLine (chars : List Char) (depth : Nat) (inString : Bool) :
    (Nat × Bool) ⊕ String :=
  match chars with
  | [] => .inl (depth, inString)
  | c :: rest =>
    if inString then
      -- An escape consumes the next character, so `"\""` does not end the literal. At end of line
      -- this leaves the scan inside the string, which is also what Lean's string gap (`\` then a
      -- newline) needs.
      if c == '\\' then
        match rest with
        | [] => .inl (depth, true)
        | _ :: rest => scanAttributeLine rest depth true
      else scanAttributeLine rest depth (c != '"')
    else if c == '"' then scanAttributeLine rest depth true
    else if c == '[' then scanAttributeLine rest (depth + 1) false
    else if c == ']' then
      if depth ≤ 1 then .inr (String.ofList rest) else scanAttributeLine rest (depth - 1) false
    else scanAttributeLine rest depth false

/-- Drops a leading `@[…]` attribute from `lines`, which may span several of them, and returns what
follows it. -/
partial def dropAttributeBlock (lines : List String) : List String :=
  go lines 0 false
where
  go (lines : List String) (depth : Nat) (inString : Bool) : List String :=
    match lines with
    | [] => []
    | line :: rest =>
      match scanAttributeLine line.toList depth inString with
      | .inl (depth, inString) => go rest depth inString
      | .inr remainder => if remainder.trimAscii.isEmpty then rest else remainder :: rest

/-- Drops the docstrings and attributes preceding a declaration, so that what is left starts at the
declaration keyword. Everything downstream reads that first word: the displayed signature, and the
`lemma`/`instance`/`alias` detection that decides how a declaration is labelled and whether it
counts as a claim. -/
partial def dropLeadingDecorations (lines : List String) : List String :=
  let lines := lines.dropWhile (fun line => line.trimAscii.isEmpty)
  match lines with
  | [] => []
  | line :: rest =>
      let trimmed := (String.trimAscii line).toString
      if trimmed.startsWith "/-" then
        let rec dropCommentBlock : List String → List String
          | [] => []
          | commentLine :: remaining =>
              if stringContains commentLine "-/" then
                remaining
              else
                dropCommentBlock remaining
        dropLeadingDecorations (dropCommentBlock (line :: rest))
      else if trimmed.startsWith "@[" then
        dropLeadingDecorations (dropAttributeBlock (line :: rest))
      else
        line :: rest

/-- Helper for cleanDeclSnippet. -/
def cleanDeclSnippet (snippet : String) : String :=
  (String.trimAscii (String.intercalate "\n" (dropLeadingDecorations (snippet.splitOn "\n")))).toString

/-- How far past a declaration's recorded range to look for its keyword. Bounded so that a range
which cleans to nothing and is followed by no declaration cannot scan to the end of the file. -/
def declKeywordLookahead : Nat := 40

/-- The cleaned snippet to read a declaration's *keyword* from — the word that decides whether the
site labels it `lemma`, `theorem` or `instance`.

Usually this is just the cleaned source range. The exception, and the only reason this function
looks past that range, is an **attribute-generated declaration**. Given

```lean
@[to_dual min_le]
lemma le_max (x : ι) : f x ≤ max f := …
```

Lean records, for the generated `min_le`, a declaration range covering *only the attribute line*.
Cleaning it strips the attribute and leaves nothing, so the `lemma` the author wrote is never seen
and the declaration is labelled a theorem — which puts it on the Claims page, among the results the
library is asserting for its own sake. `to_additive` produces exactly the same shape, as does any
other attribute that generates a sibling declaration.

Only the keyword is taken from the following lines, never the statement. A generated declaration
says something *different* from the one it was generated from — `min_le` is not `le_max` — so its
displayed signature must keep coming from its own pretty-printed type. That is why this is separate
from `displaySignatureFromSource` rather than a fix inside it. -/
def keywordSnippet (src : SourceInfo) (lines : Array String) : String :=
  let cleaned := cleanDeclSnippet (sliceSourceSnippet lines src)
  if !cleaned.isEmpty then
    cleaned
  else
    let startIdx := src.line - 1
    let endIdx := min (startIdx + declKeywordLookahead) lines.size
    if endIdx ≤ startIdx then ""
    else
      let window := (List.range (endIdx - startIdx)).map fun i => lines[startIdx + i]!
      (String.trimAscii (String.intercalate "\n" (dropLeadingDecorations window))).toString

/-- Splits a declaration's source snippet at the `:=` separating its signature from its value, into
the part before and the part after.

The separator is the first `:=` **at bracket depth zero**, not simply the first one, and the
distinction is not academic. A statement may contain any number of `:=` tokens inside brackets — a
named argument (`Tendsto (β := ProbabilityMeasure …)`), a structure instance (`{ x := 1 }`), a
binder default (`(n : ℕ := 0)`) — and splitting on the first of them truncates the statement
mid-expression while handing its tail to the proof section. Depth counting is enough to tell them
apart, since the proof separator is the only one a declaration can have outside every bracket.

Returns `none` when there is no top-level `:=` at all, which is the ordinary case for an `axiom` or
a declaration whose value is given by `where` clauses. -/
def splitAtAssignment (snippet : String) : Option (String × String) := Id.run do
  let chars := snippet.toList
  let arr := chars.toArray
  let mut depth : Int := 0
  let mut cut : Option Nat := none
  for i in [0:arr.size] do
    if cut.isNone then
      let c := arr[i]!
      if c == '(' || c == '[' || c == '{' || c == '⟨' then
        depth := depth + 1
      else if c == ')' || c == ']' || c == '}' || c == '⟩' then
        depth := depth - 1
      else if c == ':' && depth == 0 && i + 1 < arr.size && arr[i + 1]! == '=' then
        cut := some i
  match cut with
  | none => return none
  | some k => return some (String.ofList (chars.take k), String.ofList (chars.drop (k + 2)))

/-- The signature part of a snippet: everything before the top-level `:=`, or the whole snippet
when it has none. -/
def headBeforeAssignment (snippet : String) : String :=
  match splitAtAssignment snippet with
  | some (head, _) => (String.trimAscii head).toString
  | none => (String.trimAscii snippet).toString

/-- Helper for displaySignatureFromSource. -/
def displaySignatureFromSource (kind : DeclKind) (src? : Option SourceInfo) (lines : Array String) : Option String :=
  match src? with
  | none => none
  | some src =>
    let snippet := cleanDeclSnippet (sliceSourceSnippet lines src)
    if snippet.isEmpty then
      none
    else
      let rendered :=
        match kind with
        | .definition | .structure | .typeclass | .inductive => snippet
        | _ => headBeforeAssignment snippet
      if rendered.isEmpty then none else some rendered

/-! ## Reading a declaration's keyword from parsed syntax

Which keyword a declaration was written with is not recoverable from the compiled environment.
Mathlib's `lemma` is a macro that erases itself before elaboration —

```lean
@[macro «lemma»] def expandLemma : Macro := fun stx =>
  let stx := stx.modifyArg 1 fun stx =>
    let stx := stx.modifyArg 0 (mkAtomFrom · "theorem" (canonical := true))
    stx.setKind ``Parser.Command.theorem
  pure <| stx.setKind ``Parser.Command.declaration
```

— so the elaborator only ever sees a theorem, `ConstantInfo` has nowhere to record the word, and no
environment extension carries it. The source text is the only witness, which is why this is read
back rather than looked up.

Reading it by parsing rather than by matching the text is what makes it robust. `IO.processCommands`
re-elaborates the file against the already-loaded environment and hands back each command's `Syntax`,
so the answer comes from the same parser that accepted the file: modifiers on their own line, doc
comments, multi-line attribute blocks and `set_option … in` wrappers are all just structure. It also
settles the case the text can never settle — an *attribute-generated* declaration (`to_dual`,
`to_additive`) whose recorded range covers only the attribute line falls inside the generating
command, and so inherits its keyword by construction rather than by a lookahead heuristic.

The string-based readers below remain as the fallback for a declaration whose range no parsed
command covers.
-/

/-- What one parsed command says about the keyword its declarations were written with, and the line
range it covers.

Reduced to these flags at parse time rather than kept as `Syntax`: the whole point is one pass per
file, and holding every command's tree for every project module at once is a great deal of memory
for three bits. -/
structure CommandKeyword where
  startLine : Nat
  endLine : Nat
  isLemma : Bool
  isInstance : Bool
  isAlias : Bool
deriving Repr, Inhabited

/-- Parses `source` against `env` (`parseCommands`) and reports, per command, its line range and the
keyword its declarations were written with. -/
def commandKeywordsOf (env : Environment) (source : String) (filePath : String) :
    IO (Array CommandKeyword) := do
  let fileMap := source.toFileMap
  let commands ← parseCommands env source filePath
  return commands.filterMap fun stx =>
    match stx.getPos?, stx.getTailPos? with
    | some p, some e =>
      some {
        startLine := (fileMap.toPosition p).line
        endLine := (fileMap.toPosition e).line
        isLemma := containsSyntaxKind stx lemmaSyntaxKinds
        isInstance := containsSyntaxKind stx instanceSyntaxKinds
        isAlias := containsSyntaxKind stx aliasSyntaxKinds
      }
    | _, _ => none

/-- The command covering `line`, or `none` if no parsed command does.

Takes the last such command, so that a declaration inside a wrapper is attributed to the innermost
enclosing one when ranges overlap. -/
def commandKeywordAt? (cmds : Array CommandKeyword) (line : Nat) : Option CommandKeyword :=
  cmds.foldl (init := none) fun best c =>
    if c.startLine ≤ line && line ≤ c.endLine then
      match best with
      | some b => if c.startLine ≥ b.startLine then some c else best
      | none => some c
    else best

/-- The modifiers Lean allows between a declaration's attributes and its keyword.

Stripped only when reading the *keyword*, never from the displayed signature: `protected lemma foo`
is what the author wrote and is what the page should show. It is the classification that must look
past them, because `protected lemma` is still a lemma. -/
def declModifiers : Array String :=
  #["private", "protected", "public", "noncomputable", "unsafe", "partial", "nonrec", "scoped",
    "local", "meta"]

/-- Drops any leading `declModifiers` from a cleaned snippet, so the next word is the keyword.

Repeated because they combine: `protected noncomputable def`, `public meta def`.

Splits on *any* whitespace rather than on a space, because a modifier is routinely left on a line of
its own — `brownian-motion` writes

```lean
protected
lemma _root_.SupClosed.mem_countableSupClosure_iff …
```

and matching `"protected "` reads straight past that. -/
partial def dropDeclModifiers (s : String) : String :=
  let s := (String.trimAscii s).toString
  let word := (s.takeWhile (!·.isWhitespace)).toString
  if declModifiers.contains word then
    dropDeclModifiers (s.drop word.length).toString
  else
    s

/-- True if the cleaned source snippet for a `theorem`-kind declaration starts with the `lemma`
keyword rather than `theorem`.

The **fallback** for `commandKeywordsOf`, used only where no parsed command covers a declaration's
range. Reads past any visibility or binder modifier. Getting this wrong is not cosmetic: `isLemma`
feeds `DeclInfo.isClaim`, so a `protected lemma` read as a theorem is promoted onto the Claims page,
among the results the library asserts for their own sake. -/
def isLemmaFromSource (kind : DeclKind) (src? : Option SourceInfo) (lines : Array String) : Bool :=
  if kind != .theorem then
    false
  else match src? with
    | none => false
    | some src => (dropDeclModifiers (keywordSnippet src lines)).startsWith "lemma "

/-- True if the cleaned source snippet for a `theorem`-kind declaration starts with the
`instance` keyword (e.g. a `Prop`-valued instance whose `@[instance]` attribute was not picked
up by `declKindOf`). -/
def isInstanceFromSource (kind : DeclKind) (src? : Option SourceInfo) (lines : Array String) : Bool :=
  if kind != .theorem then
    false
  else match src? with
    | none => false
    | some src => (dropDeclModifiers (keywordSnippet src lines)).startsWith "instance "

/-- True if the declaration's source snippet starts with the `alias` keyword. Such declarations are
emitted verbatim (`alias … := target`), so their dependency closure must follow value dependencies. -/
def isAliasFromSource (src? : Option SourceInfo) (lines : Array String) : Bool :=
  match src? with
  | none => false
  | some src =>
    (dropDeclModifiers (cleanDeclSnippet (sliceSourceSnippet lines src))).startsWith "alias "

/-- True if `name`'s last component follows the standard naming convention for
compiler-generated instances (e.g. `instDecidableEqFoo` from a `deriving` clause), namely
`inst` followed by an uppercase letter. Such declarations are not written with the `instance`
keyword in the source (there is no source line to inspect), so `isInstanceFromSource` cannot
catch them. -/
def isInstanceName (name : Name) : Bool :=
  let s := name.getString!
  s.startsWith "inst" && s.length > 4 && (s.drop 4).front.isUpper

/-- All ways to split `s` at an internal underscore into a non-empty `(prefix, suffix)` pair. -/
def underscoreSplits (s : String) : List (String × String) :=
  let chars := s.toList
  (List.range chars.length).filterMap fun i =>
    if i > 0 && i < chars.length - 1 && chars[i]! == '_' then
      some (String.ofList (chars.take i), String.ofList (chars.drop (i + 1)))
    else
      none

/-- True if `name` looks like a `@[simps]`-generated projection lemma: a `@[simp]`-tagged
theorem whose short name has the form `<sibling>_<field>`, where `<sibling>` is itself a
declaration in the same namespace (the definition/instance the `@[simps]` attribute was applied
to). -/
def isSimpsGeneratedLemma (env : Environment) (simpLemmaNames : Std.HashSet Name) (name : Name)
    (info : ConstantInfo) : Bool :=
  match info with
  | .thmInfo _ =>
    simpLemmaNames.contains name &&
      match name with
      | .str pfx s =>
          (underscoreSplits s).any fun (sibling, _) => (env.find? (.str pfx sibling)).isSome
      | _ => false
  | _ => false

/-- Infers the display kind for a declaration from environment metadata. -/
def declKindOf (env : Environment) (info : ConstantInfo) (name : Name) : DeclKind :=
  if Lean.Meta.isInstanceCore env name then
    .instance
  else if isClass env name then
    .typeclass
  else match info with
    | .thmInfo _ => .theorem
    | .opaqueInfo _ => .opaque
    | .axiomInfo _ => .axiom
    | .inductInfo _ =>
        if (getStructureInfo? env name).isSome then
          .structure
        else
          .inductive
    | .defnInfo _ => .definition
    | _ => .definition

/-- Computes source PathForModule. -/
def sourcePathForModule (pkg : Lake.Package) (moduleName : Name) : Option System.FilePath :=
  (pkg.findModule? moduleName).map (·.leanFile)

/-- Parses ImportedModule?. -/
def parseImportedModule? (line : String) : Option Name :=
  let trimmed := (String.trimAscii line).toString
  let prefixes := ["public import ", "import "]
  prefixes.findSome? fun pfx =>
    if trimmed.startsWith pfx then
      let rest := (String.trimAscii (trimmed.drop pfx.length |>.toString)).toString
      if rest.isEmpty then none else some rest.toName
    else
      none

/-- Visits ModuleImports. -/
partial def visitModuleImports (projectDir : System.FilePath) (rootPrefix : Name)
    (moduleName : Name) (visited : Std.HashSet Name) (order : Std.HashMap Name Nat)
    (nextRank : Nat) : IO (Std.HashSet Name × Std.HashMap Name Nat × Nat) := do
  if visited.contains moduleName then
    return (visited, order, nextRank)
  let visited := visited.insert moduleName
  let text? ← readFileIfExists (moduleSourcePath projectDir moduleName)
  match text? with
  | none => return (visited, order, nextRank)
  | some contents =>
      let imports : List Name := (contents.splitOn "\n").filterMap parseImportedModule?
      let imports := imports.filter fun imported => imported != moduleName && hasPrefixName imported rootPrefix
      let mut visited := visited
      let mut order := order
      let mut nextRank := nextRank
      for imported in imports do
        if !order.contains imported then
          order := order.insert imported nextRank
          nextRank := nextRank + 1
        let (visited', order', nextRank') ← visitModuleImports projectDir rootPrefix imported visited order nextRank
        visited := visited'
        order := order'
        nextRank := nextRank'
      return (visited, order, nextRank)

/-- Computes import-traversal order used to rank modules and groups. -/
def moduleOrderMap (projectDir : System.FilePath) (rootPrefix : Name) : IO (Std.HashMap Name Nat) := do
  let rootFile := moduleSourcePath projectDir rootPrefix
  if !(← rootFile.pathExists) then
    return {}
  let initial : Std.HashMap Name Nat := {}
  let (_, order, _) ← visitModuleImports projectDir rootPrefix rootPrefix {} (initial.insert rootPrefix 0) 1
  return order

/-- Helper for proofTextFromSource. -/
def proofTextFromSource (kind : DeclKind) (src? : Option SourceInfo) (lines : Array String) : Option String :=
  match kind, src? with
  | .theorem, some src
  | .opaque, some src
  | .instance, some src =>
      -- Clean first, exactly as `displaySignatureFromSource` does. Without it the split below
      -- lands on a `:=` *inside an attribute* — `@[to_additive (attr := simp)]` made the "Proof"
      -- section start with `simp)]` followed by the entire declaration.
      let snippet := cleanDeclSnippet (sliceSourceSnippet lines src)
      match splitAtAssignment snippet with
      | some (_, proof) => some (String.trimAscii proof).toString
      | none => some snippet
  | _, _ => none

/-- Computes module IndexMap. -/
def moduleIndexMap (decls : Array DeclInfo) : Std.HashMap Name (Array DeclInfo) :=
  decls.foldl
    (fun acc decl => acc.insert decl.moduleName ((acc.getD decl.moduleName #[]).push decl))
    {}

/-- Computes group IndexMap. -/
def groupIndexMap (mods : Array ModuleInfo) : Std.HashMap String (Array ModuleInfo) :=
  mods.foldl
    (fun acc modInfo => acc.insert modInfo.groupKey ((acc.getD modInfo.groupKey #[]).push modInfo))
    {}

/-- Builds a prefilled GitHub issue URL for declaration review: the declaration's full name in the
title, and its name and source location in the body. The module is not repeated — the source path
is the module — and whether the declaration is proved is left to the author's tracker, since it
changes and the issue does not. -/
def issueUrlOf (repoUrl? : Option String) (decl : Name) (source? : Option SourceInfo) :
    Option String :=
  repoUrl?.map fun repoUrl =>
    let title := s!"Referee review: {decl}"
    let sourceLine :=
      match source? with
      | some src => s!"**Source:** {src.relPath}:{src.line}"
      | none => "**Source:** unavailable"
    let body := String.intercalate "%0A" [
      s!"**Declaration:** `{decl}`",
      sourceLine,
      "",
      "---",
      "",
      "**Describe the issue:**",
      ""
    ]
    s!"{repoUrl}/issues/new?title={title}&body={body}&labels=referee-review"

/-- Builds a repository source link for a declaration location.

`ref` is the branch or commit to link into. It defaults to `main`, which is what every link here
used to be pinned to — and which quietly rots: a published site keeps pointing at line 88 of a file
that has moved on, so the link lands on whatever now happens to be there. Given a provenance
ledger, `build-site` passes the commit the ledger was folded at instead, and the links keep showing
the code the site was actually built from. -/
def sourceUrlOf (repoUrl? : Option String) (source? : Option SourceInfo) (ref : String := "main")
    : Option String :=
  match repoUrl?, source? with
  | some repoUrl, some src => some s!"{repoUrl}/blob/{ref}/{src.relPath}#L{src.line}"
  | _, _ => none

/-- Computes repository FileUrlOf. -/
def repoFileUrlOf (repoUrl? : Option String) (relPath : String) (ref : String := "main")
    : Option String :=
  repoUrl?.map fun repoUrl => s!"{repoUrl}/blob/{ref}/{relPath}"

/-- Computes group HrefOf. -/
def groupHrefOf (groupKey : String) : String :=
  s!"chapter-{slugify groupKey}/"

/-- Where a chapter's declaration table is written, site-root-relative.

Named here, beside the other path rules, because three places have to agree on it and none of them
can see the others: the pages reference it (`Block.graph`), the build writes it (`writeDeclTables`),
and neither is in a position to notice if the other changes. Under `-verso-data/` with the hoisted
assets, since it is the same kind of thing — one file the whole site shares rather than bytes
repeated per page — and not content-addressed, because the page has to name it before it is
written. -/
def declTablePath (groupKey : String) : String :=
  s!"-verso-data/referee-decls-{slugify groupKey}.js"

/-- Where a chapter's *signature and docstring* table is written, site-root-relative.

Split from `declTablePath` because the two are needed at different moments and only one of them is
needed to draw. A graph needs every node's label, kind, module and href before it can put a box on
the screen; it needs a signature only for the one node a reader clicks, and often for none. Measured
on `Mathlib.Analysis`, signature and docstring were **68%** of the chapter tables, and a page loads
7.25 of them on average — so keeping them in the eagerly-loaded file cost a first-time reader ~8.7 MB
to draw a picture that needed ~2.9 MB of it.

Fetched by injecting a `<script>` on the first click that needs one, not by `fetch`, for the reason
`upstreamJsFile` gives: a site opened over `file://` cannot fetch its siblings, and the summary
under a clicked node is precisely what that reader is left with. -/
def upstreamTextPath : String := "-verso-data/upstream-text.js"

/-- Where the upstream constants' signatures, values and docstrings are written.

Split from `upstream.js` for the reason `declTextPath` gives, and with more force: `upstream.js` is
a `RenderConfig` asset, so *every* page of the site loads it whether or not it draws a graph, and
the text was 90% of it. What stays behind is what the band needs to be drawn — the label, module and
package of each constant, and its `nodeIndex` number. -/
def declTextPath (groupKey : String) : String :=
  s!"-verso-data/referee-text-{slugify groupKey}.js"

/-- Computes module HrefOf. -/
def moduleHrefOf (modulePath : String) : String :=
  s!"module-{slugify modulePath}/"

/-- Computes path ForPart. -/
def pathForPart (groupKey modulePath : String) (declName : Name) : String :=
  s!"{groupHrefOf groupKey}{moduleHrefOf modulePath}#{anchorIdOf declName}"

/-- Maps each declaration name to its generated page anchor path. -/
def declHrefMap (decls : Array DeclInfo) : Std.HashMap Name String :=
  decls.foldl
    (fun acc decl => acc.insert decl.name (pathForPart decl.groupKey decl.modulePath decl.name))
    {}

/-- Computes path ForDeclPage. -/
def pathForDeclPage (groupKey modulePath : String) (declName : Name) : String :=
  s!"{groupHrefOf groupKey}{moduleHrefOf modulePath}decl-{anchorIdOf declName}/"

/-- Maps each declaration name to its dedicated detail page. -/
def declPageHrefMap (decls : Array DeclInfo) : Std.HashMap Name String :=
  decls.foldl
    (fun acc decl => acc.insert decl.name (pathForDeclPage decl.groupKey decl.modulePath decl.name))
    {}

/-- Maps each declaration name to its `DeclInfo`. -/
def declByNameMap (decls : Array DeclInfo) : Std.HashMap Name DeclInfo :=
  decls.foldl (fun acc decl => acc.insert decl.name decl) {}

/-- True if `n` survives a round trip through `Name`'s JSON codec (`toString` then `toName`).
This is lossy for names containing characters outside a normal identifier — notably auto-generated
helper names from *external* libraries, which can embed hygiene markers like `_@.Mathlib.Foo.123`
that aren't valid surface syntax and so don't parse back to the original name. -/
def isJsonSafeName (n : Name) : Bool :=
  n.toString.toName == n

/-- Replaces every constant in a statement's anatomy that would not survive the JSON round trip
with `.anonymous`, which is already the anatomy's word for "no constant here".

The anatomy carries `Name`s in five places, and unlike `deps` they are not a set to filter: each one
sits beside the text it annotates, so dropping the entry would lose the text with it. Blanking the
name keeps the row and loses only its hover, which is what the reader would have got anyway — the
names this catches are hygienic internals like
`Asymptotics.wrapped._@.Mathlib.Analysis.Asymptotics.Defs.126441222._hygCtx._hyg.2`, which name no
page and no docstring, and which `anatomyTipOf` already declines to say anything about.

Without this, `collect` writes a `data.json` that `build-site` cannot read back: `Name`'s JSON codec
is `toString` then `toName`, and a hygiene marker is not valid surface syntax, so the parse fails
and takes the whole file with it — the whole run, for one name. Found by running against
`Mathlib.Analysis`, whose 28,381 declarations yielded 29 occurrences of 28 distinct such names, all
of them a `wrapped` helper from an `Asymptotics`-style definition. Rare enough that no project small
enough to be a test fixture produces one, which is why `dropUnsafeDeps` was never extended here when
the anatomy was added, and fatal enough that one is sufficient. -/
def anatomySafeNames (a : StatementAnatomy) : StatementAnatomy :=
  let safe (n : Name) : Name := if isJsonSafeName n then n else .anonymous
  let piece (p : TypePiece) : TypePiece := { p with const := safe p.const }
  let binder (b : StatementBinder) : StatementBinder :=
    { b with head := safe b.head, pieces := b.pieces.map piece }
  { a with
    binders := a.binders.map binder
    conclusionHead := safe a.conclusionHead
    conclusionPieces := a.conclusionPieces.map piece
    bodyPieces := a.bodyPieces.map piece
    fields := a.fields.map fun f =>
      { f with head := safe f.head, pieces := f.pieces.map piece } }

/-- Drops names that don't round-trip through JSON (see `isJsonSafeName`) from `deps`/`typeDeps`,
so that serializing `decls` for the `collect` subcommand can't fail. Safe to do unconditionally:
every consumer of `deps`/`typeDeps` (graph edges, the closure listings, the extraction closure)
already discards anything that isn't itself an exposed project declaration, and a name needing
this escape hatch is never one (`shouldExpose` already excludes internal/auto-generated names from
being exposed), so this can only drop names that were already inert. -/
def dropUnsafeDeps (decls : Array DeclInfo) : Array DeclInfo :=
  decls.map fun d => { d with
    deps := d.deps.filter isJsonSafeName
    typeDeps := d.typeDeps.filter isJsonSafeName
    dataDeps := d.dataDeps.filter isJsonSafeName
    anatomy? := d.anatomy?.map anatomySafeNames
  }

/-- Helper for relativeSourcePath. -/
def relativeSourcePath (projectDir absPath : System.FilePath) : IO String := do
  let projectDir ← IO.FS.realPath projectDir
  let absPath ← IO.FS.realPath absPath
  let project := projectDir.normalize.toString
  let path := absPath.normalize.toString
  match path.dropPrefix? (project ++ "/") with
  | some rel => pure rel.toString
  | none =>
      match path.dropPrefix? project with
      | some rel => pure <| (rel.toString.dropWhile (· == '/')).toString
      | none => pure path

/-- Converts declaration ranges into serializable source metadata. -/
def toSourceInfo? (projectDir : System.FilePath) (pkg : Lake.Package) (moduleName : Name) (ranges? : Option DeclarationRanges) : IO (Option SourceInfo) := do
  let some ranges := ranges? | return none
  let some absPath := sourcePathForModule pkg moduleName | return none
  let absPath ← IO.FS.realPath absPath
  let relPath ← relativeSourcePath projectDir absPath
  return some {
    relPath := relPath
    absPath := absPath
    line := ranges.range.pos.line
    endLine := ranges.range.endPos.line
  }

/-- Every exposed declaration's axiom set, via `Lean.collectAxioms`.

Lean precomputes each declaration's axiom set when the `.olean` is written and looks it up by
binary search for imported declarations, so this is a table lookup per declaration rather than a
walk of the closure. It also means the answer is the honest one: a `sorry` lifted into a
compiler-generated `_proof_N` helper counts, and so does one inherited from an upstream library.

This is the same answer `#print axioms` gives. Keeping the whole set rather than collapsing it to
"does this rest on `sorry`" is what lets the site report *what* a result assumes, not just whether
it is suspicious: `Classical.choice`/`propext`/`Quot.sound` are the ordinary three, while anything
else is a claim the reader has to accept on faith. -/
def axiomsOfDecls (env : Environment) (names : Array Name) : IO (Std.HashMap Name (Array Name)) :=
  runCoreIO env do
    let mut acc : Std.HashMap Name (Array Name) := {}
    for name in names do
      let axs ← Lean.collectAxioms name
      acc := acc.insert name (axs.qsort Name.lt)
    return acc

/-- Each package's depth in the workspace dependency graph: one more than the deepest package it
depends on, and `0` for one that depends on nothing.

This is the order the graph's upstream band stacks in. Mathlib depends on nothing else the reader
sees, so it goes on top; a package built on Mathlib goes below it; the project's own declarations go
below that, in the dependency rows. The band then reads the way the rest of the picture does —
everything sits below what it depends on — instead of being ordered by a property of the *reader*
(which packages they happened to audit), which says nothing about where a constant comes from.

Relaxed to a fixpoint rather than walked, bounded by the number of packages: a longest path in a DAG
cannot exceed that, and the bound is also what makes a dependency cycle terminate rather than
recurse forever. Workspaces have tens of packages, so the cost is irrelevant. -/
def packageRanks (packages : Array PackageInfo) : Std.HashMap Name Nat := Id.run do
  let mut rank : Std.HashMap Name Nat := packages.foldl (fun acc p => acc.insert p.name 0) {}
  for _ in [0:packages.size] do
    let mut changed := false
    for p in packages do
      let d := p.deps.foldl (fun m dep => max m (rank.getD dep 0 + 1)) 0
      if d > rank.getD p.name 0 then
        rank := rank.insert p.name d
        changed := true
    if !changed then break
  return rank

/-- The packages a reader is being told to trust, given the ones named with `--trust`: those, plus
everything they depend on, plus the toolchain.

Closing downwards is the whole semantics of the flag. Trusting Mathlib while treating `batteries` as
unaudited would be incoherent — Mathlib's own theorems rest on it — so naming a package necessarily
vouches for what it is built from. The toolchain is trusted unconditionally: it is the compiler and
kernel that checked every other package, so a site cannot coherently offer it as a choice.

Unknown names are *not* silently ignored; `unknownTrustedPackages` reports them, because a typo in
`--trust mathlbi` would otherwise read as a clean audit of nothing. -/
partial def trustClosure (packages : Array PackageInfo) (trusted : Array Name) : Std.HashSet Name :=
  let byName : Std.HashMap Name PackageInfo :=
    packages.foldl (fun acc pkg => acc.insert pkg.name pkg) {}
  go byName (trusted.toList ++
    (packages.filterMap fun pkg => if pkg.isToolchain then some pkg.name else none).toList) {}
where
  go (byName : Std.HashMap Name PackageInfo) (todo : List Name) (seen : Std.HashSet Name) :
      Std.HashSet Name :=
    match todo with
    | [] => seen
    | name :: rest =>
      if seen.contains name then go byName rest seen
      else
        let seen := seen.insert name
        match byName.get? name with
        | some pkg => go byName (pkg.deps.toList ++ rest) seen
        | none => go byName rest seen

/-- The `--trust` names that match no package in the workspace. See `trustClosure`. -/
def unknownTrustedPackages (packages : Array PackageInfo) (trusted : Array Name) : Array Name :=
  trusted.filter fun name => !packages.any (·.name == name)

/-- The `Lean` pseudo-package: the toolchain, which owns `Init`/`Std`/`Lean`/`Lake` and belongs to
no Lake package. -/
def toolchainPackage : PackageInfo where
  name := `Lean
  roots := #[`Init, `Std, `Lean, `Lake]
  isToolchain := true

/-- The workspace's packages, plus the `Lean` pseudo-package, with their declared dependencies and
library roots.

Roots come from the Lake configuration rather than from the modules actually present, because they
are what attributes a module to a package, and a package contributes roots whether or not this
particular project imports anything under them. -/
def packageInfosOf (ws : Lake.Workspace) (rootPrefix : Name) : Array PackageInfo :=
  -- `baseName`, not `keyName`: the latter carries Lake's workspace index (`mathlib.4`), which
  -- would be what `--trust` had to be spelled with and what the graph displayed.
  let named := ws.packages.map fun pkg =>
    let deps := pkg.depIdxs.filterMap fun i => ws.packages[i]?.map (·.baseName)
    let roots := pkg.leanLibs.flatMap (·.config.roots)
    { name := pkg.baseName
      deps := deps
      roots := roots
      -- By root prefix rather than by workspace position: `--root` may name a library of the root
      -- package, and it is the exposed library that "the project" means here.
      isProject := roots.any (hasPrefixName rootPrefix ·)
      : PackageInfo }
  named.push toolchainPackage

/-- Attributes each module of the environment to a package, by longest matching library root.

Longest wins so that a package whose root is nested under another's (`Foo.Bar` under `Foo`) claims
its own modules. A module matching no root at all is left unattributed and reported by `collect`
rather than silently folded into some package: it means the workspace's roots do not cover what the
project actually imports, and a trust claim over an incomplete attribution would be worthless. -/
def modulePackageOf (packages : Array PackageInfo) (moduleName : Name) : Option Name :=
  let candidates := packages.flatMap fun pkg =>
    pkg.roots.filterMap fun root =>
      if hasPrefixName moduleName root then some (root.getNumParts, pkg.name) else none
  let best : Option (Nat × Name) :=
    candidates.foldl (init := none) fun best (depth, name) =>
      match best with
      | some (bestDepth, _) => if depth > bestDepth then some (depth, name) else best
      | none => some (depth, name)
  best.map Prod.snd

/-- The packages with at least one module in the imported environment.

An exact bound on what any closure can possibly reach, and the thing that keeps the Lake-graph
closure from being useless. `LeanMachineLearning` *declares* a dependency on `verso` — it builds its
own site with it — so closing the Lake graph downwards reports every declaration that uses LML as
resting on Verso, SubVerso, MD4Lean and Illuminate too. None of that code is loaded here: no module
the project imports belongs to those packages, so no constant in any closure can live in one.
Intersecting with this set removes them without weakening the guarantee. -/
def loadedPackagesOf (env : Environment) (packages : Array PackageInfo) : Array Name :=
  let acc := env.header.moduleNames.foldl (init := ({} : Std.HashSet Name)) fun acc moduleName =>
    match modulePackageOf packages moduleName with
    | some pkg => acc.insert pkg
    | none => acc
  acc.toArray.qsort Name.lt

/-- The edges the project-local *closure* follows: type-only for theorems, type and body for
everything else. Computed from the raw `MeaningGraph` result, before a `DeclInfo` exists to ask.

This is the wider of the two edge choices and exists for one consumer: `transDeps`, which
`ChallengeGen` seeds each standalone file from. A file whose kept tactic bodies lost the lemmas
they call would not compile, so this must stay closed over proofs. Everything that asks what a
declaration *means* or what a reader must *trust* uses `meaningDepsOf` instead. -/
def closureDepsOf (kind : DeclKind) (isAlias : Bool) (deps typeDeps : Array Name) : Array Name :=
  if kind == .theorem && !isAlias then typeDeps else deps

/-- `closureDepsOf` for a thin record: the edges extraction inlines along. Defined here rather than
beside `ThinDecl` so that the rule has exactly one statement. -/
def ThinDecl.closureDeps (decl : ThinDecl) : Array Name :=
  closureDepsOf decl.kind decl.isAlias decl.deps decl.typeDeps

/-- The edges *meaning and trust* follow: nothing a proof merely calls.

Three cases, one principle. A theorem contributes its statement, not its proof — the kernel already
checked the proof, and anything left unproved in it arrives as a `sorry` or an extra axiom, both
reported transitively elsewhere. A definition contributes its type and the *data* in its value, but
not the proofs embedded in it: the obligations of a bundled structure (`left_inv`, `map_add'`, …)
are kernel-checked in exactly the same way and say nothing about what the definition means. An
`alias` contributes its value regardless, because it is emitted verbatim and its target is a genuine
dependency of the text.

An empty `dataDeps` beside a non-empty `deps` means the analysis was not run — `DeclInfo.dataDeps`
defaults to `#[]`, and a genuinely computed one is empty only when `deps` is, since it always
contains the type's constants. That case falls back to `deps`, so a `DeclInfo` built by hand (or
decoded from data an older `collect` wrote) reports too much rather than too little. Which way it
errs matters here and nowhere else: under-reporting would tell a reader they do not rest on code
they do. -/
def meaningDepsOf (kind : DeclKind) (isAlias : Bool) (deps typeDeps dataDeps : Array Name) :
    Array Name :=
  if isAlias then deps
  else if kind == .theorem then typeDeps
  else if dataDeps.isEmpty then deps
  else dataDeps

/-- Truncates `s` to `n` characters, marking that it was truncated. A preview-sized cut: the
declaration's own page carries the whole thing. -/
def clipTo (n : Nat) (s : String) : String :=
  let s := (String.trimAscii s).toString
  if s.length ≤ n then s else (s.take n).trimAscii.toString ++ "…"

/-- The first sentence of a docstring, for a one-line gloss: its first paragraph that is not a
heading, whitespace collapsed, cut after the first sentence and clipped to `limit`. A period inside
an abbreviation — `e.g.`, `a.k.a.` — does not end a sentence, which is what the last word before a
candidate cut is checked for. -/
def docGloss (doc : String) (limit : Nat := 200) : String :=
  let para := (doc.splitOn "\n\n").find? fun p =>
    let t := (String.trimAscii p).toString
    !t.isEmpty && !t.startsWith "#"
  let words := ((para.getD "").replace "\n" " ").splitOn " " |>.filter (!·.isEmpty)
  let text := " ".intercalate words
  clipTo limit (firstSentence (text.splitOn ". "))
where
  /-- Joins the pieces `splitOn ". "` produced back up to the first one whose last word is not an
  abbreviation, and closes it with the period the split removed. -/
  firstSentence : List String → String
    | [] => ""
    | [last] => last
    | piece :: rest =>
      let lastWord := (piece.splitOn " ").getLast?.getD ""
      if lastWord.any (· == '.') then piece ++ ". " ++ firstSentence rest
      else piece ++ "."

/-- What an upstream constant says beyond its type: a definition's value, or a structure's fields
one per line. Empty for a theorem (its type is its statement, and its proof is not something a
reader of this site is being asked to read) and for anything else.

Clipped at `maxExternalValue`. `Expr` is a DAG and printed syntax is a tree, so a value can expand
by orders of magnitude — the failure recorded in `KNOWN-ISSUES.md`, where one target printed to
34 MB. `Meta.ppExpr` hides implicit arguments and so is far tamer than the fully-explicit printing
that produced that, but the cap is cheap and the panel is a preview either way. -/
def maxExternalValue : Nat := 1200

/-- See `maxExternalValue`. -/
def externalValueString (env : Environment) (info : ConstantInfo) : IO String := do
  match info with
  | .defnInfo val => return clipTo maxExternalValue (← ppExprString env val.value)
  | .inductInfo val =>
    -- A structure or class: what it says is its fields, which live in its single constructor's
    -- telescope after the structure's own parameters.
    match val.ctors with
    | [ctor] =>
      let lines ← runCoreIO env <| Lean.Meta.MetaM.run' do
        let some ci := (← getEnv).find? ctor | return (#[] : Array String)
        Lean.Meta.forallTelescopeReducing ci.type fun xs _ =>
          (xs.extract val.numParams xs.size).mapM fun x => do
            return s!"{← x.fvarId!.getUserName} : {← Lean.Meta.ppExpr (← Lean.Meta.inferType x)}"
      return clipTo maxExternalValue (String.intercalate "\n" lines.toList)
    | _ => return ""
  | _ => return ""

/-- The most characters one binder type in a `StatementAnatomy` keeps; the conclusion gets twice
this and a definition's body `maxAnatomyBody`. The card shows the full source directly below, so
the anatomy only has to be legible. -/
def maxAnatomyType : Nat := 800

/-- The most characters of a definition's value the parts view shows. The source is one fold away,
and `Expr` is a DAG where printed syntax is a tree, so a value can print far larger than it reads. -/
def maxAnatomyBody : Nat := 2500

/-- Whether a run of text inside a notation stands for the notation's constant — `∫`, `∂`, `≤`,
`∑` — rather than being the punctuation around its arguments: `(`, `), `, `:`. -/
def isNotationText (s : String) : Bool :=
  s.toList.any fun c => !(c.isWhitespace || "(),:;[]{}".contains c)

/-- The pieces of tagged pretty-printer output — see `ppPieces`.

A tag whose term is a constant and whose content is bare text is that constant's name. One whose
content has structure is a *notation* for the constant — `a ≤ b` is tagged `LE.le` as a whole,
`∫ x, f x ∂μ` is tagged `MeasureTheory.integral` — so its arguments are descended into for their own
constants, and the runs of text that are the notation itself, `outer` here, stand for the constant,
which is what gives `∫` a hover. Any other tag is looked through.

`partial` because the recursion is through the `Array` inside `TaggedText`, and threading `outer`
through it is more than the structural-recursion checker follows. -/
partial def taggedPieces (outer : Name) : Lean.Widget.CodeWithInfos → Array TypePiece
  | .text s => #[{ text := s, const := if isNotationText s then outer else .anonymous }]
  | .append parts => parts.flatMap (taggedPieces outer)
  | .tag info inner =>
    -- Two shapes of term info: the delaborator's own, which carries a hover location and a
    -- docstring override, and the plain one. Both know the term.
    let expr? : Option Expr :=
      match info.info.val.info with
      | Elab.Info.ofTermInfo ti => some ti.expr
      | Elab.Info.ofDelabTermInfo di => some di.expr
      | _ => none
    match expr?.map Expr.consumeMData, inner with
    | some (.const n _), .text s => #[{ text := s, const := n }]
    | some (.const n _), _ => taggedPieces n inner
    | _, _ => taggedPieces .anonymous inner

/-- Pretty-prints `e` as text and as `TypePiece`s: the same text, split so that every token the
pretty printer knows to be a constant is its own piece and names it. Function heads are tagged only
under `pp.tagAppFns`, which `statementAnatomyOf` switches on. -/
def ppPieces (e : Expr) (limit : Nat) : MetaM (String × Array TypePiece) := do
  let tagged ← Lean.Widget.ppExprTagged e
  return (clipTo limit tagged.stripTags,
    clipPieces limit (coalescePieces (taggedPieces .anonymous tagged)))

/-- A structure's fields as `StatementField`s, in the context `params` — the structure's own
parameters as free variables, so that field types print with the same names as the parameters
above them. Field docstrings live on the projections, `S.field`. -/
def structureFieldsOf (structName : Name) (params : Array Expr) : MetaM (Array StatementField) := do
  let env ← getEnv
  let some (.inductInfo val) := env.find? structName | return #[]
  let [ctor] := val.ctors | return #[]
  let some ctorInfo := env.find? ctor | return #[]
  if params.size != val.numParams then return #[]
  let ctorType ← instantiateForall ctorInfo.type params
  forallTelescope ctorType (cleanupAnnotations := true) fun fs _ => do
    let mut out : Array StatementField := #[]
    for f in fs do
      let decl ← f.fvarId!.getDecl
      let type := decl.type.consumeMData
      let fieldName := decl.userName.eraseMacroScopes
      let doc := (← findDocString? env (structName ++ fieldName)).getD ""
      let (typeStr, pieces) ← ppPieces type maxAnatomyType
      out := out.push {
        name := fieldName.toString
        type := typeStr
        pieces
        head := (type.getForallBody.getAppFn.constName?).getD .anonymous
        doc := clipTo 3000 doc }
    return out

/-- A definition's value with its parameters substituted, as the thing to show under its result
type. For a recursive definition the stored value is what the equation compiler produced —
`brecOn`, `WellFounded.fix` — which nobody wrote and nobody can read, so the right-hand side of its
unfolding equation is shown instead, which has the `match` the author wrote. -/
def definitionBodyOf (name : Name) (val : DefinitionVal) (params : Array Expr) : MetaM Expr := do
  let unfolded? ← try getUnfoldEqnFor? name catch _ => pure none
  match unfolded? with
  | some eqn =>
    let eqType ← instantiateForall (← inferType (.const eqn (val.levelParams.map mkLevelParam))) params
    match eqType.eq? with
    | some (_, _, rhs) => return rhs
    | none => return val.value.beta params
  | none => return val.value.beta params

/-- A declaration taken apart by binder role (`StatementAnatomy`): for a theorem its assumptions and
its claim, for a definition its parameters, its result type and its body — a structure's fields, or
a definition's value. `none` when anything about it fails to print.

The telescope is *not* reduced: a theorem stated as `IsFoo x` where `IsFoo` unfolds to a `∀` is shown
with the shape the author gave it, which is the one the code block has. Binder types are printed
inside the telescope so they carry the author's names, with the declaration's own namespaces open
so that scoped notation prints, as `mkDocstringBlock?` does. The body is the elaborated value with
the parameters substituted rather than the source text, so that it prints in the same context and
vocabulary as everything above it; the source is in the folded code block underneath. -/
def statementAnatomyOf (env : Environment) (name : Name) (info : ConstantInfo) :
    IO (Option StatementAnatomy) := do
  -- `pp.tagAppFns`: without it the pretty printer tags a constant only where it is an argument,
  -- and the one constant a reader most wants to hover — the predicate at the head of a hypothesis —
  -- would be the one without a hover.
  let coreCtx : Core.Context := {
    fileName := "<referee>", fileMap := default
    options := Options.empty.setBool `pp.tagAppFns true }
  let openDecls := (namespaceAncestors name.getPrefix).map (OpenDecl.simple · [])
  let act : MetaM (Option StatementAnatomy) :=
    forallTelescope info.type (cleanupAnnotations := true) fun xs body => do
      let conclusionIsProp ← try isProp body catch _ => pure false
      let mut indexOf : Std.HashMap FVarId Nat := {}
      let mut binders : Array StatementBinder := #[]
      for x in xs do
        let decl ← x.fvarId!.getDecl
        let type := decl.type.consumeMData
        let isHyp ← try isProp type catch _ => pure false
        -- By the type, not only by the brackets: Mathlib-style statements bind measurable-space
        -- structure as `{mΩ : MeasurableSpace Ω}` so that it can be named, and to a reader that is
        -- the same assumption as `[MeasurableSpace Ω]`.
        let isClass ← try (·.isSome) <$> isClass? type catch _ => pure false
        let role : BinderRole :=
          match decl.binderInfo with
          | .instImplicit => .typeclass
          | _ => if isClass then .typeclass else if isHyp then .hypothesis else .object
        let implicit :=
          match decl.binderInfo with
          | .implicit | .strictImplicit => true
          | _ => false
        let mentions := (collectFVars {} type).fvarIds.filterMap fun fv => indexOf.get? fv
        let (typeStr, pieces) ← ppPieces type maxAnatomyType
        binders := binders.push {
          name := if decl.userName.hasMacroScopes then "" else decl.userName.toString
          role
          isType := type.isSort
          implicit
          type := typeStr
          pieces
          head := (type.getForallBody.getAppFn.constName?).getD .anonymous
          mentions
        }
        indexOf := indexOf.insert x.fvarId! (binders.size - 1)
      -- What a definition produces, beyond its type. A theorem's proof is not shown, not being part
      -- of what the theorem says; an `opaque`'s value is hidden on purpose; and an inductive type
      -- with several constructors is described by its source, which the card keeps open.
      let mut bodyStr := ""
      let mut bodyPieces : Array TypePiece := #[]
      let mut fields : Array StatementField := #[]
      if !conclusionIsProp then
        match info with
        | .defnInfo val =>
          let (s, ps) ← ppPieces (← definitionBodyOf name val xs) maxAnatomyBody
          bodyStr := s
          bodyPieces := ps
        | .inductInfo _ =>
          if isStructure env name then
            fields ← structureFieldsOf name xs
        | _ => pure ()
      let (conclusion, conclusionPieces) ← ppPieces body (2 * maxAnatomyType)
      return some {
        binders
        conclusion
        conclusionHead := (body.getForallBody.getAppFn.constName?).getD .anonymous
        conclusionPieces
        isProp := conclusionIsProp
        body := bodyStr
        bodyPieces
        fields
      }
  try
    (act.run' {}).toIO' { coreCtx with currNamespace := name.getPrefix, openDecls } { env := env }
  catch _ =>
    pure none

/-- The most constants one upstream package may contribute before it is left unexpanded.

The budget is what lets this run without knowing which packages the reader will trust. `--trust` is a
render-time flag by design, so `collect` cannot be told which packages matter; instead every upstream
package is walked and the ones that do not fit are abandoned. Mathlib exceeds this within a few steps
and is recorded as the flat surface it always was; a small sibling like `LeanMachineLearning` — 15
declarations of surface out of `AlphaRAR` — finishes immediately and gets its internal structure
drawn. The cutoff is a legibility bound as much as a cost one: a block of 500 nodes is not a picture
anyone reads. -/
def maxExpandedPackage : Nat := 500

/-- The meaning edges of an *upstream* constant: the same rule `meaningDepsOf` applies to the
project's own declarations, restated for a constant that has no `DeclInfo`.

A theorem contributes its statement, a definition its type and the data in its value, everything else
its type and whatever its constructors and field defaults mention. -/
def upstreamMeaningDeps (env : Environment) (name : Name) (info : ConstantInfo) :
    Lean.Meta.MetaM (Array Name) := do
  match info with
  | .thmInfo _ => return MeaningGraph.exprUsedConstants info.type
  | .defnInfo _ =>
    return MeaningGraph.usedConstantsOf env name info (includeValue := false)
      ++ (← MeaningGraph.dataValueConstants info)
  | _ => return MeaningGraph.usedConstantsOf env name info (includeValue := true)

/-- What a dependency of an upstream constant should appear as: itself, or — when it is a
compiler-generated helper — whatever it in turn references.

The same treatment `MeaningGraph.expandThroughInternals` gives the project's own declarations,
restated here because that one is scoped to the project. Without it an `_autoParam` (the tactic
behind a structure field's default) or a `match_1` becomes a node in the picture, and nobody
wrote it. Recursion is guarded by `seen`, so a helper referring to itself terminates. -/
partial def upstreamVisibleDeps (env : Environment) (packages : Array PackageInfo) (pkg : Name)
    (seen : Std.HashSet Name) (d : Name) : Lean.Meta.MetaM (Array Name) := do
  if !MeaningGraph.isInternalName d then return #[d]
  if seen.contains d then return #[]
  let some info := env.find? d | return #[]
  let ds ← try upstreamMeaningDeps env d info catch _ => pure #[]
  let mut out : Array Name := #[]
  for e in ds do
    if e == d then continue
    match moduleNameOf env e with
    | some m =>
      if modulePackageOf packages m == some pkg then
        out := out ++ (← upstreamVisibleDeps env packages pkg (seen.insert d) e)
    | none => pure ()
  return out

/-- Closes each upstream package's surface over the package's own internal edges, up to
`maxExpandedPackage`.

Returns the intra-package edges of every constant reached, and the packages that finished inside the
budget. A package that overruns contributes nothing: its constants keep the records `externalDeclsOf`
builds for them and are drawn flat, so overrunning degrades the picture rather than breaking it. -/
def expandUpstream (env : Environment) (packages : Array PackageInfo)
    (surface : Array (Name × Name)) : IO (Std.HashMap Name (Array Name) × Array Name) := do
  runCoreIO env <| Lean.Meta.MetaM.run' do
    let mut seeds : Std.HashMap Name (Array Name) := {}
    for (c, pkg) in surface do
      seeds := seeds.insert pkg ((seeds.getD pkg #[]).push c)
    let mut edges : Std.HashMap Name (Array Name) := {}
    let mut expanded : Array Name := #[]
    for (pkg, start) in seeds.toArray.qsort (fun a b => Name.lt a.1 b.1) do
      let mut pkgEdges : Std.HashMap Name (Array Name) := {}
      let mut seen : Std.HashSet Name := {}
      let mut frontier := start
      let mut withinBudget := true
      while withinBudget && !frontier.isEmpty do
        let mut next : Array Name := #[]
        for n in frontier do
          if seen.contains n then continue
          if seen.size ≥ maxExpandedPackage then
            withinBudget := false
            break
          seen := seen.insert n
          let some info := env.find? n | continue
          let ds ← try upstreamMeaningDeps env n info catch _ => pure #[]
          -- Only edges that stay inside the package. One leaving it either points at the project,
          -- which depends on the package rather than the other way round, or at another package,
          -- whose expansion is decided on its own terms.
          let mut acc : Std.HashSet Name := {}
          for d in ds do
            if d == n then continue
            match moduleNameOf env d with
            | some m =>
              if modulePackageOf packages m == some pkg then
                for v in ← upstreamVisibleDeps env packages pkg {} d do
                  if v != n then acc := acc.insert v
            | none => pure ()
          let inPkg := acc.toArray.qsort Name.lt
          pkgEdges := pkgEdges.insert n inPkg
          for d in inPkg do
            if !seen.contains d then next := next.push d
        frontier := next
      if withinBudget then
        expanded := expanded.push pkg
        for (k, v) in pkgEdges.toArray do
          edges := edges.insert k v
    return (edges, expanded)

/-- Every constant outside the project that some declaration's *statement* names, with its package,
module, signature and docstring.

Collected so that a declaration's dependency graph can show the upstream declarations it rests on,
not merely count them — and, since these are exactly the nodes where a reader's trust has to start,
so that clicking one answers "is this the definition I think it is" without leaving the site.
Restricted to the meaning edges (`meaningDepsOf`) and to constants that resolve to a package: this is
the set that can appear as a node, and collecting all of `deps` instead would multiply it by every
proof-only reference, none of which the graph shows.

The signature is pretty-printed here rather than at render time because `build-site` has no
environment: the whole point of the phase split is that it runs on the JSON alone. -/
def externalDeclsOf (env : Environment) (packages : Array PackageInfo) (rootPrefix : Name)
    (decls : Array DeclInfo) : IO (Array ExternalDeclInfo × Array Name) := do
  let byName := decls.foldl (init := ({} : Std.HashMap Name Name)) fun acc decl =>
    (meaningDepsOf decl.kind decl.isAlias decl.deps decl.typeDeps decl.dataDeps).foldl
      (init := acc) fun acc dep =>
      if acc.contains dep then acc
      else match moduleNameOf env dep with
        | none => acc
        | some moduleName =>
          if hasPrefixName moduleName rootPrefix then acc
          else match modulePackageOf packages moduleName with
            | some pkg => acc.insert dep pkg
            | none => acc
  -- Close each package over its own internal edges before building the records, because the closure
  -- reaches constants no project statement names and those need a record too — a node with no
  -- signature and no docstring is the thing this table exists to stop.
  let (edges, expanded) ← expandUpstream env packages
    (byName.toArray.qsort fun a b => Name.lt a.1 b.1)
  let mut all := byName
  for (name, _) in edges.toArray do
    if !all.contains name then
      match moduleNameOf env name with
      | none => pure ()
      | some m =>
        match modulePackageOf packages m with
        | some pkg => all := all.insert name pkg
        | none => pure ()
  let mut out : Array ExternalDeclInfo := #[]
  for (name, pkg) in all.toArray.qsort (fun a b => Name.lt a.1 b.1) do
    let some info := env.find? name | continue
    -- A failure to pretty-print one upstream type must not lose the whole table, so it degrades to
    -- the name, which is exactly what every node showed before this existed.
    let signature ← try ppExprString env info.type catch _ => pure name.toString
    let doc ← try pure ((← findDocString? env name).getD "") catch _ => pure ""
    let value ← try externalValueString env info catch _ => pure ""
    out := out.push {
      name := name
      package := pkg
      moduleName := (moduleNameOf env name).getD pkg
      signature := signature
      value := value
      doc := doc
      deps := edges.getD name #[]
    }
  return (out, expanded)

/-- The upstream packages a single declaration's own type and body reference, with the project's own
package dropped: the one-level part of `DeclInfo.upstreamPackages`, before propagation. -/
def directUpstreamPackages (env : Environment) (packages : Array PackageInfo)
    (rootPrefix : Name) (deps : Array Name) : Array Name :=
  let acc := deps.foldl (init := ({} : Std.HashSet Name)) fun acc dep =>
    match moduleNameOf env dep with
    | none => acc
    | some moduleName =>
      if hasPrefixName moduleName rootPrefix then acc
      else match modulePackageOf packages moduleName with
        | some pkg => acc.insert pkg
        | none => acc
  acc.toArray.qsort Name.lt

/-- Prints how long one step of `collect` took.

`build-site` has had phase timings since it started taking hours; `collect` never did, so the only
way to tell which of its steps is expensive was to guess. That matters more now that `--claims-only`
exists: the point of a scoped build is to skip work, and without timings there is no way to see
which work is still being done for the whole library. -/
def collectPhase (label : String) (startMs : Nat) : IO Nat := do
  let now := ← IO.monoMsNow
  IO.println s!"  [{label}] {(now - startMs) / 1000}.{((now - startMs) % 1000) / 100}s"
  return now

/-! ### The two passes

`collectDecls` runs over every exposed declaration twice, and the split is what makes
`--claims-only` worth having.

The first pass computes the facts that are *cheap per declaration*: the dependency edges, the kind,
and the four keyword questions read off the parsed source. Every file cost in it — reading the
source, parsing its commands — is paid once per *file*, and both are cached, so a project's 1901
declarations cost 161 file reads whether they are all kept or none are.

The second pass computes what is expensive per declaration and is wanted only by a page:
`ppExprString` over the type, `statementAnatomyOf` taking the statement apart, the signature and
proof text cut out of the source, the docstring rendered to blocks. On `colt-2026-83` a
`--claims-only` build runs that pass 37 times instead of 1901.

Nothing about the unscoped path changes: with no scope, the second pass runs over everything the
first produced, and the result is the same array it always was. -/

/-- What the first pass learns about a declaration: everything needed to place it in the dependency
graph and to decide whether it is in scope, and nothing that costs real work.

Holds a `ConstantInfo` and so never leaves this process — it is the hand-off between the two passes,
not a stored form. -/
structure DeclFacts where
  name : Name
  moduleName : Name
  info : ConstantInfo
  kind : DeclKind
  isLemma : Bool
  isAlias : Bool
  isInstanceDecl : Bool
  source? : Option SourceInfo
  typeDeps : Array Name
  deps : Array Name
  dataDeps : Array Name
  axioms : Array Name
  hasOwnSorry : Bool
  dependsOnSorry : Bool

/-- `meaningDepsOf` for the first pass's record: the edges a *statement* rests on. Seeds the page
scope. -/
def DeclFacts.meaningDeps (facts : DeclFacts) : Array Name :=
  meaningDepsOf facts.kind facts.isAlias facts.deps facts.typeDeps facts.dataDeps

/-- `closureDepsOf` for the first pass's record: the edges extraction inlines along. -/
def DeclFacts.closureDeps (facts : DeclFacts) : Array Name :=
  closureDepsOf facts.kind facts.isAlias facts.deps facts.typeDeps

/-! ### Discovering the scope without walking the library

A scoped build asks a reachability question from a handful of seeds. Computing every declaration's
dependencies and *then* traversing answers it, and that is what the first version did — but it costs
the whole library to learn about 2% of it, which is exactly backwards at the scale this exists for.
Measured on `colt-2026-83`, that eager first pass was 30.7s of a 35.6s `--claims-only` collect; on a
million-line library it is the difference between minutes and hours.

So a scoped build walks outward from the seeds instead, computing a declaration's edges, kind and
keywords only when the traversal actually reaches it. Source files are read and parsed only when
they contain a declaration in scope — ten files rather than a hundred and forty.

The traversal has to interleave two kinds of step, which is why it is one worklist and not two
passes. Following `meaningDeps` finds what a claim's statement rests on. Pulling in the theorems
that *speak for* a definition — `@[specifies]`, `@[characterization]` — finds what a reader needs in
order to judge it, and no dependency edge points that way. A pulled-in theorem has a statement of
its own, so the two steps feed each other until neither adds anything.

The full build keeps the eager loop. It needs every declaration anyway, so a worklist would only
add bookkeeping, and keeping the paths separate is what stops the scoped work from changing what an
unscoped build computes. Both call `declFactsOf`, so the per-declaration answer cannot drift. -/

/-- The caches the first pass threads: memoized dependency expansion, and the lines and parsed
commands of each source file.

Explicit rather than mutable locals because both the eager loop and the lazy traversal thread them
through the same `declFactsOf`, and a file read once for the eager path must not be read again. -/
structure FactsCache where
  deps : MeaningGraph.Cache := {}
  lines : Std.HashMap System.FilePath (Array String) := {}
  commands : Std.HashMap System.FilePath (Array CommandKeyword) := {}

/-- Everything the first pass learns about one declaration.

Cheap in the sense that matters: the per-file work — reading the source and running the Lean parser
over it — is paid once per file however many declarations ask for it, and the per-declaration work
is a dependency expansion and four keyword questions. What it deliberately does *not* do is anything
that costs real time per declaration; that is `declInfoOf`'s half, and a scoped build runs it 38
times instead of 1901.

`axioms` and `dependsOnSorry` are left empty here and filled by `withAxioms`, because which
declarations need them is not known until the scope is. -/
def declFactsOf (env : Environment) (projectDir : System.FilePath) (pkg : Lake.Package)
    (depsCtx : MeaningGraph.Context) (simpLemmaNames : Std.HashSet Name) (cache : FactsCache)
    (name moduleName : Name) (info : ConstantInfo) : IO (DeclFacts × FactsCache) := do
  let mut cache := cache
  let ranges? ← findRanges? env name
  let source? ← toSourceInfo? projectDir pkg moduleName ranges?
  let mut text? : Option String := none
  let lines ← match source? with
    | none => pure #[]
    | some src =>
      match cache.lines.get? src.absPath with
      | some ls => pure ls
      | none => do
          let text ← IO.FS.readFile src.absPath
          let ls := (text.splitOn "\n").toArray
          cache := { cache with lines := cache.lines.insert src.absPath ls }
          text? := some text
          pure ls
  -- The command this declaration's range falls inside, which is where its keyword is read from.
  let cmd? ← match source? with
    | none => pure none
    | some src => do
      let cmds ← match cache.commands.get? src.absPath with
        | some cs => pure cs
        | none => do
            let text ← match text? with
              | some t => pure t
              | none => IO.FS.readFile src.absPath
            let cs ← commandKeywordsOf env text src.absPath.toString
            cache := { cache with commands := cache.commands.insert src.absPath cs }
            pure cs
      pure (commandKeywordAt? cmds src.line)
  let kind := declKindOf env info name
  -- Parsed syntax when the range lands in a command, the source text otherwise.
  let isLemma := (kind == .theorem &&
      match cmd? with
      | some c => c.isLemma
      | none => isLemmaFromSource kind source? lines)
    || isSimpsGeneratedLemma env simpLemmaNames name info
  let isInstanceDecl := kind == .theorem &&
    match cmd? with
    | some c => c.isInstance
    | none => isInstanceFromSource kind source? lines
  let isInstanceDecl := isInstanceDecl || (kind == .theorem && isInstanceName name)
  let isAlias := match cmd? with
    | some c => c.isAlias
    | none => isAliasFromSource source? lines
  -- The constants this declaration rests on, recovered by `MeaningGraph` (which also looks
  -- through compiler-generated helpers and recovers the notation/coercion dependencies the
  -- elaborated term drops). The reverse notation direction — a declaration whose *source* uses a
  -- notation — is handled syntactically during extraction, where the parsed syntax is available.
  let (declDeps, depsCache) := depsCtx.declDeps cache.deps name info
  cache := { cache with deps := depsCache }
  let facts : DeclFacts := {
    name := name
    moduleName := moduleName
    info := info
    kind := kind
    isLemma := isLemma
    isAlias := isAlias
    isInstanceDecl := isInstanceDecl
    source? := source?
    typeDeps := declDeps.typeDeps
    deps := declDeps.deps
    dataDeps := declDeps.dataDeps
    axioms := #[]
    dependsOnSorry := false
    -- `allowOpaque := true` is required, not cosmetic: `ConstantInfo.value?` returns `none` for
    -- a `.thmInfo` without it, so every theorem — the declarations that actually carry a `sorry`
    -- in their proof — reported `hasOwnSorry := false`, and `sorryChain` then found no culprit
    -- and the page blamed the gap on an upstream package.
    hasOwnSorry := info.type.hasSorry ||
      ((info.value? (allowOpaque := true)).map Expr.hasSorry).getD false
  }
  return (facts, cache)

/-- Fills in what `collectAxioms` reports, once it is known which declarations need it. -/
def DeclFacts.withAxioms (facts : DeclFacts) (axs : Array Name) : DeclFacts :=
  { facts with axioms := axs, dependsOnSorry := axs.contains ``sorryAx }

/-- Exposed declaration ↦ its module and `ConstantInfo`, for a traversal that looks names up rather
than iterating. Cheap: one insert per project constant, and no analysis. -/
def exposedIndex (depsCtx : MeaningGraph.Context) :
    Std.HashMap Name (Name × ConstantInfo) :=
  depsCtx.constants.foldl (init := {}) fun acc (name, moduleName, info) =>
    if depsCtx.exposed.contains name then acc.insert name (moduleName, info) else acc

/-- Definition ↦ the theorems whose authors said what it means.

The inverse of the `@[specifies]` and `@[characterization]` tables, which are keyed by the theorem
and by the definition respectively while the traversal needs to ask "what speaks for *this*". Built
once, in time proportional to the number of annotations rather than to the library. -/
def speakersForTargets (env : Environment) : Std.HashMap Name (Array Name) := Id.run do
  let mut acc : Std.HashMap Name (Array Name) := {}
  for entry in Characterization.specEntries env do
    acc := acc.insert entry.target ((acc.getD entry.target #[]).push entry.theoremName)
  for c in Characterization.characterizations env do
    let parts := #[c.property] ++ c.existence.map (·.declName) ++ c.uniqueness.map (·.declName)
    acc := acc.insert c.target (acc.getD c.target #[] ++ parts)
  return acc

/-- What `collectDecls` hands back.

A record rather than a tuple because three of the four are answers only it is in a position to give:
it holds the `MeaningGraph.Context`, which has already walked every project constant and applied
`shouldExpose` to each. Recomputing that in the caller cost a second whole-environment scan — 26.3s
on a 32,154-declaration project, spent to print one diagnostic line. -/
structure CollectedDecls where
  decls : Array DeclInfo
  /-- The declarations a scoped build keeps the edges of; empty on a full build. -/
  thin : Array ThinDecl := #[]
  /-- Exposed declarations *before* scoping, which a scoped file cannot recompute. -/
  libraryDeclCount : Nat := 0
  /-- Project constants `shouldExpose` rejected: compiler helpers and internals. -/
  excludedNames : Array Name := #[]

/-- The first pass over every exposed declaration: the full build's path.

A plain loop, because a full build needs all of them and a worklist would only add bookkeeping. -/
def collectFactsEager (env : Environment) (projectDir : System.FilePath) (pkg : Lake.Package)
    (depsCtx : MeaningGraph.Context) (simpLemmaNames : Std.HashSet Name) :
    IO (Array DeclFacts × FactsCache) := do
  let mut cache : FactsCache := {}
  let mut facts : Array DeclFacts := #[]
  for (name, moduleName, info) in depsCtx.constants do
    if !depsCtx.exposed.contains name then
      continue
    let (f, cache') ← declFactsOf env projectDir pkg depsCtx simpLemmaNames cache name moduleName
      info
    cache := cache'
    facts := facts.push f
  return (facts, cache)

/-- The first pass from the claim seeds outward: the scoped build's path.

One worklist carrying both kinds of step — the statement edges a declaration rests on, and the
theorems that speak for a definition already reached — because each feeds the other and neither
reaches a fixpoint alone. See the section note above.

Bounded by the number of exposed declarations: a name is enqueued at most once, so the number of
levels cannot exceed the number of names, and the bound is what makes this structurally terminating
rather than merely terminating. -/
def collectFactsLazy (env : Environment) (projectDir : System.FilePath) (pkg : Lake.Package)
    (depsCtx : MeaningGraph.Context) (simpLemmaNames : Std.HashSet Name)
    (index : Std.HashMap Name (Name × ConstantInfo)) (speakers : Std.HashMap Name (Array Name))
    (seeds : Array Name) (cache : FactsCache) : IO (Array DeclFacts × FactsCache) := do
  let mut cache := cache
  let mut facts : Array DeclFacts := #[]
  let mut visited : Std.HashSet Name := {}
  let mut pending : Array Name := #[]
  for seed in seeds do
    if index.contains seed && !visited.contains seed then
      visited := visited.insert seed
      pending := pending.push seed
  for _ in [0:index.size + 1] do
    if pending.isEmpty then
      break
    let mut next : Array Name := #[]
    for name in pending do
      let some (moduleName, info) := index.get? name
        | continue
      let (f, cache') ← declFactsOf env projectDir pkg depsCtx simpLemmaNames cache name moduleName
        info
      cache := cache'
      facts := facts.push f
      -- What the statement rests on.
      for dep in f.meaningDeps do
        if index.contains dep && !visited.contains dep then
          visited := visited.insert dep
          next := next.push dep
      -- And what speaks for it, which no edge points at.
      for speaker in speakers.getD name #[] do
        if index.contains speaker && !visited.contains speaker then
          visited := visited.insert speaker
          next := next.push speaker
    pending := next
  return (facts, cache)

/-- Walks outward from `start` along `edge`, computing facts on demand, and returns the
declarations reached that are not already `known`.

Both thin tiers are this shape, and both are traversals a scoped build must not pay the library for:
the extraction closure a minimal file inlines along, and the declarations a `sorry` chain passes
through. `admit` decides whether a reached declaration is kept *and* whether the walk continues
through it — which is what lets the `sorry` tier prune at declarations that cannot reach a gap. -/
def expandTier (env : Environment) (projectDir : System.FilePath) (pkg : Lake.Package)
    (depsCtx : MeaningGraph.Context) (simpLemmaNames : Std.HashSet Name)
    (index : Std.HashMap Name (Name × ConstantInfo)) (known : Std.HashSet Name)
    (start : Array Name) (edge : DeclFacts → Array Name)
    (admit : Array DeclFacts → IO (Array DeclFacts)) (cache : FactsCache) :
    IO (Array DeclFacts × FactsCache) := do
  let mut cache := cache
  let mut out : Array DeclFacts := #[]
  let mut visited : Std.HashSet Name := known
  let mut pending : Array Name := #[]
  for name in start do
    if !visited.contains name then
      visited := visited.insert name
      pending := pending.push name
  -- `start` itself is already known; the walk begins at its edges.
  let mut frontier : Array Name := #[]
  for name in start do
    if let some (moduleName, info) := index.get? name then
      let (f, cache') ← declFactsOf env projectDir pkg depsCtx simpLemmaNames cache name moduleName
        info
      cache := cache'
      for dep in edge f do
        if index.contains dep && !visited.contains dep then
          visited := visited.insert dep
          frontier := frontier.push dep
  for _ in [0:index.size + 1] do
    if frontier.isEmpty then
      break
    let mut reached : Array DeclFacts := #[]
    for name in frontier do
      let some (moduleName, info) := index.get? name
        | continue
      let (f, cache') ← declFactsOf env projectDir pkg depsCtx simpLemmaNames cache name moduleName
        info
      cache := cache'
      reached := reached.push f
    let kept ← admit reached
    out := out ++ kept
    let mut next : Array Name := #[]
    for f in kept do
      for dep in edge f do
        if index.contains dep && !visited.contains dep then
          visited := visited.insert dep
          next := next.push dep
    frontier := next
  return (out, cache)

/-- Collects all exposed declarations and computes their primary metadata. The dependency lists
(`deps`, `typeDeps`) come from `MeaningGraph`; everything else — signature, docstring, source
snippet, kind, `sorry` status — is computed here.

`scopeSeeds?` switches the first pass from the eager loop to the traversal described above, so that
a scoped build's cost is proportional to what it renders rather than to the library. Returns the
full declarations and, when scoped, the thin tier: the dropped declarations two analyses still need
the edges of. See `ThinDecl`. -/
def collectDecls (projectDir : System.FilePath) (rootPrefix : Name)
    (pkg : Lake.Package) (env : Environment) (packages : Array PackageInfo := #[])
    (scopeSeeds? : Option (Array Name) := none) : IO CollectedDecls := do
  -- `withDataValueConsts` is what lets `declDeps` report `dataDeps`; without it every `dataDeps`
  -- would silently equal `deps` and the graph would be unchanged. It needs `MetaM` because deciding
  -- whether a constructor field is `Prop`-valued is a typing question.
  let tStart ← IO.monoMsNow
  let depsCtx ← runCoreIO env
    (Lean.Meta.MetaM.run' (MeaningGraph.Context.of env rootPrefix).withDataValueConsts)
  let tCtx ← collectPhase "dependency context" tStart
  let simpTheorems ← runCoreIO env Lean.Meta.getSimpTheorems
  let simpLemmaNames : Std.HashSet Name :=
    simpTheorems.lemmaNames.fold (fun acc origin =>
      match origin with
      | .decl declName .. => acc.insert declName
      | _ => acc) {}
  -- The project's `@[specifies]` annotations, grouped by the theorem carrying them. Reading them
  -- needs no cooperation from the target beyond depending on `Characterization`: the entries ride
  -- in the `.olean`s and are matched to this process's copy of the extension by name during
  -- `importModules (loadExts := true)`. A project without the dependency yields an empty array.
  let specsByTheorem : Std.HashMap Name (Array SpecLink) :=
    (Characterization.specEntries env).foldl (init := {}) fun acc entry =>
      let link : SpecLink := { name := entry.target, comment := entry.comment }
      acc.insert entry.theoremName ((acc.getD entry.theoremName #[]).push link)
  -- The `@[characterization]` annotations, already assembled into bundles by `Characterization` and
  -- keyed by the definition each claims to pin down. Incomplete bundles are kept rather than
  -- dropped: a property with no uniqueness theorem is a claim its author started and did not
  -- finish, which is worth showing as such and not worth silently rendering as a characterization.
  let charsByTarget : Std.HashMap Name (Array CharBundle) :=
    (Characterization.characterizations env).foldl (init := {}) fun acc c =>
      let bundle : CharBundle := {
        property := c.property
        comment := c.comment
        existence := c.existence.map (·.declName)
        uniqueness := c.uniqueness.map fun e =>
          { name := e.declName, relation := e.relation, relationHead := e.relationHead } }
      acc.insert c.target ((acc.getD c.target #[]).push bundle)
  -- ## First pass
  let index := if scopeSeeds?.isNone then {} else exposedIndex depsCtx
  let (facts, cache) ← match scopeSeeds? with
    | none => collectFactsEager env projectDir pkg depsCtx simpLemmaNames
    | some seeds =>
      collectFactsLazy env projectDir pkg depsCtx simpLemmaNames index
        (speakersForTargets env) seeds {}
  let tFacts ← collectPhase
    s!"pass 1: edges and keywords, {facts.size} declarations in {cache.commands.size} files" tCtx
  -- `collectAxioms` for exactly the declarations that were reached. On a full build that is every
  -- exposed declaration, as it always was; on a scoped one it is the scope, which is the only set
  -- whose axioms any page reports.
  let declAxioms ← axiomsOfDecls env (facts.map (·.name))
  let facts := facts.map fun f => f.withAxioms (declAxioms.getD f.name #[])
  let tAxioms ← collectPhase s!"collectAxioms, {facts.size} declarations" tFacts
  -- ## The thin tier
  --
  -- Two walks, both from the scope outward and neither over the library. The second is bounded far
  -- more tightly than it looks: `sorryChain` walks `deps` to the first declaration carrying its own
  -- `sorry`, and every declaration on such a path depends on the `sorry` below it — so one with
  -- `dependsOnSorry := false` cannot reach a gap and cannot lie on any chain. Pruning there loses
  -- no chain, and on a project with no `sorry` anywhere the walk never starts.
  let scopeNames : Std.HashSet Name := facts.foldl (fun acc f => acc.insert f.name) {}
  let (thinFacts, _cache) ← match scopeSeeds? with
    | none => pure (#[], cache)
    | some _ => do
      let (inlined, cache) ← expandTier env projectDir pkg depsCtx simpLemmaNames index scopeNames
        (facts.map (·.name)) DeclFacts.closureDeps (fun reached => pure reached) cache
      let sorried := facts.filterMap fun f => if f.dependsOnSorry then some f.name else none
      if sorried.isEmpty then
        pure (inlined, cache)
      else
        let known := inlined.foldl (fun acc f => acc.insert f.name) scopeNames
        let (chained, cache) ← expandTier env projectDir pkg depsCtx simpLemmaNames index known
          sorried (·.deps)
          (fun reached => do
            -- Batched per level rather than per declaration: one `CoreM` run for the whole
            -- frontier instead of one apiece.
            let axs ← axiomsOfDecls env (reached.map (·.name))
            pure <| reached.filterMap fun f =>
              let f := f.withAxioms (axs.getD f.name #[])
              if f.dependsOnSorry then some f else none)
          cache
        pure (inlined ++ chained, cache)
  let thin : Array ThinDecl := thinFacts.map fun f => {
    name := f.name
    moduleName := f.moduleName
    kind := f.kind
    isAlias := f.isAlias
    deps := f.deps
    typeDeps := f.typeDeps
    hasOwnSorry := f.hasOwnSorry
    dependsOnSorry := f.dependsOnSorry
  }
  let tThin ← collectPhase s!"thin tier: {thin.size} declarations" tAxioms
  -- ## Second pass: the expensive analysis, for the declarations that get a page
  let fileLines := cache.lines
  let mut decls := #[]
  for f in facts do
    let name := f.name
    let info := f.info
    let kind := f.kind
    let source? := f.source?
    -- A hit by construction: the first pass read every source file it could and left them here.
    let lines := match source? with
      | none => #[]
      | some src => fileLines.getD src.absPath #[]
    let expandedSignature ← ppExprString env info.type
    let anatomy? ← statementAnatomyOf env name info
    -- Before the signature, not after: an attribute-generated declaration has no source of its own
    -- to display and falls back to the pretty-printed type, which has to be introduced by the
    -- keyword the author actually wrote or the code block says `theorem` under a card labelled
    -- "Lemma".
    let displaySignature :=
      (displaySignatureFromSource kind source? lines).getD <|
        displaySignatureFallback kind name expandedSignature (isLemma := f.isLemma)
    let proofText? := proofTextFromSource kind source? lines
    let doc? ← findDocString? env name
    let docBlocks :=
      match doc? with
      | some doc => markdownToBlocks doc
      | none => #[]
    let decl : DeclInfo := {
      name := name
      moduleName := f.moduleName
      modulePath := modulePathOf rootPrefix f.moduleName
      groupKey := groupKeyOfModule rootPrefix f.moduleName
      kind := kind
      displaySignature := displaySignature
      expandedSignature := expandedSignature
      anatomy? := anatomy?
      docBlocks := docBlocks
      docText? := doc?
      proofText? := proofText?
      source? := source?
      dependsOnSorry := f.dependsOnSorry
      hasOwnSorry := f.hasOwnSorry
      axioms := f.axioms
      isLemma := f.isLemma
      isInstanceDecl := f.isInstanceDecl
      isAlias := f.isAlias
      specifies := specsByTheorem.getD name #[]
      -- Only the forward direction here; `attachCharacterizes` fills in `characterizes` on the
      -- three declarations each bundle is made of, exactly as `attachSpecifiedBy` does.
      characterizedBy := charsByTarget.getD name #[]
      -- One level here; `attachUpstreamPackages` propagates it along the project's own edges.
      -- The edges `closureDeps` picks: a theorem's *statement*, everything else's body too. A
      -- theorem's proof is not a trust dependency — the kernel checked it.
      -- `isAliasFromSource` rather than `f.isAlias`, which prefers the parsed command keyword:
      -- this is what the single-pass version passed, and the two disagree on a declaration whose
      -- range lands in a command. Kept exactly as it was so the split changes no output.
      upstreamPackages := directUpstreamPackages env packages rootPrefix
        (meaningDepsOf kind (isAliasFromSource source? lines) f.deps f.typeDeps f.dataDeps)
      deps := f.deps
      typeDeps := f.typeDeps
      dataDeps := f.dataDeps
    }
    decls := decls.push decl
  let _ ← collectPhase s!"pass 2: full analysis, {decls.size} declarations" tThin
  -- Straight off the context, which walked every project constant to build `exposed` in the first
  -- place. The caller used to ask the environment the same question a second time.
  let excludedNames := depsCtx.constants.filterMap fun (name, _, _) =>
    if depsCtx.exposed.contains name then none else some name
  pure { decls, thin, libraryDeclCount := depsCtx.exposed.size, excludedNames }

/-! ## Dependency-graph passes

Each of these is a thin adapter that projects `decls` onto the plain `(name, deps)` graph the
`MeaningGraph` passes work on, runs the pass, and writes the result back into the corresponding
`DeclInfo` field. What varies between them is only *which* edges they follow — full `deps` for
`usedBy`, `closureDeps` for the extraction closure and `meaningDeps` for the meaning closure.
-/

/-- Adds reverse dependency links (`usedBy`) between exposed declarations, sorted by name. -/
def attachReverseDeps (decls : Array DeclInfo) : Array DeclInfo :=
  let rev := MeaningGraph.reverseDeps (decls.map fun decl => (decl.name, decl.deps))
  decls.map fun decl => { decl with usedBy := (rev.getD decl.name #[]).qsort Name.lt }

/-- `closureDepsOf` for a `DeclInfo`. Drives `transDeps`, and through it extraction; also the
module-level graph, which is about what a module needs in order to build rather than about what it
means.

Not a way to "see through proofs", despite being the wider of the two rules: it widens over
`meaningDeps` for *definitions* only, and for a non-alias theorem both are `typeDeps`. Anything that
has to follow a theorem's proof — the `sorry` chain is the one such caller — must take `decl.deps`
directly. -/
def closureDeps (decl : DeclInfo) : Array Name :=
  closureDepsOf decl.kind decl.isAlias decl.deps decl.typeDeps

/-- The hand-off to `ChallengeGen`: the four fields the extraction reads, out of the twenty-odd a
`DeclInfo` carries.

The narrowness is the point. Extraction needs to know what a declaration is called, what kind it
is, which module to read it from, and what to inline with it; everything else here — signatures,
docstrings, specification links, trust, provenance — is this tool's business and not a challenge
generator's, and passing it along would be how `ChallengeGen` acquired Verso.

`transDeps` rather than `deps`: the closure is already taken over `closureDeps` edges, which keep a
theorem's proof, because a file whose kept tactic blocks lost the lemmas they call would not
compile. `ChallengeGen` neither computes the closure nor chooses its edges — see the note on
`closureDepsOf` for why that choice belongs here. -/
def DeclInfo.toChallengeDecl (decl : DeclInfo) : ChallengeDecl where
  name := decl.name
  kind := decl.kind
  moduleName := decl.moduleName
  transDeps := decl.transDeps

/-- `meaningDepsOf` for a `DeclInfo`: what the declaration claims and what that claim rests on, with
every proof dropped.

This is what the site follows nearly everywhere — the dependency graph and its node set
(`dataTransDeps`), the upstream-trust analysis, the audit closure and its coverage, and the
revision diff's meaning propagation. All of them ask a version of "what must I accept in order to
believe this", and the answer never includes a lemma some proof merely called. -/
def meaningDeps (decl : DeclInfo) : Array Name :=
  meaningDepsOf decl.kind decl.isAlias decl.deps decl.typeDeps decl.dataDeps

/-! ## Integrity of the collected data

`MeaningGraph`'s `Proofs.lean` proves these properties of the *functions* that build the closures —
`transitiveDeps_closed`, `topologicalClosure_nodup`, `mem_topologicalClosure_of_mem_start`. What the
site renders has been through `toJson`, `intern`, a file, `Json.parse`, `resolve` and `fromJson?`,
and the round trip across that boundary is *not* proved — see `Proofs/Collect.lean` for why it is
out of reach in this toolchain — so a theorem about the producer establishes nothing about the value
the renderer holds.

Since format version 12 the closures themselves no longer make that trip: `CollectedData.withClosures`
recomputes them in-process, after decoding, from the direct edges. That narrows what these checks
defend against, and they are kept for what remains. The *edges* still cross the unproved boundary, a
corrupted or truncated file still deserves a report rather than a render, and the recomputation has
wiring of its own that a proof about `transitiveDeps` does not cover — seeding from `closureDeps`
versus `meaningDeps` per declaration kind, and the map the closure is taken over. A future change
that stops routing a closure through `MeaningGraph.transitiveDeps` is caught here and nowhere else.

The site is a trust instrument; rendering a closure that is quietly wrong is worse than failing.
-/

/-- How many violations to list before summarizing. A corrupt file tends to fail every check at
once, and a wall of near-identical lines buries the useful first one. -/
def maxReportedViolations : Nat := 12

/-- Internal consistency checks on decoded collected data, as reader-facing messages. Empty when the
data satisfies everything `MeaningGraph`'s `Proofs.lean` proves of the functions that produced it.

Each check names the theorem it restates, so a failure points at whether the *property* is wrong or
the *data* is. -/
def CollectedData.integrityViolations (data : CollectedData) : Array String := Id.run do
  let byName : Std.HashMap Name DeclInfo :=
    data.decls.foldl (fun m d => m.insert d.name d) {}
  -- The extraction closure walks through the thin tier, so closure-closedness has to be checked
  -- through it too: without these edges a scoped file would pass the check by treating every thin
  -- declaration as a leaf, which is the one reading that cannot fail.
  let thinClosureEdges : Std.HashMap Name (Array Name) :=
    data.thinDecls.foldl (fun m t => m.insert t.name t.closureDeps) {}
  let mut out : Array String := #[]
  for decl in data.decls do
    for (label, closure, direct) in
        #[("transDeps", decl.transDeps, closureDeps decl),
          ("dataTransDeps", decl.dataTransDeps, meaningDeps decl)] do
      let isTrans := label == "transDeps"
      let inClosure : Std.HashSet Name := closure.foldl (fun s n => s.insert n) {}
      -- `transitiveDeps` filters the declaration itself out of its own closure.
      if closure.contains decl.name then
        out := out.push s!"{decl.name}: {label} contains the declaration itself"
      -- `topologicalClosure_nodup`.
      if inClosure.size != closure.size then
        out := out.push s!"{decl.name}: {label} has repeated entries           ({closure.size} entries, {inClosure.size} distinct)"
      -- `mem_topologicalClosure_of_mem_start`: the closure contains what it was seeded with.
      for d in direct do
        unless d == decl.name || inClosure.contains d do
          out := out.push s!"{decl.name}: {label} omits its direct dependency {d}"
      -- `transitiveDeps_closed`: the closure is closed under taking dependencies. Only project
      -- declarations have recorded edges; an upstream constant is a leaf here.
      for y in closure do
        let yDirect? : Option (Array Name) :=
          match byName[y]? with
          | some ydecl => some (if isTrans then closureDeps ydecl else meaningDeps ydecl)
          -- Absent from `decls`: an upstream constant, which is a leaf, or — only ever in a scoped
          -- file — a thin declaration the extraction closure walked through.
          | none => if isTrans && !thinClosureEdges.isEmpty then thinClosureEdges[y]? else none
        if let some yDirect := yDirect? then
          for z in yDirect do
            unless z == decl.name || inClosure.contains z do
              out := out.push s!"{decl.name}: {label} is not closed — contains {y},                 which depends on {z}, which is absent"
  return out

/-- Formats `integrityViolations` for a command-line error, truncated to `maxReportedViolations`. -/
def CollectedData.integrityReport (data : CollectedData) : Option String :=
  let vs := data.integrityViolations
  if vs.isEmpty then none
  else
    let shown := vs.extract 0 maxReportedViolations
    let more := if vs.size > maxReportedViolations then
        s!"\n  … and {vs.size - maxReportedViolations} more" else ""
    some <| "collected data failed its own consistency checks:\n  "
      ++ String.intercalate "\n  " shown.toList ++ more

/-- Adds the reverse of the `@[specifies]` links: each definition learns which of the exposed
theorems its author declared to be part of its specification.

Kept in declaration order rather than sorted by name, unlike `attachReverseDeps` — a specification
is a short, deliberately ordered list, and the order its author wrote it in is the order it reads
best in. A link whose target is not an exposed declaration (a Mathlib definition, say) simply has
nowhere to land here; it stays visible on the theorem's own `specifies`. -/
def attachSpecifiedBy (decls : Array DeclInfo) : Array DeclInfo :=
  let rev : Std.HashMap Name (Array SpecLink) :=
    decls.foldl (init := {}) fun acc decl =>
      decl.specifies.foldl (init := acc) fun acc link =>
        let back : SpecLink := { name := decl.name, comment := link.comment }
        acc.insert link.name ((acc.getD link.name #[]).push back)
  decls.map fun decl => { decl with specifiedBy := rev.getD decl.name #[] }

/-- Adds the reverse of the `@[characterization]` links: each of the three declarations a bundle is
made of learns which definition it helps pin down, and in what role.

The counterpart of `attachSpecifiedBy`, and needed for the same reason in the other direction. A
reader who lands on `IsEntropy.unique` sees a lemma about a predicate; what they are missing is that
it is the half of a claim about `entropy`, which nothing in the statement says. A part whose bundle
names a definition outside the project has nowhere to land in `characterizedBy`, so it never reaches
this function — the link is only ever built from bundles already attached to an exposed
definition. -/
def attachCharacterizes (decls : Array DeclInfo) : Array DeclInfo :=
  let rev : Std.HashMap Name (Array CharPartLink) :=
    decls.foldl (init := {}) fun acc decl =>
      decl.characterizedBy.foldl (init := acc) fun acc bundle =>
        let add (acc : Std.HashMap Name (Array CharPartLink)) (part : Name) (role : String) :=
          let link : CharPartLink := { target := decl.name, property := bundle.property, role }
          acc.insert part ((acc.getD part #[]).push link)
        let acc := add acc bundle.property "property"
        let acc := bundle.existence.foldl (fun acc n => add acc n "existence") acc
        bundle.uniqueness.foldl (fun acc u => add acc u.name "uniqueness") acc
  decls.map fun decl => { decl with characterizes := rev.getD decl.name #[] }

/-! ## Semantic hashes

Read from a JSONL file produced by [`semantic_hash export`](https://github.com/mathlib-initiative/semantic_hash),
one `{"name": ..., "hash": ..., "proofIrrelHash": ...}` object per line. That tool is run separately,
against the same project, and is not a build dependency of this one — which is deliberate. It
enforces a toolchain match against the project it reads, exactly as this tool does, and taking it as
a Lake dependency would mean a *third* toolchain that also has to line up. A file on disk has no
such constraint, and keeps the phase boundary the pipeline is built on: everything that needs the
environment produces data, and everything downstream is a pure function of it.

The hashes matter to Referee for one reason. `expandedSignature` is a *pretty-printed* elaborated
type, and a toolchain upgrade can change how every type in a library prints at once — which turns
the revision diff into a page telling the reader to re-audit everything. A structural hash of the
`Expr` cannot do that. See `Referee.Diff` for what it is used for and where it is not trusted. -/

/-- Renders a 64-bit hash as fixed-width hex.

Fixed width, and base 16, so the result reads as an identifier rather than as a number someone might
compare with `<` — these are compared for equality and for nothing else. -/
def hex16 (n : UInt64) : String :=
  let hexDigit (d : Nat) : Char :=
    if d < 10 then Char.ofNat (d + '0'.toNat) else Char.ofNat (d - 10 + 'a'.toNat)
  let rec go (n : UInt64) (fuel : Nat) (acc : String) : String :=
    match fuel with
    | 0 => acc
    | fuel + 1 => go (n / 16) fuel (String.singleton (hexDigit (n % 16).toNat) ++ acc)
  go n 16 ""

/-- Reads one hash field of a `semantic_hash` JSONL record.

Accepts a JSON string or a JSON number. Lean serializes `UInt64` as a *decimal string*, since
JavaScript cannot hold 64 bits in a number, so the string form is what the tool actually writes
today; the numeric branch is there so that a change of heart upstream degrades to nothing rather
than to a silently empty hash table. Either way the value is canonicalized to `hex16`, so a file
written under either convention compares equal to one written under the other. -/
def parseHashField? (j : Json) : Option String :=
  let n? : Option Nat :=
    match j with
    | .str s => s.toNat?
    | .num _ => j.getNat?.toOption
    | _ => none
  n?.map fun n => hex16 (UInt64.ofNat n)

/-- Declaration ↦ (`hash`, `proofIrrelHash`), read from a `semantic_hash export` JSONL file.

Lines that do not parse are skipped rather than fatal, and the caller reports the coverage it got.
A hash file is an *optimization of the comparison key*: a partial one costs a partial upgrade, and
failing the whole collection over a malformed line would trade a good outcome for no outcome. -/
def readSemanticHashes (path : System.FilePath) : IO (Std.HashMap Name (String × String)) := do
  let contents ← IO.FS.readFile path
  let mut out : Std.HashMap Name (String × String) := {}
  for line in contents.splitOn "\n" do
    -- No trimming: `Json.parse` already tolerates surrounding whitespace, and a line that is
    -- nothing but whitespace simply fails to parse and is skipped with the rest.
    if line.isEmpty then continue
    let .ok json := Json.parse line | continue
    let .ok nameStr := json.getObjValAs? String "name" | continue
    let some hash := (json.getObjVal? "hash").toOption.bind parseHashField? | continue
    let some proofIrrel :=
      (json.getObjVal? "proofIrrelHash").toOption.bind parseHashField? | continue
    let name := nameStr.toName
    if name.isAnonymous then continue
    out := out.insert name (hash, proofIrrel)
  return out

/-- Attaches the semantic hashes to the declarations they name.

A declaration the export does not mention keeps `none` and is compared as text, so this never has
to be complete to be useful. -/
def attachSemanticHashes (hashes : Std.HashMap Name (String × String))
    (decls : Array DeclInfo) : Array DeclInfo :=
  decls.map fun decl =>
    match hashes.get? decl.name with
    | some (hash, proofIrrel) =>
      { decl with semanticHash? := some hash, proofIrrelHash? := some proofIrrel }
    | none => decl

/-- Propagates the directly-referenced upstream packages along the project's own dependency edges,
so that each declaration's `upstreamPackages` covers everything its project-level closure touches.

Follows `meaningDeps`, the same edges the rest of the trust analysis follows, for the reason recorded
there: a proof is not something a reader has to trust further, because the kernel checked it. What a
reader must take on faith from upstream is a *definition* their statements are about — so a package
reached only by a lemma that some proof called is not a package this declaration rests on, whether
that proof is a theorem's or one bundled into a definition's value.

Reuses `MeaningGraph.transitiveDeps` for the closure rather than iterating a fixpoint: the closure
is over 784-ish project declarations, not over the environment, so it is cheap and already
written. -/
def attachUpstreamPackages (decls : Array DeclInfo) : Array DeclInfo :=
  let depsMap : Std.HashMap Name (Array Name) :=
    decls.foldl (fun acc decl => acc.insert decl.name (meaningDeps decl)) {}
  let ownPkgs : Std.HashMap Name (Array Name) :=
    decls.foldl (fun acc decl => acc.insert decl.name decl.upstreamPackages) {}
  decls.map fun decl =>
    let closure := #[decl.name] ++ MeaningGraph.transitiveDeps depsMap decl.name
    let acc := closure.foldl (init := ({} : Std.HashSet Name)) fun acc name =>
      (ownPkgs.getD name #[]).foldl (init := acc) (·.insert ·)
    { decl with upstreamPackages := acc.toArray.qsort Name.lt }

/-- Adds the transitive closure of `closureDeps` to each declaration as `transDeps`, topologically
ordered so that every dependency precedes the declarations that use it (suitable for emitting a
minimal standalone Lean file).

This is the *extraction* closure and is deliberately wider than what the site reports: see
`dataTransDeps` for the meaning closure the reader is shown. -/
def attachTransitiveDeps (decls : Array DeclInfo) (thin : Array ThinDecl := #[]) :
    Array DeclInfo :=
  -- Thin declarations contribute *edges* and receive nothing. A scoped build drops declarations a
  -- minimal file still has to inline — a definition's body drags in the lemmas discharging its
  -- embedded proof obligations, which `meaningDeps` rightly leaves out of the graph and extraction
  -- rightly needs — and without their edges here the closure would stop at the scope boundary and
  -- the extracted file would silently lose what it needs to compile.
  let depsMap : Std.HashMap Name (Array Name) :=
    thin.foldl (init := decls.foldl (fun acc decl => acc.insert decl.name (closureDeps decl)) {})
      fun acc t => acc.insert t.name t.closureDeps
  decls.map fun decl => { decl with transDeps := MeaningGraph.transitiveDeps depsMap decl.name }

/-- Adds the transitive closure of `meaningDeps` as `dataTransDeps`, exactly as
`attachTransitiveDeps` does for `closureDeps`.

This is the node set of a declaration's dependency graph: the declarations its *meaning* rests on. -/
def attachDataTransitiveDeps (decls : Array DeclInfo) : Array DeclInfo :=
  let depsMap : Std.HashMap Name (Array Name) :=
    decls.foldl (fun acc decl => acc.insert decl.name (meaningDeps decl)) {}
  decls.map fun decl => { decl with dataTransDeps := MeaningGraph.transitiveDeps depsMap decl.name }

/-- Fills in `transDeps` and `dataTransDeps` for every declaration, from the direct edges.

Every consumer of collected data calls this exactly once, right after obtaining it — after
`decodeCollectedData` on the file paths, after `collectData` on the in-process `all` path — and no
producer stores the result. That single call site is what preserves the property the old
collect-time computation had: the graph, the closure listings, the audit queues and extraction all
read the same arrays, so they cannot disagree about what a closure contains.

Overwrites whatever the fields held, rather than filling only when empty. A version-11 file arrives
with closures; ignoring them in favor of the recomputation means every render is backed by the
in-process functions `MeaningGraph`'s `Proofs.lean` reasons about, regardless of the file's age, and
a version-11 file whose stored closures had been corrupted is corrected rather than trusted.

The cost is one `transitiveDeps` walk per declaration per closure kind — linear in the total number
of closure entries, seconds at 28k declarations. It is paid on load instead of at collect time
because storing the result is what did not scale: materialized closures measured at 69.9% of
`data.json` on `Mathlib.Analysis`, against 12.6% for the direct edges they derive from. -/
def CollectedData.withClosures (data : CollectedData) : CollectedData :=
  -- Only the extraction closure walks through the thin tier. The meaning closure must not: the page
  -- scope is closed under `meaningDeps` by construction, so a thin declaration appearing in a
  -- `dataTransDeps` would be a graph node with no data behind it — and letting the edges through
  -- here is exactly how that would happen.
  { data with
    decls := attachDataTransitiveDeps (attachTransitiveDeps data.decls data.thinDecls) }

end Referee