Trigger CI for leanprover/lean4#6334

leanprover-community · Dec 10, 2024 · bdc3336 · bdc3336
2 parents 062861f + ded531d
commit bdc3336
Show file tree

Hide file tree

Showing 350 changed files with 8,796 additions and 3,031 deletions.
diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -127,16 +127,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-
       - name: get cache
         id: get
         run: |

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -137,16 +137,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-
       - name: get cache
         id: get
         run: |

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -144,16 +144,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-
       - name: get cache
         id: get
         run: |

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -141,16 +141,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-
       - name: get cache
         id: get
         run: |

diff --git a/.github/workflows/lean4checker.yml b/.github/workflows/lean4checker.yml
@@ -1,19 +1,23 @@
-# https://chat.openai.com/share/26102e95-ac9c-4d03-a000-73e4f6cee8cd
 name: lean4checker Workflow
 
 on:
   schedule:
     - cron: '0 0 * * *'   # Runs at 00:00 UTC every day
   workflow_dispatch:
 
+env:
+  DEFAULT_BRANCH: master
+  TAG_PATTERN: '^nightly-testing-[0-9]{4}-[0-9]{2}-[0-9]{2}$'
+
 jobs:
   check-lean4checker:
-    runs-on: pr
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        branch_type: [master, nightly]
     steps:
-
-      - name: cleanup
+      - name: Cleanup
         run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
           # Delete all but the 5 most recent toolchains.
           # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
           # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
@@ -23,21 +27,24 @@ jobs:
               : # Do nothing on failure, but suppress errors
           fi
 
-      # The Hoskinson runners may not have jq installed, so do that now.
-      - name: 'Setup jq'
-        uses: dcarbone/[email protected]
-
-      - name: install elan
+      - name: Install elan
         run: |
           set -o pipefail
           curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: Checkout master branch
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          git fetch --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"
+
+      - name: Checkout branch or tag
         uses: actions/checkout@v4
         with:
-          ref: 'master'
+          ref: ${{ matrix.branch_type == 'master' && env.DEFAULT_BRANCH || env.LATEST_TAG }}
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -46,7 +53,7 @@ jobs:
             elan toolchain uninstall "$(cat lean-toolchain)"
           fi
 
-      - name: print lean and lake versions
+      - name: Print Lean and Lake versions
         run: |
           lean --version
           lake --version
@@ -55,16 +62,6 @@ jobs:
         run: |
           lake exe cache get
 
-      - name: prune ProofWidgets .lake
-        run: |
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-          lake build ProofWidgets
-
       - name: Check environments using lean4checker
         id: lean4checker
         run: |
@@ -100,7 +97,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ✅ lean4checker [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
+            ✅ lean4checker [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ matrix.branch_type == 'master' && 'master' || env.LATEST_TAG }})
 
       - name: Post failure message on Zulip
         if: failure()
@@ -113,7 +110,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker failure'
           content: |
-            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
+            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ matrix.branch_type == 'master' && 'master' || env.LATEST_TAG }})
         continue-on-error: true
 
       - name: Post failure message on Zulip main topic
@@ -127,5 +124,5 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
+            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ matrix.branch_type == 'master' && 'master' || env.LATEST_TAG }})
         continue-on-error: true
diff --git a/Archive/Imo/Imo1964Q1.lean b/Archive/Imo/Imo1964Q1.lean
@@ -5,25 +5,17 @@ Authors: Kevin Buzzard
 -/
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Data.Nat.ModEq
-import Mathlib.Tactic.Ring
 
 /-!
 # IMO 1964 Q1
 
 (a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$.
-
 (b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.
 
-We define a predicate for the solutions in (a), and prove that it is the set of positive
-integers which are a multiple of 3.
--/
-
-
-/-!
-## Intermediate lemmas
+For (a), we find that the order of $2$ mod $7$ is $3$. Therefore for (b), it suffices to check
+$n = 0, 1, 2$.
 -/
 
-
 open Nat
 
 namespace Imo1964Q1
@@ -33,17 +25,13 @@ theorem two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7] :=
   calc 2 ^ n = 2 ^ (3 * (n / 3) + t) := by rw [Nat.div_add_mod]
     _ = (2 ^ 3) ^ (n / 3) * 2 ^ t := by rw [pow_add, pow_mul]
     _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; decide
-    _ = 2 ^ t := by ring
-
-/-!
-## The question
--/
+    _ = 2 ^ t := by rw [one_pow, one_mul]
 
+end Imo1964Q1
 
-def ProblemPredicate (n : ℕ) : Prop :=
-  7 ∣ 2 ^ n - 1
+open Imo1964Q1
 
-theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : ProblemPredicate n ↔ 3 ∣ n := by
+theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : 7 ∣ 2 ^ n - 1 ↔ 3 ∣ n := by
   let t := n % 3
   have : t < 3 := Nat.mod_lt _ (by decide)
   calc 7 ∣ 2 ^ n - 1 ↔ 2 ^ n ≡ 1 [MOD 7] := by
@@ -53,15 +41,11 @@ theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : ProblemPredicate n ↔ 3 ∣ n := by
     _ ↔ t = 0 := by interval_cases t <;> decide
     _ ↔ 3 ∣ n := by rw [dvd_iff_mod_eq_zero]
 
-end Imo1964Q1
-
-open Imo1964Q1
-
 theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1 := by
   intro h
   let t := n % 3
   have : t < 3 := Nat.mod_lt _ (by decide)
   have H : 2 ^ t + 1 ≡ 0 [MOD 7] := calc
-    2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7 ] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
+    2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
       _ ≡ 0 [MOD 7] := h.modEq_zero_nat
   interval_cases t <;> contradiction
