cherry-pick CI changes from pitmonticone:bump

Co-authored-by: Pietro Monticone <[email protected]>

.github/workflows/blueprint.yml

@@ -86,4 +86,5 @@ jobs:
 
       - name: Make sure the cache works
         run: |
-          mv docs/docs .lake/build/doc
+          mv docs/docs .lake/build/doc
+

.github/workflows/push.yml

@@ -0,0 +1,123 @@
+on:
+  push:
+    branches:
+      - main
+      - bump
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  # style_lint:
+  #   name: Lint style
+  #   runs-on: ubuntu-latest
+  #   steps:
+  #     # Check for long lines in .lean files and report if any lines exceed 100 characters
+  #     - name: Check for long lines
+  #       if: always()
+  #       run: |
+  #         ! (find Polya -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
+
+  #     - name: Don't 'import Mathlib', use precise imports
+  #       if: always()
+  #       run: |
+  #         ! (find Polya -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
+
+  build_project:
+    runs-on: ubuntu-latest
+    name: Build project
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+
+      - name: Install elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+      # - name: Update doc-gen4
+      #   run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
+
+      - name: Get cache
+        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake -Kenv=dev build Polya
+
+      - name: Cache mathlib documentation
+        uses: actions/cache@v3
+        with:
+          path: |
+            .lake/build/doc/Init
+            .lake/build/doc/Lake
+            .lake/build/doc/Lean
+            .lake/build/doc/Std
+            .lake/build/doc/Mathlib
+            .lake/build/doc/declarations
+            !.lake/build/doc/declarations/declaration-data-Polya*
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          #restore-keys: MathlibDoc-
+
+      - name: Build project documentation
+        run: ~/.elan/bin/lake -Kenv=dev build Polya:docs
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        uses: xu-cheng/texlive-action@v2
+        with:
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+          run: |
+            export PIP_BREAK_SYSTEM_PACKAGES=1
+            apk update
+            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
+            git config --global --add safe.directory $GITHUB_WORKSPACE
+            git config --global --add safe.directory `pwd`
+            python3 -m venv env
+            source env/bin/activate
+            pip install --upgrade pip requests wheel
+            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install leanblueprint
+            leanblueprint pdf
+            mkdir docs
+            cp blueprint/print/print.pdf docs/blueprint.pdf
+            leanblueprint web
+            cp -r blueprint/web docs/blueprint
+
+      - name: Check declarations
+        run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+
+      - name: Remove lake files from documentation
+        run: |
+          find .lake/build/doc -name "*.trace" -delete
+          find .lake/build/doc -name "*.hash" -delete
+          find .lake/build/doc -name "*/header-data.bmp" -delete
+
+      - name: Copy documentation to `docs/docs`
+        run: |
+          sudo chown -R runner docs
+          cp -r .lake/build/doc docs/docs
+
+      # - name: Bundle dependencies
+      #   uses: ruby/setup-ruby@v1
+      #   with:
+      #     working-directory: docs
+      #     ruby-version: "3.0"
+      #     bundler-cache: true
+
+      # - name: Bundle website
+      #   working-directory: docs
+      #   run: JEKYLL_ENV=production bundle exec jekyll build
+
+      - name: Upload docs & blueprint artifact to `docs`
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: docs/
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1
+
+      - name: Make sure the cache works
+        run: mv docs/docs .lake/build/doc

.github/workflows/push_pr.yml

@@ -0,0 +1,57 @@
+on:
+  pull_request:
+
+jobs:
+  # style_lint:
+  #   name: Lint style
+  #   runs-on: ubuntu-latest
+  #   steps:
+  #     # Check for long lines in .lean files and report if any lines exceed 100 characters
+  #     - name: Check for long lines
+  #       if: always()
+  #       run: |
+  #         ! (find Polya -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
+
+  #     - name: Don't 'import Mathlib', use precise imports
+  #       if: always()
+  #       run: |
+  #         ! (find Polya -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
+
+  build_project:
+    runs-on: ubuntu-latest
+    name: Build project
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+
+      - name: Install elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+      - name: Get cache
+        run: ~/.elan/bin/lake exe cache get
+
+      - name: Build project
+        run: ~/.elan/bin/lake build Polya
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        uses: xu-cheng/texlive-action@v2
+        with:
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+          run: |
+            export PIP_BREAK_SYSTEM_PACKAGES=1
+            apk update
+            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
+            git config --global --add safe.directory $GITHUB_WORKSPACE
+            git config --global --add safe.directory `pwd`
+            python3 -m venv env
+            source env/bin/activate
+            pip install --upgrade pip requests wheel
+            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install leanblueprint
+            leanblueprint pdf
+            leanblueprint web
+
+      - name: Check declarations
+        run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls

