ci: Import Archive when checking YAML files (#11562)

We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`.

It also changes the hyperlinks to Archive to instead list declarations directly.

Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612).

Co-authored-by: Enrico Borba <enricozb@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Archive/Imo/Imo1986Q5.lean

@@ -54,7 +54,7 @@ theorem map_of_lt_two (hx : x < 2) : f x = 2 / (2 - x) := by
   have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx
   apply le_antisymm
   · rw [NNReal.le_div_iff hx', ← NNReal.le_div_iff' hfx, tsub_le_iff_right, ← hf.map_eq_zero,
-     hf.map_add, div_mul_cancel _ hfx, hf.map_two, zero_mul]
+     hf.map_add, div_mul_cancel₀ _ hfx, hf.map_two, zero_mul]
   · rw [NNReal.div_le_iff' hx', ← hf.map_eq_zero]
     refine (mul_eq_zero.1 ?_).resolve_right hfx
     rw [hf.map_add_rev, hf.map_eq_zero, tsub_add_cancel_of_le hx.le]
@@ -77,7 +77,7 @@ theorem isGood_iff {f : ℝ≥0 → ℝ≥0} : IsGood f ↔ f = fun x ↦ 2 / (2
     cases lt_or_le y 2 with
     | inl hy =>
       have hy' : 2 - y ≠ 0 := (tsub_pos_of_lt hy).ne'
-      rw [div_mul_div_comm, tsub_mul, mul_assoc, div_mul_cancel _ hy', mul_comm x,
+      rw [div_mul_div_comm, tsub_mul, mul_assoc, div_mul_cancel₀ _ hy', mul_comm x,
         ← mul_tsub, tsub_add_eq_tsub_tsub_swap, mul_div_mul_left _ _ two_ne_zero]
     | inr hy =>
       have : 2 ≤ x + y := le_add_left hy

Archive/OxfordInvariants/Summer2021/Week3P1.lean

@@ -137,7 +137,7 @@ theorem OxfordInvariants.Week3P1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤
         rw [Finset.sum_range_succ, hb, Finset.mul_sum]
         congr; ext i
         rw [← mul_div_assoc, ← mul_div_right_comm, mul_div_assoc,
-          mul_div_cancel _ (a_pos _ <| Nat.le_succ _).ne', mul_comm]
+          mul_div_cancel_right₀ _ (a_pos _ <| Nat.le_succ _).ne', mul_comm]
   -- Check the divisibility condition
   · rw [mul_tsub, ← mul_assoc, Nat.mul_div_cancel' ha, add_mul, Nat.mul_div_cancel' han,
       add_tsub_tsub_cancel ha₀, add_tsub_cancel_right]

Archive/Wiedijk100Theorems/HeronsFormula.lean

@@ -67,7 +67,7 @@ theorem heron {p1 p2 p3 : P} (h1 : p1 ≠ p2) (h2 : p3 ≠ p2) :
       field_simp [numerator, denominator, ab2_nonneg]; ring
     _ = ↑1 / ↑4 * √ (s * (s - a) * (s - b) * (s - c) * ↑4 ^ 2) := by simp only [s]; ring_nf
     _ = √ (s * (s - a) * (s - b) * (s - c)) := by
-      rw [sqrt_mul', sqrt_sq, div_mul_eq_mul_div, one_mul, mul_div_cancel] <;> norm_num
+      rw [sqrt_mul', sqrt_sq, div_mul_eq_mul_div, one_mul, mul_div_cancel_right₀] <;> norm_num
 #align theorems_100.heron Theorems100.heron
 
 end Theorems100

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -28,7 +28,7 @@ open scoped BigOperators
 open Finset
 
 /-- **Sum of the Reciprocals of the Triangular Numbers** -/
-theorem Theorem100.inverse_triangle_sum :
+theorem Theorems100.inverse_triangle_sum :
     ∀ n, ∑ k in range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n := by
   refine' sum_range_induction _ _ (if_pos rfl) _
   rintro (_ | n)
@@ -38,4 +38,4 @@ theorem Theorem100.inverse_triangle_sum :
   push_cast
   field_simp
   ring
-#align theorem_100.inverse_triangle_sum Theorem100.inverse_triangle_sum
+#align theorem_100.inverse_triangle_sum Theorems100.inverse_triangle_sum

docs/100.yaml

@@ -28,8 +28,7 @@
   title  : The Impossibility of Trisecting the Angle and Doubling the Cube
 9:
   title  : The Area of a Circle
-  links  :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/AreaOfACircle.lean
+  decl   : Theorems100.area_disc
   author : James Arthur, Benjamin Davidson, and Andrew Souther
 10:
   title  : Euler’s Generalization of Fermat’s Little Theorem
@@ -55,9 +54,8 @@
   author : Yury G. Kudryashov (first) and Benjamin Davidson (second)
 16:
   title  : Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem)
-  author: Thomas Browning
-  links :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/AbelRuffini.lean
+  author : Thomas Browning
+  decl   : AbelRuffini.exists_not_solvable_by_rad
 17:
   title  : De Moivre’s Formula
   decl   : Complex.cos_add_sin_mul_I_pow
@@ -110,8 +108,7 @@
 30:
   title  : The Ballot Problem
   author : Bhavik Mehta, Kexing Ying
-  links  :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/BallotProblem.lean
+  decl   : Ballot.ballot_problem
 31:
   title  : Ramsey’s Theorem
   author : Bhavik Mehta
@@ -139,8 +136,7 @@
 37:
   title  : The Solution of a Cubic
   author : Jeoff Lee
-  links  :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/SolutionOfCubic.lean
+  decl   : Theorems100.cubic_eq_zero_iff
 38:
   title  : Arithmetic Mean/Geometric Mean
   decl   : Real.geom_mean_le_arith_mean_weighted
@@ -161,8 +157,7 @@
 42:
   title  : Sum of the Reciprocals of the Triangular Numbers
   author : Jalex Stark, Yury Kudryashov
-  links :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/InverseTriangleSum.lean
+  decl   : Theorems100.inverse_triangle_sum
 43:
   title  : The Isoperimetric Theorem
 44:
@@ -172,8 +167,7 @@
 45:
   title  : The Partition Theorem
   author : Bhavik Mehta, Aaron Anderson
-  links:
-    mathlib archive: https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean
+  decl   : Theorems100.partition_theorem
 46:
   title  : The Solution of the General Quartic Equation
 47:
@@ -198,8 +192,7 @@
   title  : Pi is Transcendental
 54:
   title  : Königsberg Bridges Problem
-  links:
-    mathlib archive: https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Konigsberg.lean
+  decl   : Konigsberg.not_isEulerian
   author : Kyle Miller
 55:
   title  : Product of Segments of Chords
@@ -209,8 +202,7 @@
   title  : The Hermite-Lindemann Transcendence Theorem
 57:
   title  : Heron’s Formula
-  links :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/HeronsFormula.lean
+  decl   : Theorems100.heron
   author : Matt Kempster
 58:
   title  : Formula for the Number of Combinations
@@ -269,8 +261,7 @@
   author : mathlib
 70:
   title  : The Perfect Number Theorem
-  links  :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/PerfectNumbers.lean
+  decl   : Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect
   author : Aaron Anderson
 71:
   title  : Order of a Subgroup
@@ -287,8 +278,7 @@
   author : Chris Hughes
 73:
   title  : Ascending or Descending Sequences (Erdős–Szekeres Theorem)
-  links  :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean
+  decl   : Theorems100.erdos_szekeres
   author : Bhavik Mehta
 74:
   title  : The Principle of Mathematical Induction
@@ -301,7 +291,7 @@
   author : Yury G. Kudryashov
 76:
   title  : Fourier Series
-  decls   :
+  decls  :
     - fourierCoeff
     - hasSum_fourier_series_L2
   author : Heather Macbeth
@@ -333,19 +323,17 @@
   note   : "it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain."
 81:
   title  : Divergence of the Prime Reciprocal Series
-  links  :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean
-  decl   : not_summable_one_div_on_primes
+  decls  :
+    - Theorems100.Real.tendsto_sum_one_div_prime_atTop
+    - not_summable_one_div_on_primes
   author : Manuel Candales (archive), Michael Stoll (Mathlib)
 82:
   title  : Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof)
-  links :
-    mathlib archive : https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/CubingACube.lean
+  decl   : Theorems100.«82».cannot_cube_a_cube
   author : Floris van Doorn
 83:
   title  : The Friendship Theorem
-  links  :
-    mathlib archive: https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
+  decl   : Theorems100.friendship_theorem
   author : Aaron Anderson, Jalex Stark, Kyle Miller
 84:
   title  : Morley’s Theorem
@@ -385,8 +373,9 @@
   title  : Pick’s Theorem
 93:
   title  : The Birthday Problem
-  links  :
-    mathlib archive: https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/BirthdayProblem.lean
+  decls  :
+    - Theorems100.birthday
+    - Theorems100.birthday_measure
   author : Eric Rodriguez
 94:
   title  : The Law of Cosines

scripts/checkYaml.lean

@@ -43,7 +43,7 @@ def processDb (decls : ConstMap) : String × String → IO Bool
     return false
 
 unsafe def main : IO Unit := do
-  CoreM.withImportModules #[`Mathlib]
+  CoreM.withImportModules #[`Mathlib, `Archive]
       (searchPath := compile_time_search_path%) (trustLevel := 1024) do
     let decls := (←getEnv).constants
     let results ← databases.mapM (fun p => processDb decls p)

