[Merged by Bors] - feat: warn on deprecated declarations in scripts/check-yaml

scripts/check-yaml.lean

@@ -1,20 +1,22 @@
 /-
 Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Eric Wieser
+Authors: Eric Wieser, Thomas R. Murrills
 -/
-import Mathlib.Lean.CoreM
-import Mathlib.Tactic.ToExpr
+module
+
+import Lean.Data.Json
+import Lean.Linter.Deprecated
 
 /-! # Script to check `undergrad.yaml`, `overview.yaml`, `100.yaml` and `1000.yaml`
 
 This assumes `yaml_check.py` has first translated these to `json` files.
 
-It verifies that the referenced declarations exist, and prints an error otherwise.
+It verifies that the referenced declarations exist and are not deprecated, and prints an error
+otherwise.
 -/
 
-open IO.FS Lean Lean.Elab
-open Lean Core Elab Command
+open Lean
 
 abbrev DBFile := Array (String × Name)
 
@@ -25,25 +27,29 @@ def readJsonFile (α) [FromJson α] (path : System.FilePath) : IO α := do
 def databases : List String :=
   ["undergrad", "overview", "100", "1000"]
 
-def processDb (decls : ConstMap) : String → IO Bool
-| file => do
+def processDb (env : Environment) (file : String) : IO Bool := do
   let lines ← readJsonFile DBFile s!"{file}.json"
-  let missing := lines.filter (fun l ↦ !(decls.contains l.2))
-  if 0 < missing.size then
-    IO.println s!"Entries in `docs/{file}.yaml` refer to {missing.size} declaration(s) that don't exist. \
-      Please correct the following:"
-    for p in missing do
-      IO.println s!"  {p.1}: {p.2}"
-    IO.println ""
-    return true
-  else
-    return false
-
-unsafe def main : IO Unit := do
-  let searchPath ← addSearchPathFromEnv (← getBuiltinSearchPath (← findSysroot))
-  CoreM.withImportModules #[`Mathlib, `Archive]
-      (searchPath := searchPath) (trustLevel := 1024) do
-    let decls := (← getEnv).constants
-    let results ← databases.mapM (fun p ↦ processDb decls p)
-    if results.any id then
+  let mut missing := #[]; let mut deprecated := #[]
+  for entry@(_, decl) in lines do
+    if !env.contains decl then
+      missing := missing.push entry
+    else if let some newName := Linter.getDeprecatedNewName env decl then
+      deprecated := deprecated.push (entry, newName)
+  unless missing.isEmpty do
+    IO.println s!"Entries in `docs/{file}.yaml` refer to {missing.size} declaration(s) that don't \
+      exist. Please correct the following:"
+    for (key, decl) in missing do
+      IO.println s!"  {key}: '{decl}'"
+  unless deprecated.isEmpty do
+    IO.println s!"Entries in `docs/{file}.yaml` refer to {deprecated.size} declaration(s) that are \
+      deprecated. Please update the document to refer to the following declaration(s):"
+    for ((key, decl), newName) in deprecated do
+      IO.println s!"  {key}: '{newName}' (previously '{decl}')"
+  return missing.isEmpty && deprecated.isEmpty
+
+public unsafe def main : IO Unit := do
+  initSearchPath (← findSysroot)
+  withImportModules #[`Mathlib, `Archive] ∅ (trustLevel := 1024) fun env => do
+    let results ← databases.mapM (fun p ↦ processDb env p)
+    unless results.all id do
       IO.Process.exit 1