Trigger CI for leanprover/lean4#2972

.github/workflows/bors.yml

@@ -260,7 +260,10 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.3.0-rc2
+          git checkout toolchain/v4.3.0
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..

.github/workflows/build.yml

@@ -267,7 +267,10 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.3.0-rc2
+          git checkout toolchain/v4.3.0
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..

.github/workflows/build.yml.in

@@ -246,7 +246,10 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.3.0-rc2
+          git checkout toolchain/v4.3.0
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..

.github/workflows/build_fork.yml

@@ -264,7 +264,10 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.3.0-rc2
+          git checkout toolchain/v4.3.0
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -93,16 +93,14 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
         · have := ht₃ v
           have := he₃ v
           simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
-              Bool.not_eq_true', AList.lookup_insert]
+              Bool.not_eq_true', AList.lookup_insert, imp_false]
           obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
           split <;> rename_i h'
           · subst h'
             simp_all
           · simp_all? says simp_all only [ne_eq, hasNestedIf, Bool.or_self, hasConstantIf,
               and_self, hasRedundantIf, Bool.or_false, beq_eq_false_iff_ne, not_false_eq_true,
-              disjoint, List.disjoint, decide_not, Bool.and_true, Bool.and_eq_true,
-              Bool.not_eq_true', decide_eq_false_iff_not, true_and]
-            constructor <;> assumption
+              disjoint, List.disjoint, decide_True, Bool.and_self]
         · have := ht₃ w
           have := he₃ w
           by_cases h : w = v

Archive/Imo/Imo1972Q5.lean

@@ -27,7 +27,7 @@ from `hneg` directly), finally raising a contradiction with `k' < k'`.
 theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x * g y)
     (hf2 : ∀ y, ‖f y‖ ≤ 1) (hf3 : ∃ x, f x ≠ 0) (y : ℝ) : ‖g y‖ ≤ 1 := by
   -- Suppose the conclusion does not hold.
-  by_contra' hneg
+  by_contra! hneg
   set S := Set.range fun x => ‖f x‖
   -- Introduce `k`, the supremum of `f`.
   let k : ℝ := sSup S
@@ -82,8 +82,8 @@ This is a more concise version of the proof proposed by Ruben Van de Velde.
 -/
 theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x * g y)
     (hf2 : BddAbove (Set.range fun x => ‖f x‖)) (hf3 : ∃ x, f x ≠ 0) (y : ℝ) : ‖g y‖ ≤ 1 := by
-  -- porting note: moved `by_contra'` up to avoid a bug
-  by_contra' H
+  -- porting note: moved `by_contra!` up to avoid a bug
+  by_contra! H
   obtain ⟨x, hx⟩ := hf3
   set k := ⨆ x, ‖f x‖
   have h : ∀ x, ‖f x‖ ≤ k := le_ciSup hf2

Archive/Imo/Imo1994Q1.lean

@@ -75,7 +75,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1)
     _ = (m + 1) * (n + 1) := by rw [sum_const, card_fin, Nat.nsmul_eq_mul]
   -- It remains to prove the key inequality, by contradiction
   rintro k -
-  by_contra' h : a k + a (rev k) < n + 1
+  by_contra! h : a k + a (rev k) < n + 1
   -- We exhibit `k+1` elements of `A` greater than `a (rev k)`
   set f : Fin (m + 1) ↪ ℕ :=
     ⟨fun i => a i + a (rev k), by

Archive/Imo/Imo2008Q4.lean

@@ -68,7 +68,7 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
     field_simp at H₂ ⊢
     linear_combination 1 / 2 * H₂
   have h₃ : ∀ x > 0, f x = x ∨ f x = 1 / x := by simpa [sub_eq_zero] using h₂
-  by_contra' h
+  by_contra! h
   rcases h with ⟨⟨b, hb, hfb₁⟩, ⟨a, ha, hfa₁⟩⟩
   obtain hfa₂ := Or.resolve_right (h₃ a ha) hfa₁
   -- f(a) ≠ 1/a, f(a) = a