scripts/yaml_check.py

@@ -27,19 +27,19 @@ def flatten_names(data: List[Tuple[List[str], str]]) -> List[Tuple[str, str]]:
   return [(' :: '.join(id), v) for id, v in data]
 
 def print_list(fn: str, pairs: List[Tuple[str, str]]) -> None:
-  with open(fn, 'w') as out:
+  with open(fn, 'w', encoding='utf8') as out:
     for (id, val) in pairs:
       out.write(f'{id}\n{val.strip()}\n\n')
 
 hundred_yaml = sys.argv[1]
 overview_yaml = sys.argv[2]
 undergrad_yaml = sys.argv[3]
 
-with open(hundred_yaml, 'r') as hy:
+with open(hundred_yaml, 'r', encoding='utf8') as hy:
   hundred = yaml.safe_load(hy)
-with open(overview_yaml, 'r') as hy:
+with open(overview_yaml, 'r', encoding='utf8') as hy:
   overview = yaml.safe_load(hy)
-with open(undergrad_yaml, 'r') as hy:
+with open(undergrad_yaml, 'r', encoding='utf8') as hy:
   undergrad = yaml.safe_load(hy)
 
 hundred_decls:List[Tuple[str, str]] = []
@@ -49,6 +49,8 @@ def print_list(fn: str, pairs: List[Tuple[str, str]]) -> None:
   if 'decl' in entry:
     hundred_decls.append((f'{index} {title}', entry['decl']))
   elif 'decls' in entry:
+    if not isinstance(entry['decls'], list):
+      raise ValueError(f"For key {index} ({title}): did you mean `decl` instead of `decls`?")
     hundred_decls = hundred_decls + [(f'{index} {title}', d) for d in entry['decls']]
 
 overview_decls = tiered_extract(overview)