feat: Time dependent Wick theorem. (#274) #332
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| on: | |
| push: | |
| branches: | |
| - master | |
| name: Build and deploy documentation | |
| # borrowed from https://github.com/teorth/pfr/blob/master/.github/workflows/push.yml | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| jobs: | |
| build_project: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install Graphviz | |
| run: sudo apt-get update && sudo apt-get install -y graphviz | |
| - name: Verify Graphviz Installation | |
| run: dot -V | |
| ################## | |
| # Remove this section if you don't want docs to be made | |
| - name: Install elan | |
| run: | | |
| set -o pipefail | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | |
| ~/.elan/bin/lean --version | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Get Mathlib cache | |
| run: lake -Kenv=dev exe cache get || true | |
| - name: Build project | |
| run: lake -Kenv=dev build HepLean | |
| - name: make TODO list | |
| run : lake exe find_TODOs mkFile | |
| - name: make list of informal proofs and lemmas | |
| run : lake exe informal mkFile mkDot mkHTML | |
| - name: make stats page | |
| run : lake exe stats mkHTML | |
| - name: make notes | |
| run : lake exe notes | |
| - name: Generate svg from dot | |
| run : dot -Tsvg -o ./docs/graph.svg ./docs/InformalDot.dot | |
| - name: Replace template file with custom | |
| run : cp ./scripts/Template.lean .lake/packages/doc-gen4/DocGen4/Output/Template.lean | |
| - name: Get doc cache | |
| uses: actions/cache@v3 | |
| with: | |
| path: | | |
| .lake/build/doc/Init | |
| .lake/build/doc/DocGen4 | |
| .lake/build/doc/Aesop | |
| .lake/build/doc/Lake | |
| .lake/build/doc/Batteries | |
| .lake/build/doc/Lean | |
| .lake/build/doc/Std | |
| .lake/build/doc/Mathlib | |
| .lake/build/doc/declarations | |
| !.lake/build/doc/declarations/declaration-data-HepLean* | |
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: | | |
| MathlibDoc- | |
| - name: Build documentation | |
| run: lake -Kenv=dev build HepLean:docs | |
| - name: Copy documentation to `docs/docs` | |
| run: | | |
| mv .lake/build/doc docs/docs | |
| #End Section | |
| ################## | |
| - name: Bundle dependencies | |
| uses: ruby/setup-ruby@v1 | |
| with: | |
| working-directory: docs | |
| ruby-version: "3.1" # Not needed with a .ruby-version file | |
| bundler-cache: true # runs 'bundle install' and caches installed gems automatically | |
| - name: Bundle website | |
| working-directory: docs | |
| run: JEKYLL_ENV=production bundle exec jekyll build | |
| - name: Upload docs & blueprint artifact | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: docs/_site | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |