import Mathlib

/-!
Dump the names of the public theorems of `Init`, `Std` and `Batteries` visible after
`import Mathlib`, as JSON Lines (`{"name", "module"}`).

Run from `lean_project/` (done by `scripts/build_index.py --extra-names`):

    FORMAL_MAS_NAMES_OUT=<file> lake env lean <this file>

These names only feed the Retriever's `unknown identifier` suggestions; they are never
added to the search index (BM25 or dense), so the Phase 1.4 evaluation still holds.
Excluded here: the `Lean` namespace, private and internal names, deprecated aliases and
instances; auto-generated equation/congruence lemmas are dropped in Python.
-/

open Lean Meta Elab Command

#eval show CommandElabM Unit from do
  let some out ← IO.getEnv "FORMAL_MAS_NAMES_OUT"
    | throwError "set FORMAL_MAS_NAMES_OUT to the output path"
  let prefixes : List Name := [`Init, `Std, `Batteries]
  let env ← getEnv
  let h ← IO.FS.Handle.mk out .write
  let mut emitted : Nat := 0
  for (n, ci) in env.constants.map₁.toList do
    let .thmInfo _ := ci | continue
    let some idx := env.getModuleIdxFor? n | continue
    let mod := env.header.moduleNames[idx.toNat]!
    unless prefixes.any (·.isPrefixOf mod) do continue
    if (`Lean).isPrefixOf n || isPrivateName n || n.isInternalDetail
        || Linter.isDeprecated env n || isInstanceCore env n then
      continue
    h.putStrLn <| Json.compress <| Json.mkObj [
      ("name", toJson n.toString), ("module", toJson mod.toString)]
    emitted := emitted + 1
  h.flush
  logInfo m!"extract_names: emitted {emitted}"