Trigger CI for leanprover/lean4#2643

.docker/gitpod/Dockerfile

@@ -6,7 +6,7 @@ FROM ubuntu:jammy
 
 USER root
 
-RUN apt-get update && apt-get install sudo git curl git bash-completion python3 -y && apt-get clean
+RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-requests -y && apt-get clean
 
 RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
     # passwordless sudo for users in the 'sudo' group

.github/workflows/bors.yml

@@ -98,6 +98,25 @@ jobs:
       - name: check that all files are imported
         run: git diff --exit-code
 
+  check_workflows:
+    if: github.repository == 'leanprover-community/mathlib4'
+    name: check workflows
+    runs-on: ubuntu-latest
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v3
+
+      - name: update workflows
+        run: |
+          cd .github/workflows/
+          ./mk_build_yml.sh
+
+      - name: check that workflows were consistent
+        run: git diff --exit-code
+
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build
@@ -137,6 +156,11 @@ jobs:
             elan toolchain uninstall `cat lean-toolchain`
           fi
 
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
       - name: get cache
         run: |
           lake exe cache clean
@@ -232,7 +256,11 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          lake build
+          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
+          # we just keep rebuilding until it works!
+          # I'll try to come up with something better.
+          until lake build > /dev/null 2>&1; do :; done
+          ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker
 

.github/workflows/build.yml

@@ -104,6 +104,25 @@ jobs:
       - name: check that all files are imported
         run: git diff --exit-code
 
+  check_workflows:
+    if: github.repository == 'leanprover-community/mathlib4'
+    name: check workflows
+    runs-on: ubuntu-latest
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v3
+
+      - name: update workflows
+        run: |
+          cd .github/workflows/
+          ./mk_build_yml.sh
+
+      - name: check that workflows were consistent
+        run: git diff --exit-code
+
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build
@@ -143,6 +162,11 @@ jobs:
             elan toolchain uninstall `cat lean-toolchain`
           fi
 
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
       - name: get cache
         run: |
           lake exe cache clean
@@ -238,7 +262,11 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          lake build
+          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
+          # we just keep rebuilding until it works!
+          # I'll try to come up with something better.
+          until lake build > /dev/null 2>&1; do :; done
+          ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker
 

.github/workflows/build.yml.in

@@ -84,6 +84,25 @@ jobs:
       - name: check that all files are imported
         run: git diff --exit-code
 
+  check_workflows:
+    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
+    name: check workflowsJOB_NAME
+    runs-on: ubuntu-latest
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v3
+
+      - name: update workflows
+        run: |
+          cd .github/workflows/
+          ./mk_build_yml.sh
+
+      - name: check that workflows were consistent
+        run: git diff --exit-code
+
   build:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: BuildJOB_NAME
@@ -123,6 +142,11 @@ jobs:
             elan toolchain uninstall `cat lean-toolchain`
           fi
 
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
       - name: get cache
         run: |
           lake exe cache clean
@@ -218,7 +242,11 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          lake build
+          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
+          # we just keep rebuilding until it works!
+          # I'll try to come up with something better.
+          until lake build > /dev/null 2>&1; do :; done
+          ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker
 

.github/workflows/build_fork.yml

@@ -102,6 +102,25 @@ jobs:
       - name: check that all files are imported
         run: git diff --exit-code
 
+  check_workflows:
+    if: github.repository != 'leanprover-community/mathlib4'
+    name: check workflows (fork)
+    runs-on: ubuntu-latest
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v3
+
+      - name: update workflows
+        run: |
+          cd .github/workflows/
+          ./mk_build_yml.sh
+
+      - name: check that workflows were consistent
+        run: git diff --exit-code
+
   build:
     if: github.repository != 'leanprover-community/mathlib4'
     name: Build (fork)
@@ -141,6 +160,11 @@ jobs:
             elan toolchain uninstall `cat lean-toolchain`
           fi
 
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
       - name: get cache
         run: |
           lake exe cache clean
@@ -236,7 +260,11 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          lake build
+          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
+          # we just keep rebuilding until it works!
+          # I'll try to come up with something better.
+          until lake build > /dev/null 2>&1; do :; done
+          ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker
 

Archive/Examples/PropEncodable.lean

@@ -30,7 +30,7 @@ show encodability.
 namespace PropEncodable
 
 /-- Propositional formulas with labels from `α`. -/
