Merge branch 'definition-of-Cohen-Macaulay' into CM-local-ring-is-catenary

Author: Thmoas-Guan

.github/build.in.yml

@@ -574,10 +574,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       # This action is used to determine the PR metadata in the event of a push.
-      # If it is called from a PR from a fork, it will find nothing/irrelevant data.
       - if: github.event_name != 'pull_request_target'
         id: PR_from_push
-        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
+        uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

.github/workflows/bors.yml

@@ -38,7 +38,7 @@ permissions:
 
 jobs:
   build:
-    if: github.repository == 'leanprover-community/mathlib4'
+    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
     name: Build
     runs-on: bors
     outputs:
@@ -456,7 +456,7 @@ jobs:
 
   post_steps:
     name: Post-Build Step
-    if: github.repository == 'leanprover-community/mathlib4'
+    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -558,7 +558,7 @@ jobs:
 
   style_lint:
     name: Lint style
-    if: github.repository == 'leanprover-community/mathlib4'
+    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@d29fb3b12c1c834450680b3c544f63fe0237a2e2 # 2025-06-20
@@ -569,7 +569,7 @@ jobs:
 
   build_and_lint:
     name: CI Success
-    if: github.repository == 'leanprover-community/mathlib4'
+    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
     needs: [style_lint, post_steps]
     runs-on: ubuntu-latest
     steps:
@@ -579,15 +579,14 @@ jobs:
 
   final:
     name: Post-CI job
-    if: github.repository == 'leanprover-community/mathlib4'
+    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
       # This action is used to determine the PR metadata in the event of a push.
-      # If it is called from a PR from a fork, it will find nothing/irrelevant data.
       - if: github.event_name != 'pull_request_target'
         id: PR_from_push
-        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
+        uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

.github/workflows/build.yml

@@ -591,10 +591,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       # This action is used to determine the PR metadata in the event of a push.
-      # If it is called from a PR from a fork, it will find nothing/irrelevant data.
       - if: github.event_name != 'pull_request_target'
         id: PR_from_push
-        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
+        uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

.github/workflows/build_fork.yml

@@ -588,10 +588,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       # This action is used to determine the PR metadata in the event of a push.
-      # If it is called from a PR from a fork, it will find nothing/irrelevant data.
       - if: github.event_name != 'pull_request_target'
         id: PR_from_push
-        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
+        uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

.github/workflows/mk_build_yml.sh

@@ -54,7 +54,7 @@ on:
 
 name: continuous integration (staging)
 EOF
-  include "github.sha" bors "github.repository == 'leanprover-community\/mathlib4'" "" bors
+  include "github.sha" bors "github.repository == 'leanprover-community\/mathlib4' || github.repository == 'leanprover-community\/mathlib4-nightly-testing'" "" bors
 }
 
 build_fork_yml() {

.github/workflows/nightly_merge_master.yml

@@ -46,7 +46,7 @@ jobs:
           git merge upstream/master --strategy-option ours --no-commit --allow-unrelated-histories || true
           # We aggressively run `lake update`, to avoid having to do this by hand.
           # When Batteries changes break Mathlib, this will likely show up on nightly-testing first.
-          lake update
+          lake update -v
           git add .
           # If there's nothing to do (because there are no new commits from master),
           # that's okay, hence the '|| true'.

.github/workflows/stale.yml

@@ -1,7 +1,5 @@
 name: 'Close stale issues and PRs'
 on:
-  schedule:
-    - cron: '30 1 * * *' # every day at 01:30 UTC
   workflow_dispatch:
 
 jobs:

.github/workflows/update_dependencies.yml

@@ -32,7 +32,7 @@ jobs:
       - name: Get PR and labels
         if: ${{ steps.sha.outputs.sha }}
         id: PR # all the steps below are skipped if 'ready-to-merge' is in the list of labels found here
-        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
+        uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:
@@ -56,7 +56,7 @@ jobs:
 
       - name: Update dependencies
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
-        run: lake update
+        run: lake update -v
 
       - name: Check if lean-toolchain was modified
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}

Archive.lean

@@ -3,6 +3,7 @@ import Archive.Examples.Eisenstein
 import Archive.Examples.IfNormalization.Result
 import Archive.Examples.IfNormalization.Statement
 import Archive.Examples.IfNormalization.WithoutAesop
+import Archive.Examples.Kuratowski
 import Archive.Examples.MersennePrimes
 import Archive.Examples.PropEncodable
 import Archive.Hairer
@@ -56,6 +57,7 @@ import Archive.Imo.Imo2024Q2
 import Archive.Imo.Imo2024Q3
 import Archive.Imo.Imo2024Q5
 import Archive.Imo.Imo2024Q6
+import Archive.Kuratowski
 import Archive.MiuLanguage.Basic
 import Archive.MiuLanguage.DecisionNec
 import Archive.MiuLanguage.DecisionSuf