Merge remote-tracking branch 'origin/master' into hint_tactic_parallel

Author: kim-em

.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 ..

.github/workflows/nightly_detect_failure.yml

@@ -40,8 +40,29 @@ jobs:
         toolchain=$(<lean-toolchain)
         if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
           version=${BASH_REMATCH[1]}
+          echo "NIGHTLY=$version" >> $GITHUB_ENV
           git push origin refs/heads/nightly-testing:refs/heads/nightly-testing-$version
         else
           echo "Error: The file lean-toolchain does not contain the expected pattern."
           exit 1
         fi
+
+    # Next, we'll update the `nightly-with-mathlib` branch at Lean.
+    - name: Cleanup workspace
+      run: |
+        sudo rm -rf *
+    # Checkout the Lean repository on 'nightly-with-mathlib'
+    - name: Checkout Lean repository
+      uses: actions/checkout@v3
+      with:
+        repository: leanprover/lean4
+        token: ${{ secrets.LEAN_PR_TESTING }}
+        ref: nightly-with-mathlib
+    # Merge the relevant nightly.
+    - name: Fetch tags from 'lean4-nightly', and merge relevant nightly into 'nightly-with-mathlib'
+      run: |
+        git remote add nightly https://github.com/leanprover/lean4-nightly.git
+        git fetch nightly --tags
+        # Note: old jobs may run out of order, but it is safe to merge an older `nightly-YYYY-MM-DD`.
+        git merge nightly-${NIGHTLY} --strategy-option ours --allow-unrelated-histories || true
+        git push origin

.github/workflows/nightly_merge_master.yml

@@ -3,9 +3,8 @@
 name: Merge master to nightly
 
 on:
-  push:
-    branches:
-      - master
+  schedule:
+    - cron: '30 */3 * * *'  # 8AM CET/11PM PT
 
 jobs:
   merge-to-nightly:
@@ -25,9 +24,11 @@ jobs:
       - name: Merge master to nightly favoring nightly changes
         run: |
           git checkout nightly-testing
-          # If the merge goes badly, we proceed anyway via '|| true'
+          # If the merge goes badly, we proceed anyway via '|| true'.
           # CI will report failures on the 'nightly-testing' branch direct to Zulip.
           git merge master --strategy-option ours --no-commit --allow-unrelated-histories || true
           git add .
-          git commit -m "Merge master into nightly-testing"
+          # If there's nothing to do (because there are no new commits from master),
+          # that's okay, hence the '|| true'.
+          git commit -m "Merge master into nightly-testing" || true
           git push origin nightly-testing

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