-inductive PropForm (α : Type _)
+inductive PropForm (α : Type*)
   | var : α → PropForm α
   | not : PropForm α → PropForm α
   | and : PropForm α → PropForm α → PropForm α
@@ -49,7 +49,7 @@ The next three functions make it easier to construct functions from a small
 
 namespace PropForm
 
-private def Constructors (α : Type _) :=
+private def Constructors (α : Type*) :=
   α ⊕ (Unit ⊕ (Unit ⊕ Unit))
 
 local notation "cvar " a => Sum.inl a
@@ -61,13 +61,13 @@ local notation "cand" => Sum.inr (Sum.inr (Sum.inr Unit.unit))
 local notation "cor" => Sum.inr (Sum.inr (Sum.inl Unit.unit))
 
 @[simp]
-private def arity (α : Type _) : Constructors α → Nat
+private def arity (α : Type*) : Constructors α → Nat
   | cvar _ => 0
   | cnot => 1
   | cand => 2
   | cor => 2
 
-variable {α : Type _}
+variable {α : Type*}
 
 instance : ∀ c : Unit ⊕ (Unit ⊕ Unit), NeZero (arity α (.inr c))
   | .inl () => ⟨one_ne_zero⟩

Archive/Imo/Imo1962Q4.lean

@@ -106,7 +106,7 @@ We now present a second solution.  The key to this solution is that, when the id
 converted to an identity which is polynomial in `a` := `cos x`, it can be rewritten as a product of
 terms, `a ^ 2 * (2 * a ^ 2 - 1) * (4 * a ^ 2 - 3)`, being equal to zero.
 -/
-theorem formula {R : Type _} [CommRing R] [IsDomain R] [CharZero R] (a : R) :
+theorem formula {R : Type*} [CommRing R] [IsDomain R] [CharZero R] (a : R) :
     a ^ 2 + ((2 : R) * a ^ 2 - (1 : R)) ^ 2 + ((4 : R) * a ^ 3 - 3 * a) ^ 2 = 1 ↔
       ((2 : R) * a ^ 2 - (1 : R)) * ((4 : R) * a ^ 3 - 3 * a) = 0 := by
   constructor <;> intro h

Archive/Imo/Imo1987Q1.lean

@@ -25,7 +25,7 @@ holds true for `n = 0` as well, so we first prove it, then deduce the original v
 `n ≥ 1`. -/
 
 
-variable (α : Type _) [Fintype α] [DecidableEq α]
+variable (α : Type*) [Fintype α] [DecidableEq α]
 
 open scoped BigOperators Nat
 
@@ -54,7 +54,7 @@ theorem card_fixed_points :
     Finset.filter_eq', Finset.card_univ]
 #align imo1987_q1.card_fixed_points Imo1987Q1.card_fixed_points
 
-/-- Given `α : Type _` and `k : ℕ`, `fiber α k` is the set of permutations of `α` with exactly `k`
+/-- Given `α : Type*` and `k : ℕ`, `fiber α k` is the set of permutations of `α` with exactly `k`
 fixed points. -/
 def fiber (k : ℕ) : Set (Perm α) :=
   {σ : Perm α | card (fixedPoints σ) = k}
@@ -91,7 +91,7 @@ def fixedPointsEquiv' :
   right_inv := fun ⟨⟨x, σ⟩, h⟩ => rfl
 #align imo1987_q1.fixed_points_equiv' Imo1987Q1.fixedPointsEquiv'
 
