From 74a7e40ba0843dd0abc1f66617d377e800dd459b Mon Sep 17 00:00:00 2001 From: Niklas Halonen Date: Thu, 18 Jul 2024 16:53:02 +0300 Subject: [PATCH] cherry-pick CI changes from pitmonticone:bump Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> --- .github/workflows/blueprint.yml | 3 +- .github/workflows/push.yml | 123 ++++++++++++++++++++++++++++++++ .github/workflows/push_pr.yml | 57 +++++++++++++++ .gitignore | 28 +++++++- .vscode/settings.json | 5 ++ blueprint/src/occupation.tex | 8 +-- blueprint/src/overview.tex | 7 +- blueprint/src/random_walk.tex | 6 +- lake-manifest.json | 41 ++++++++--- lakefile.lean | 2 +- lean-toolchain | 2 +- 11 files changed, 256 insertions(+), 26 deletions(-) create mode 100644 .github/workflows/push.yml create mode 100644 .github/workflows/push_pr.yml create mode 100644 .vscode/settings.json diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 30416b9..2432704 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -86,4 +86,5 @@ jobs: - name: Make sure the cache works run: | - mv docs/docs .lake/build/doc \ No newline at end of file + mv docs/docs .lake/build/doc + diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml new file mode 100644 index 0000000..87b1928 --- /dev/null +++ b/.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 \ No newline at end of file diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml new file mode 100644 index 0000000..bd542d7 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index 714f016..7dc25df 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,25 @@ -/.lake -/.devenv -/.stfolder \ No newline at end of file +.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 \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..7b30b85 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,5 @@ +{ + "editor.rulers": [ + 100 + ] +} \ No newline at end of file diff --git a/blueprint/src/occupation.tex b/blueprint/src/occupation.tex index 53bdff0..9bd6366 100644 --- a/blueprint/src/occupation.tex +++ b/blueprint/src/occupation.tex @@ -54,9 +54,9 @@ \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]$.) @@ -64,7 +64,7 @@ \subsection*{Regularized occupation of a walk} \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} \ No newline at end of file diff --git a/blueprint/src/overview.tex b/blueprint/src/overview.tex index 242702a..90789d1 100644 --- a/blueprint/src/overview.tex +++ b/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} \ No newline at end of file diff --git a/blueprint/src/random_walk.tex b/blueprint/src/random_walk.tex index 186a777..8c91adf 100644 --- a/blueprint/src/random_walk.tex +++ b/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} \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index 11ddf5c..9eee31b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,10 +1,11 @@ -{"version": "1.0.0", +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "15d42e1a92a80d0db5ca1c12123866ba392b9d76", + "scope": "leanprover-community", + "rev": "937cd3219c0beffa7b623d2905707d1304da259e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,6 +14,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, + "scope": "leanprover-community", "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", @@ -22,7 +24,8 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c", + "scope": "leanprover-community", + "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,25 +34,28 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", + "scope": "leanprover-community", + "rev": "d1b33202c3a29a079f292de65ea438648123b635", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.36", + "inputRev": "v0.0.39", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, + "scope": "", "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474", + "scope": "leanprover-community", + "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +64,8 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "e956397c2b1ce52e263934adccea1098c6194840", + "scope": "", + "rev": "8b6570600657f5445210afa0edb4103a0750721b", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -67,6 +74,7 @@ {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, + "scope": "", "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5", "name": "checkdecls", "manifestFile": "lake-manifest.json", @@ -76,6 +84,7 @@ {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, + "scope": "", "rev": "9148a0a7506099963925cf239c491fcda5ed0044", "name": "MD4Lean", "manifestFile": "lake-manifest.json", @@ -85,16 +94,28 @@ {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "rev": "c74a052aebee847780e165611099854de050adf7", + "scope": "", + "rev": "f93115d0209de6db335725dee900d379f40c0317", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "c369436d21c583a60da62d4513c7b9ea08389074", + "scope": "", + "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index cba3e40..dfa1521 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -19,4 +19,4 @@ require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" meta if get_config? env = some "dev" then require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "main" \ No newline at end of file + "https://github.com/leanprover/doc-gen4" @ "main" diff --git a/lean-toolchain b/lean-toolchain index 29c0cea..6a4259f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0-rc2 +leanprover/lean4:v4.10.0-rc2