diff --git a/Archive/Imo/Imo2019Q4.lean b/Archive/Imo/Imo2019Q4.lean
@@ -30,7 +30,7 @@ open scoped Nat
 
 open Nat hiding zero_le Prime
 
-open Finset multiplicity
+open Finset
 
 namespace Imo2019Q4
 

diff --git a/Archive/Wiedijk100Theorems/PerfectNumbers.lean b/Archive/Wiedijk100Theorems/PerfectNumbers.lean
@@ -55,7 +55,7 @@ theorem even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).Pr
     Even (2 ^ k * mersenne (k + 1)) := by simp [ne_zero_of_prime_mersenne k pr, parity_simps]
 
 theorem eq_two_pow_mul_odd {n : ℕ} (hpos : 0 < n) : ∃ k m : ℕ, n = 2 ^ k * m ∧ ¬Even m := by
-  have h := Nat.multiplicity_finite_iff.2 ⟨Nat.prime_two.ne_one, hpos⟩
+  have h := Nat.finiteMultiplicity_iff.2 ⟨Nat.prime_two.ne_one, hpos⟩
   cases' pow_multiplicity_dvd 2 n with m hm
   use multiplicity 2 n, m
   refine ⟨hm, ?_⟩

diff --git a/Cache/Requests.lean b/Cache/Requests.lean
@@ -161,14 +161,27 @@ into the `lean-toolchain` file at the root directory of your project"
 
 /-- Fetches the ProofWidgets cloud release and prunes non-JS files. -/
 def getProofWidgets (buildDir : FilePath) : IO Unit := do
-  if (← buildDir.pathExists) then return
-  -- Unpack the ProofWidgets cloud release (for its `.js` files)
+  if (← buildDir.pathExists) then
+    -- Check if the ProofWidgets build is out-of-date via `lake`.
+    -- This is done through Lake as cache has no simple heuristic
+    -- to determine whether the ProofWidgets JS is out-of-date.
+    let exitCode ← (← IO.Process.spawn {cmd := "lake", args := #["-q", "build", "--no-build", "proofwidgets:release"]}).wait
+    if exitCode == 0 then -- up-to-date
+      return
+    else if exitCode == 3 then -- needs fetch (`--no-build` triggered)
+      pure ()
+    else
+      throw <| IO.userError s!"Failed to validate ProofWidgets cloud release: lake failed with error code {exitCode}"
+  -- Download and unpack the ProofWidgets cloud release (for its `.js` files)
   let exitCode ← (← IO.Process.spawn {cmd := "lake", args := #["-q", "build", "proofwidgets:release"]}).wait
   if exitCode != 0 then
     throw <| IO.userError s!"Failed to fetch ProofWidgets cloud release: lake failed with error code {exitCode}"
-  -- prune non-js ProofWidgets files (e.g., `olean`, `.c`)
-  IO.FS.removeDirAll (buildDir / "lib")
-  IO.FS.removeDirAll (buildDir / "ir")
+  -- Prune non-JS ProofWidgets files (e.g., `olean`, `.c`)
+  try
+    IO.FS.removeDirAll (buildDir / "lib")
+    IO.FS.removeDirAll (buildDir / "ir")
+  catch e =>
+    throw <| IO.userError s!"Failed to prune ProofWidgets cloud release: {e}"
 
 /-- Downloads missing files, and unpacks files. -/
 def getFiles (hashMap : IO.HashMap) (forceDownload forceUnpack parallel decompress : Bool) :

diff --git a/Counterexamples/Pseudoelement.lean b/Counterexamples/Pseudoelement.lean
@@ -74,26 +74,24 @@ theorem x_not_pseudo_eq : ¬PseudoEqual _ x y := by
   replace h := ModuleCat.eq_range_of_pseudoequal h
   dsimp [x, y] at h
   let φ := biprod.lift (𝟙 (of ℤ ℚ)) (2 • 𝟙 (of ℤ ℚ))
-  have mem_range := mem_range_self φ (1 : ℚ)
+  have mem_range := mem_range_self φ.hom (1 : ℚ)
   rw [h] at mem_range
   obtain ⟨a, ha⟩ := mem_range
-  erw [← ModuleCat.id_apply (φ (1 : ℚ)), ← biprod.total, ← LinearMap.comp_apply, ← comp_def,
-    Preadditive.comp_add] at ha
+  rw [← ModuleCat.id_apply _ (φ (1 : ℚ)), ← biprod.total, ← LinearMap.comp_apply,
+    ← ModuleCat.hom_comp, Preadditive.comp_add] at ha
   let π₁ := (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _)
   have ha₁ := congr_arg π₁ ha
-    -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-  erw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₁
+  rw [← ModuleCat.comp_apply, ← ModuleCat.comp_apply] at ha₁
   simp only [π₁, φ, BinaryBiproduct.bicone_fst, biprod.lift_fst, CategoryTheory.id_apply,
     biprod.lift_fst_assoc, Category.id_comp, biprod.lift_snd_assoc, Linear.smul_comp,
     Preadditive.add_comp, BinaryBicone.inl_fst, BinaryBicone.inr_fst, smul_zero, add_zero] at ha₁
   let π₂ := (biprod.snd : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _)
   have ha₂ := congr_arg π₂ ha
-    -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-  erw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₂
+  rw [← ModuleCat.comp_apply, ← ModuleCat.comp_apply] at ha₂
   simp only [π₁, π₂, φ, BinaryBiproduct.bicone_snd, biprod.lift_snd, CategoryTheory.id_apply,
     biprod.lift_fst_assoc, Category.id_comp, biprod.lift_snd_assoc, Linear.smul_comp,
     Preadditive.add_comp, BinaryBicone.inl_snd, BinaryBicone.inr_snd, zero_add, two_smul] at ha₂
-  erw [add_apply, CategoryTheory.id_apply] at ha₂
+  erw [add_apply, ModuleCat.id_apply] at ha₂
   subst ha₁
   simp only [self_eq_add_right] at ha₂
   exact one_ne_zero' ℚ ha₂
@@ -104,12 +102,12 @@ open scoped Pseudoelement
 
 /-- `biprod.fst ⟦x⟧ = biprod.fst ⟦y⟧`. -/
 theorem fst_mk'_x_eq_fst_mk'_y :
-    (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) ⟦x⟧ = (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) ⟦y⟧ :=
+    pseudoApply biprod.fst ⟦x⟧ = pseudoApply biprod.fst ⟦y⟧ :=
   Quotient.eq.2 fst_x_pseudo_eq_fst_y
 
 /-- `biprod.snd ⟦x⟧ = biprod.snd ⟦y⟧`. -/
 theorem snd_mk'_x_eq_snd_mk'_y :
-    (biprod.snd : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) ⟦x⟧ = (biprod.snd : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) ⟦y⟧ :=
+    pseudoApply biprod.snd ⟦x⟧ = pseudoApply biprod.snd ⟦y⟧ :=
   Quotient.eq.2 snd_x_pseudo_eq_snd_y
 
 -- Porting note: needs explicit type ascription `: Quotient <| Pseudoelement.setoid _`
@@ -125,8 +123,8 @@ theorem exist_ne_and_fst_eq_fst_and_snd_eq_snd :
     ∃ x y, -- Porting note: removed type ascription `: of ℤ ℚ ⊞ of ℤ ℚ`, it gave an error about
            -- `Type` not having zero morphisms. jmc: I don't understand where the error came from
       x ≠ y ∧
-        (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) x = (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) y ∧
-          (biprod.snd : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) x = (biprod.snd : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) y :=
+        pseudoApply (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) x = pseudoApply biprod.fst y ∧
+          pseudoApply biprod.snd x = pseudoApply biprod.snd y :=
   ⟨⟦x⟧, ⟦y⟧, mk'_x_ne_mk'_y, fst_mk'_x_eq_fst_mk'_y, snd_mk'_x_eq_snd_mk'_y⟩
 
 end