-/-- Main statement for any `(α : Type _) [Fintype α]`. -/
+/-- Main statement for any `(α : Type*) [Fintype α]`. -/
 theorem main_fintype : ∑ k in range (card α + 1), k * p α k = card α * (card α - 1)! := by
   have A : ∀ (k) (σ : fiber α k), card (fixedPoints (↑σ : Perm α)) = k := fun k σ => σ.2
   simpa [A, ← Fin.sum_univ_eq_sum_range, -card_ofFinset, Finset.card_univ, card_fixed_points,

Archive/Imo/Imo1998Q2.lean

@@ -45,19 +45,19 @@ set_option linter.uppercaseLean3 false
 
 open scoped Classical
 
-variable {C J : Type _} (r : C → J → Prop)
+variable {C J : Type*} (r : C → J → Prop)
 
 namespace Imo1998Q2
 
 noncomputable section
 
 /-- An ordered pair of judges. -/
-abbrev JudgePair (J : Type _) :=
+abbrev JudgePair (J : Type*) :=
   J × J
 #align imo1998_q2.judge_pair Imo1998Q2.JudgePair
 
 /-- A triple consisting of contestant together with an ordered pair of judges. -/
-abbrev AgreedTriple (C J : Type _) :=
+abbrev AgreedTriple (C J : Type*) :=
   C × JudgePair J
 #align imo1998_q2.agreed_triple Imo1998Q2.AgreedTriple
 
@@ -168,7 +168,7 @@ theorem A_card_upper_bound {k : ℕ}
 
 end
 
-theorem add_sq_add_sq_sub {α : Type _} [Ring α] (x y : α) :
+theorem add_sq_add_sq_sub {α : Type*} [Ring α] (x y : α) :
     (x + y) * (x + y) + (x - y) * (x - y) = 2 * x * x + 2 * y * y := by noncomm_ring
 #align imo1998_q2.add_sq_add_sq_sub Imo1998Q2.add_sq_add_sq_sub
 

Archive/Imo/Imo2019Q2.lean

@@ -67,7 +67,7 @@ set_option linter.uppercaseLean3 false
 
 attribute [local instance] FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two
 
-variable (V : Type _) (Pt : Type _)
+variable (V : Type*) (Pt : Type*)
 
 variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
 

Archive/OxfordInvariants/Summer2021/Week3P1.lean

@@ -71,7 +71,7 @@ natural.
 
 open scoped BigOperators
 
-variable {α : Type _} [LinearOrderedField α]
+variable {α : Type*} [LinearOrderedField α]
 
 theorem OxfordInvariants.Week3P1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤ n, 0 < a i)
     (ha : ∀ i, i + 2 ≤ n → a (i + 1) ∣ a i + a (i + 2)) :

Archive/Sensitivity.lean

@@ -216,6 +216,7 @@ theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by
   · rw [show p = q from Subsingleton.elim (α := Q 0) p q]
     dsimp [ε, e]
     simp
+    rfl
   · dsimp [ε, e]
     cases hp : p 0 <;> cases hq : q 0
     all_goals

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -39,7 +39,7 @@ open scoped Polynomial
 
 attribute [local instance] splits_ℚ_ℂ
 
-variable (R : Type _) [CommRing R] (a b : ℕ)
+variable (R : Type*) [CommRing R] (a b : ℕ)
 
 /-- A quintic polynomial that we will show is irreducible -/
 noncomputable def Φ : R[X] :=
@@ -49,7 +49,7 @@ noncomputable def Φ : R[X] :=
 variable {R}
 
 @[simp]
-theorem map_Phi {S : Type _} [CommRing S] (f : R →+* S) : (Φ R a b).map f = Φ S a b := by simp [Φ]
+theorem map_Phi {S : Type*} [CommRing S] (f : R →+* S) : (Φ R a b).map f = Φ S a b := by simp [Φ]
 #align abel_ruffini.map_Phi AbelRuffini.map_Phi
 
 @[simp]

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -24,7 +24,7 @@ sequences, increasing, decreasing, Ramsey, Erdos-Szekeres, Erdős–Szekeres, Er
 -/
 
 
-variable {α : Type _} [LinearOrder α] {β : Type _}
+variable {α : Type*} [LinearOrder α] {β : Type*}
 
 open Function Finset
 

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -252,7 +252,7 @@ theorem first_vote_pos :
     · simp
 #align ballot.first_vote_pos Ballot.first_vote_pos
 
-theorem headI_mem_of_nonempty {α : Type _} [Inhabited α] : ∀ {l : List α} (_ : l ≠ []), l.headI ∈ l
+theorem headI_mem_of_nonempty {α : Type*} [Inhabited α] : ∀ {l : List α} (_ : l ≠ []), l.headI ∈ l
   | [], h => (h rfl).elim
   | x::l, _ => List.mem_cons_self x l
 #align ballot.head_mem_of_nonempty Ballot.headI_mem_of_nonempty

Archive/Wiedijk100Theorems/HeronsFormula.lean

@@ -31,7 +31,7 @@ namespace Theorems100
 
 local notation "√" => Real.sqrt
 
-variable {V : Type _} {P : Type _} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
+variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
   [NormedAddTorsor V P]
 
 /-- **Heron's formula**: The area of a triangle with side lengths `a`, `b`, and `c` is