Archive/Imo/Imo2013Q5.lean

@@ -35,7 +35,7 @@ namespace Imo2013Q5
 
 theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
     (h : ∀ n : ℕ, 0 < n → x ^ n - 1 < y ^ n) : x ≤ y := by
-  by_contra' hxy
+  by_contra! hxy
   have hxmy : 0 < x - y := sub_pos.mpr hxy
   have hn : ∀ n : ℕ, 0 < n → (x - y) * (n : ℝ) ≤ x ^ n - y ^ n := by
     intro n _
@@ -68,7 +68,7 @@ theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
 theorem le_of_all_pow_lt_succ' {x y : ℝ} (hx : 1 < x) (hy : 0 < y)
     (h : ∀ n : ℕ, 0 < n → x ^ n - 1 < y ^ n) : x ≤ y := by
   refine' le_of_all_pow_lt_succ hx _ h
-  by_contra' hy'' : y ≤ 1
+  by_contra! hy'' : y ≤ 1
   -- Then there exists y' such that 0 < y ≤ 1 < y' < x.
   let y' := (x + 1) / 2
   have h_y'_lt_x : y' < x :=
@@ -163,7 +163,7 @@ theorem fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
       (x : ℝ) + (a ^ N - x : ℚ) ≤ f x + (a ^ N - x : ℚ) := by gcongr; exact H5 x hx
       _ ≤ f x + f (a ^ N - x) := by gcongr; exact H5 _ h_big_enough
   have hxp : 0 < x := by positivity
-  have hNp : 0 < N := by by_contra' H; rw [le_zero_iff.mp H] at hN; linarith
+  have hNp : 0 < N := by by_contra! H; rw [le_zero_iff.mp H] at hN; linarith
   have h2 :=
     calc
       f x + f (a ^ N - x) ≤ f (x + (a ^ N - x)) := H2 x (a ^ N - x) hxp (by positivity)

Archive/Imo/Imo2021Q1.lean

@@ -124,7 +124,7 @@ theorem imo2021_q1 :
   have hBsub : B ⊆ Finset.Icc n (2 * n) := by
     intro c hcB; simpa only [Finset.mem_Icc] using h₂ c hcB
   have hB' : 2 * 1 < (B ∩ (Finset.Icc n (2 * n) \ A) ∪ B ∩ A).card := by
-    rw [←inter_distrib_left, sdiff_union_self_eq_union, union_eq_left.2 hA,
+    rw [← inter_distrib_left, sdiff_union_self_eq_union, union_eq_left.2 hA,
       inter_eq_left.2 hBsub]
     exact Nat.succ_le_iff.mp hB
   -- Since B has cardinality greater or equal to 3, there must exist a subset C ⊆ B such that

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -136,8 +136,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
   -- Finished both goals!
   -- Now that we have uniqueness of each label, it remains to do some counting to finish off.
   -- Suppose all the labels are small.
-  by_contra q
-  push_neg at q
+  by_contra! q
   -- Then the labels `(a_i, b_i)` all fit in the following set: `{ (x,y) | 1 ≤ x ≤ r, 1 ≤ y ≤ s }`
   let ran : Finset (ℕ × ℕ) := (range r).image Nat.succ ×ˢ (range s).image Nat.succ
   -- which we prove here.

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -72,6 +72,7 @@ def countedSequence (p q : ℕ) : Set (List ℤ) :=
   {l | l.count 1 = p ∧ l.count (-1) = q ∧ ∀ x ∈ l, x = (1 : ℤ) ∨ x = -1}
 #align ballot.counted_sequence Ballot.countedSequence
 
+open scoped List in
 /-- An alternative definition of `countedSequence` that uses `List.Perm`. -/
 theorem mem_countedSequence_iff_perm {p q l} :
     l ∈ countedSequence p q ↔ l ~ List.replicate p (1 : ℤ) ++ List.replicate q (-1) := by

Cache/Hashing.lean

@@ -76,7 +76,7 @@ def getRootHash : IO UInt64 := do
       pure ((← mathlibDepPath) / ·)
   let hashs ← rootFiles.mapM fun path =>
     hashFileContents <$> IO.FS.readFile (qualifyPath path)
-  return hash ((hash Lean.versionString) :: hashs)
+  return hash (hash Lean.githash :: hashs)
 
 /--
 Computes the hash of a file, which mixes:
@@ -86,14 +86,13 @@ Computes the hash of a file, which mixes:
 * The hashes of the imported files that are part of `Mathlib`
 -/
 partial def getFileHash (filePath : FilePath) : HashM $ Option UInt64 := do
-  let stt ← get
-  match stt.cache.find? filePath with
+  match (← get).cache.find? filePath with
   | some hash? => return hash?
   | none =>
     let fixedPath := (← IO.getPackageDir filePath) / filePath
     if !(← fixedPath.pathExists) then
       IO.println s!"Warning: {fixedPath} not found. Skipping all files that depend on it"
-      set { stt with cache := stt.cache.insert filePath none }
+      modify fun stt => { stt with cache := stt.cache.insert filePath none }
       return none
     let content ← IO.FS.readFile fixedPath
     let fileImports := getFileImports content pkgDirs
@@ -102,7 +101,7 @@ partial def getFileHash (filePath : FilePath) : HashM $ Option UInt64 := do
       match importHash? with
       | some importHash => importHashes := importHashes.push importHash
       | none =>
-        set { stt with cache := stt.cache.insert filePath none }
+        modify fun stt => { stt with cache := stt.cache.insert filePath none }
         return none
     let rootHash := (← get).rootHash
     let pathHash := hash filePath.components

Cache/IO.lean

@@ -70,7 +70,7 @@ def CURLBIN :=
 
 /-- leantar version at https://github.com/digama0/leangz -/
 def LEANTARVERSION :=
-  "0.1.9"
+  "0.1.10"
 
 def EXE := if System.Platform.isWindows then ".exe" else ""
 
@@ -221,7 +221,7 @@ def validateLeanTar : IO Unit := do
     pure <|
       if System.Platform.getIsOSX () then s!"{arch}-apple-darwin"
       else s!"{arch}-unknown-linux-musl"
-  IO.println s!"leantar is too old; downloading more recent version"
+  IO.println s!"installing leantar {LEANTARVERSION}"
   IO.FS.createDirAll IO.CACHEDIR
   let ext := if win then "zip" else "tar.gz"
   let _ ← runCmd "curl" #[
@@ -361,4 +361,16 @@ def cleanCache (keep : Lean.RBTree FilePath compare := default) : IO Unit := do
   for path in ← getFilesWithExtension CACHEDIR "ltar" do
     if !keep.contains path then IO.FS.removeFile path
 
+/-- Prints the LTAR file and embedded comments (in particular, the mathlib commit that built the
+file) regarding the files with specified paths. -/
+def lookup (hashMap : HashMap) (paths : List FilePath) : IO Unit := do
+  let mut err := false
+  for path in paths do
+    let some hash := hashMap.find? path | err := true
+    let ltar := CACHEDIR / hash.asLTar
+    IO.println s!"{path}: {ltar}"
+    for line in (← runCmd (← getLeanTar) #["-k", ltar.toString]).splitOn "\n" |>.dropLast do
+      println! "  comment: {line}"
+  if err then IO.Process.exit 1
+
 end Cache.IO

Cache/Main.lean

@@ -20,6 +20,7 @@ Commands:
   unpack!      Decompress linked already downloaded files (no skipping)
   clean        Delete non-linked files
   clean!       Delete everything on the local cache
+  lookup       Show information about cache files for the given lean files
 
   # Privilege required
   put          Run 'mk' then upload linked files missing on the server
@@ -59,7 +60,7 @@ def curlArgs : List String :=
   ["get", "get!", "get-", "put", "put!", "commit", "commit!"]
 
 def leanTarArgs : List String :=
-  ["get", "get!", "pack", "pack!", "unpack"]
+  ["get", "get!", "pack", "pack!", "unpack", "lookup"]
 
 open Cache IO Hashing Requests System in
 def main (args : List String) : IO Unit := do
@@ -102,4 +103,5 @@ def main (args : List String) : IO Unit := do
     if !(← isGitStatusClean) then IO.println "Please commit your changes first" return else
     commit hashMap true (← getToken)
   | ["collect"] => IO.println "TODO"
+  | "lookup" :: args => lookup hashMap (toPaths args)
   | _ => println help

Counterexamples/CharPZeroNeCharZero.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Eric Wieser
 -/
 import Mathlib.Algebra.CharP.Basic
+import Mathlib.Algebra.PUnitInstances
 
 #align_import char_p_zero_ne_char_zero from "leanprover-community/mathlib"@"328375597f2c0dd00522d9c2e5a33b6a6128feeb"
 

Counterexamples/CliffordAlgebra_not_injective.lean

@@ -80,7 +80,7 @@ theorem mul_self_mem_kIdeal_of_X0_X1_X2_mul_mem {x : MvPolynomial (Fin 3) (ZMod
   obtain rfl := Finset.mem_singleton.1 (support_monomial_subset hm')
   rw [mem_ideal_span_X_image] at this
   obtain ⟨i, _, hi⟩ := this m hm
-  simp_rw [←one_add_one_eq_two]
+  simp_rw [← one_add_one_eq_two]
   refine ⟨i, Nat.add_le_add ?_ ?_⟩ <;> rwa [Nat.one_le_iff_ne_zero]
 
 /-- `𝔽₂[α, β, γ] / (α², β², γ²)` -/
@@ -233,7 +233,7 @@ theorem gen_mul_gen (i) : gen i * gen i = 1 := by
 /-- By virtue of the quotient, terms of this form are zero -/
 theorem quot_obv : α • x' - β • y' - γ • z' = 0 := by
   dsimp only [gen]
-  simp_rw [← LinearMap.map_smul, ←LinearMap.map_sub, ← Submodule.Quotient.mk_smul _ (_ : K),
+  simp_rw [← LinearMap.map_smul, ← LinearMap.map_sub, ← Submodule.Quotient.mk_smul _ (_ : K),
     ← Submodule.Quotient.mk_sub]
   convert LinearMap.map_zero _ using 2
   rw [Submodule.Quotient.mk_eq_zero]

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -65,7 +65,7 @@ def submoduleZ : Submodule R (R × R) where
   carrier := {zz | zz.1 = zz.2}
   zero_mem' := rfl
   add_mem' := @fun _ _ ha hb => congr_arg₂ (· + ·) ha hb
-  smul_mem' a _ hb := congr_arg ((· * ·) a) hb
+  smul_mem' a _ hb := congr_arg (a * ·) hb
 #align counterexample.counterexample_not_prime_but_homogeneous_prime.submodule_z Counterexample.CounterexampleNotPrimeButHomogeneousPrime.submoduleZ
 
 /-- The grade 1 part of `R²` is `{(0, b) | b ∈ R}`. -/

Counterexamples/Monic_nonRegular.lean

@@ -56,19 +56,22 @@ instance : Mul N₃ where
   | _, 0 => 0
   | _, _ => more
 
-instance : CommSemiring N₃ where
-  add_assoc := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
-  zero_add  := by rintro ⟨⟩ <;> rfl
-  add_zero  := by rintro ⟨⟩ <;> rfl
-  add_comm  := by rintro ⟨⟩ ⟨⟩ <;> rfl
-  left_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
-  right_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
+instance : CommMonoid N₃ where
   mul_assoc := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
-  mul_comm := by rintro ⟨⟩ ⟨⟩ <;> rfl
-  zero_mul := by rintro ⟨⟩ <;> rfl
-  mul_zero := by rintro ⟨⟩ <;> rfl
   one_mul := by rintro ⟨⟩ <;> rfl
   mul_one := by rintro ⟨⟩ <;> rfl
+  mul_comm := by rintro ⟨⟩ ⟨⟩ <;> rfl
+
+instance : CommSemiring N₃ :=
+  { (inferInstance : CommMonoid N₃) with
+    add_assoc := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
+    zero_add  := by rintro ⟨⟩ <;> rfl
+    add_zero  := by rintro ⟨⟩ <;> rfl
+    add_comm  := by rintro ⟨⟩ ⟨⟩ <;> rfl
+    left_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
+    right_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
+    zero_mul := by rintro ⟨⟩ <;> rfl
+    mul_zero := by rintro ⟨⟩ <;> rfl }
 
 theorem X_add_two_mul_X_add_two : (X + C 2 : N₃[X]) * (X + C 2) = (X + C 2) * (X + C 3) := by
   simp only [mul_add, add_mul, X_mul, add_assoc]

Counterexamples/Phillips.lean

@@ -261,7 +261,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
     In this proof, we use explicit coercions `↑s` for `s : A` as otherwise the system tries to find
     a `CoeFun` instance on `↥A`, which is too costly.
     -/
-  by_contra' h
+  by_contra! h
   -- We will formulate things in terms of the type of countable subsets of `α`, as this is more
   -- convenient to formalize the inductive construction.
   let A : Set (Set α) := {t | t.Countable}
@@ -570,9 +570,9 @@ theorem countable_ne (Hcont : #ℝ = aleph 1) (φ : (DiscreteCopy ℝ →ᵇ ℝ
     {x | φ.toBoundedAdditiveMeasure.continuousPart univ ≠ φ (f Hcont x)} ⊆
       {x | φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x ≠ ∅} := by
     intro x hx
+    simp only [mem_setOf] at *
     contrapose! hx
-    simp only [Classical.not_not, mem_setOf_eq, not_nonempty_iff_eq_empty] at hx
-    simp [apply_f_eq_continuousPart Hcont φ x hx]
+    exact apply_f_eq_continuousPart Hcont φ x hx |>.symm
   have B :
     {x | φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x ≠ ∅} ⊆
       ⋃ y ∈ φ.toBoundedAdditiveMeasure.discreteSupport, {x | y ∈ spf Hcont x} := by

Counterexamples/SorgenfreyLine.lean

@@ -179,8 +179,8 @@ theorem isClopen_Ico (a b : ℝₗ) : IsClopen (Ico a b) :=
 
 instance : TotallyDisconnectedSpace ℝₗ :=
   ⟨fun _ _ hs x hx y hy =>
-    le_antisymm (hs.subset_clopen (isClopen_Ici x) ⟨x, hx, left_mem_Ici⟩ hy)
-      (hs.subset_clopen (isClopen_Ici y) ⟨y, hy, left_mem_Ici⟩ hx)⟩
+    le_antisymm (hs.subset_isClopen (isClopen_Ici x) ⟨x, hx, left_mem_Ici⟩ hy)
+      (hs.subset_isClopen (isClopen_Ici y) ⟨y, hy, left_mem_Ici⟩ hx)⟩
 
 instance : FirstCountableTopology ℝₗ :=
   ⟨fun x => (nhds_basis_Ico_rat x).isCountablyGenerated⟩

GNUmakefile

@@ -1,3 +1,5 @@
+SHELL=/usr/bin/env -S bash -o pipefail
+
 TESTS := $(shell find test -name '*.lean')
 
 .PHONY: all build test lint
@@ -10,15 +12,7 @@ build:
 test: $(addsuffix .run, $(TESTS))
 
 test/%.run: build
-	lake env lean test/$* > test/$*.log
-	@if [ -s test/$*.log ]; then \
-		echo "Error: Test output is not empty"; \
-		cat test/$*.log; \
-		rm -f test/$*.log; \
-		exit 1; \
-	fi
-	@rm -f test/$*.log
-
+	lake env lean test/$* | scripts/check_silent.sh test/$*.log
 
 lint: build
 	env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib