docs(mwe): add section on bug reports, #guard_msgs, and minimizers (#… #3775
This file contains hidden or 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
| name: deploy site | |
| on: | |
| push: | |
| branches-ignore: | |
| - 'master' | |
| - 'oldsite' | |
| schedule: | |
| - cron: '0 4 * * *' | |
| workflow_dispatch: | |
| concurrency: | |
| # label each workflow run; only the latest with each label will run | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| # if there is a run in progress with the same label, the next new run will be queued | |
| # and new runs after that will cancel pending runs | |
| cancel-in-progress: false | |
| permissions: | |
| contents: write | |
| jobs: | |
| build: | |
| name: Build HTML | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1 | |
| id: app-token | |
| with: | |
| app-id: ${{ secrets.LEANPROVER_COMMUNITY_WEBSITE_APP_ID }} | |
| private-key: ${{ secrets.LEANPROVER_COMMUNITY_WEBSITE_PRIVATE_KEY }} | |
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| - name: install Python | |
| uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0 | |
| with: | |
| # TODO: fix things so we can build with 3.12 and above | |
| python-version: 3.11 | |
| - name: install bibtool | |
| run: | | |
| sudo apt-get update --fix-missing | |
| sudo apt-get install bibtool | |
| - name: install Python dependencies | |
| run: python -m pip install --upgrade pip -r requirements.txt | |
| - name: build and deploy | |
| id: build | |
| run: | | |
| ./deploy.sh | |
| env: | |
| git_hash: ${{ github.sha }} | |
| GITHUB_TOKEN: ${{ steps.app-token.outputs.token }} | |
| DEPLOY_GITHUB_TOKEN: ${{ steps.app-token.outputs.token }} | |
| DEPLOY_GITHUB_USER: leanprover-community-bot | |
| github_repo: ${{ github.repository }} | |
| github_ref: ${{ github.ref }} | |
| ZULIP_KEY: ${{ secrets.ZULIP_KEY }} | |
| - name: Upload artifact | |
| id: upload-artifact | |
| if: ${{ !cancelled() && (steps.build.outcome == 'success') }} | |
| uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0 | |
| with: | |
| name: site | |
| path: build/ |