.gitignore

@@ -1,3 +1,25 @@
-/.lake
-/.devenv
-/.stfolder
+.cache/*
+.lake/*
+.devenv/*
+.stfolder/*
+/build
+/lakefile.olean
+/lake-packages/*
+.DS_Store
+# Lean blueprint
+/blueprint/lean_decls
+blueprint/print/print.log
+blueprint/web/
+blueprint/src/web.paux
+blueprint/src/web.bbl
+blueprint/print/
+# Files generated by LaTeX
+*.aux
+*.bbl
+*.blg
+*.log
+*.out
+*.pdf
+*.fls
+*.fdb_latexmk
+*.synctex.gz

.vscode/settings.json

@@ -0,0 +1,5 @@
+{
+    "editor.rulers": [
+        100
+    ]
+}

blueprint/src/occupation.tex

@@ -54,17 +54,17 @@ \subsection*{Regularized occupation of a walk}
   \uses{def:walkRegOccup}
   \lean{tsum_walkRegularizedOccupation_eq_geom_series}
   The sum over all points $x \in \bZ^d$ of the $r$-regularized
-  occupations $L^\walk_r(x)$ of a walk $\walk \colon \bN \to \bZ^d$ is
+  occupations $L^{\walk}_r(x)$ of a walk $\walk \colon \bN \to \bZ^d$ is
   \begin{align*}
-  \sum_{x \in \bZ^d} L^\walk_r(x) = \sum_{t \in \bN} r^t .
+  \sum_{x \in \bZ^d} L^{\walk}_r(x) = \sum_{t \in \bN} r^t .
   \end{align*}
   (Both sides above are infinite if $r \ge 1$, but the equality
   nevertheless holds in $[0,+\infty]$.)
 \end{lemma}
 \begin{proof}
 Unravel the definitions and interchange the two summations by Fubini's theorem:
 \begin{align*}
-\sum_{x \in \bZ^d} L^\walk_r(x)
+\sum_{x \in \bZ^d} L^{\walk}_r(x)
 = & \; \sum_{x \in \bZ^d} \sum_{t \in \bN} r^t \, \indOf{\set{\walk(t) = x}} \\
 = & \; \sum_{t \in \bN} \underbrace{\sum_{x \in \bZ^d} r^t \, \indOf{\set{\walk(t) = x}}}_{=r^t}.
 \end{align*}
@@ -286,4 +286,4 @@ \section{Expected occupation from the Green's function}
 $\Greg{r_n}(\vec{0}) \nearrow \Greg{1}(\vec{0})$ as $n \to \infty$.
 Lemma \ref{lem:regularized_occupation_left_cont}
 shows exactly that.
-\end{proof}
+\end{proof}

blueprint/src/overview.tex

@@ -31,7 +31,7 @@ \chapter{P\'olya's theorem}
 for the simple random walk.
 \end{proof}
 
-The essence of the proof is to establishe the following slightly modified
+The essence of the proof is to establish the following slightly modified
 version of the theorem.
 
 \begin{theorem}[P\'olya's theorem, alternative form]
@@ -45,6 +45,7 @@ \chapter{P\'olya's theorem}
 %   on the $d$-dimensional grid $\bZ^d$.
 \end{theorem}
 \begin{proof}
-\uses{lem:recurrence_iff_finite_limit_integral, lem:SRW_Green_Fourier, lem:integral_near, lem:integral_away, cor:recurrence_iff_finite_limit_integral}
+\uses{lem:SRW_Green_Fourier, lem:integral_near, lem:integral_away, 
+      cor:recurrence_iff_finite_limit_integral}
 \ldots
-\end{proof}
+\end{proof}

blueprint/src/random_walk.tex

@@ -2,7 +2,7 @@ \chapter{Random walks}
 
 
 
-\section{Random walks on the $d$-dimensional integer grid}
+\section{Random walks on the \texorpdfstring{$d$}{d}-dimensional integer grid}
 
 \begin{definition}
   \label{def:grid}
@@ -17,7 +17,7 @@ \section{Random walks on the $d$-dimensional integer grid}
 
 \begin{definition}
   \label{def:walk}
-  \lean{deftest}
+  %\lean{deftest}
   \uses{def:grid}
   \leanok
   A sequence $(u_s)_{s \in \bN}$ of steps in $\bZ^d$
@@ -79,4 +79,4 @@ \section{Random walks on the $d$-dimensional integer grid}
         0             & \text{ otherwise.}
     \end{cases}
   \end{align*}
-\end{definition}
+\end{definition}