Bump mathlib

Signed-off-by: zeramorphic <[email protected]>

.github/workflows/push_main.yml

@@ -45,15 +45,6 @@ jobs:
           dot -Tpng -Gnewrank=true -Goverlaps=false -Gsplines=ortho depgraph.dot > depgraph.png
           dot -Tsvg -Gnewrank=true -Goverlaps=false -Gsplines=ortho depgraph.dot > depgraph.svg
 
-      # - name: build lean4checker
-      #   run: |
-      #     git clone https://github.com/leanprover/lean4checker
-      #     cd lean4checker
-      #     ~/.elan/bin/lake -Kenv=dev build
-
-      # - name: check environments using lean4checker
-      #   run: grep -h '^import ConNF.' ConNF/*.lean | sed 's/import //' | xargs -n 1 -P 8 ~/.elan/bin/lake -Kenv=dev env lean4checker/build/bin/lean4checker
-
       - name: build documentation
         run: ~/.elan/bin/lake -Kenv=dev build ConNF:docs
 
@@ -100,3 +91,47 @@ jobs:
 
       - name: deploy website
         uses: actions/deploy-pages@v1
+
+  style_lint:
+    name: Lint style
+    runs-on: ubuntu-latest
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v4
+
+      - name: check case sensitivity
+        uses: credfeto/[email protected]
+
+      - name: look for ignored files
+        uses: credfeto/[email protected]
+
+      - name: check for lean files with the executable bit set
+        shell: bash
+        run: |
+          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
+          if [[ -n "$executable_files" ]]
+          then
+            echo "ERROR: The following Lean files have the executable bit set."
+            echo "$executable_files"
+            exit 1
+          fi
+
+      - name: install python
+        if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: 3.8
+
+      - 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: run style linters
+        run: |
+          lake exe lint-style

.vscode/settings.json

@@ -6,6 +6,5 @@
   "files.eol": "\n",
   "files.insertFinalNewline": true,
   "files.trimFinalNewlines": true,
-  "files.trimTrailingWhitespace": true,
-  "search.usePCRE2": true
+  "files.trimTrailingWhitespace": true
 }

ConNF.lean

@@ -1 +1 @@
-def hello := "world"
+import ConNF.Basic

ConNF/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

DependencyGraph.lean

@@ -1,5 +1,7 @@
-import Mathlib.Data.ByteArray
-import Lean
+import Batteries.Tactic.PrintDependents
+import Mathlib.Data.List.Sort
+import Mathlib.Data.String.Basic
+import Mathlib.Util.AssertNoSorry
 import ConNF
 
 open Lean
@@ -58,7 +60,7 @@ elab "#deptree " : command => do
 -- source:
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Counting.20prerequisites.20of.20a.20theorem/near/425370265
 def getVisited (env : Environment) (decl : Name) :=
-  let (_, { visited, .. }) := Elab.Command.CollectAxioms.collect decl |>.run env |>.run {}
+  let (_, { visited, .. }) := CollectAxioms.collect decl |>.run env |>.run {}
   visited.erase decl
 
 partial def allDeclsIn (module : Name) : Elab.Command.CommandElabM (Array Name) := do

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b3ae244300f97308f07d01ba948d345f354a1001",
+   "rev": "9e23bfc012e95672d31d81958b4dce717a46c84d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,