Review essential tutorial content #486
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
| name: Juvix Docs CI | |
| "on": | |
| workflow_dispatch: | |
| inputs: | |
| build-type: | |
| type: choice | |
| description: "Docs build type" | |
| default: "latest" | |
| options: | |
| - "dev" | |
| - "latest" | |
| skip: | |
| description: Skipped build tasks (comma-separated) e.g., check-format-juvix-files, typecheck-juvix-files | |
| default: "" | |
| required: false | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| branches: | |
| - main | |
| types: | |
| - opened | |
| - reopened | |
| - synchronize | |
| - ready_for_review | |
| - closed | |
| concurrency: | |
| group: "${{ github.workflow }}-${{ github.head_ref || github.run_id }}" | |
| cancel-in-progress: true | |
| env: | |
| GIT_COMMITTER_NAME: juvix-docs-ci | |
| GIT_COMMITTER_EMAIL: [email protected] | |
| SKIP: ${{ github.event.inputs.skip }} | |
| GH_TOKEN: ${{ secrets.GH_TOKEN }} | |
| permissions: | |
| contents: write | |
| pull-requests: write | |
| jobs: | |
| build-and-deploy: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout our repository | |
| uses: actions/checkout@v3 | |
| with: | |
| fetch-depth: 0 | |
| - name: comment on PR (Pull Request) | |
| if: >- | |
| github.event_name == 'pull_request' | |
| run: gh $GH_FLAGS --edit-last --body "$MSG" || gh $GH_FLAGS --body "$MSG" || true | |
| env: | |
| MSG: "The build is in progress. Please wait for the preview link." | |
| GH_FLAGS: pr -R anoma/juvix-docs comment ${{ github.event.pull_request.number }} | |
| - name: Install Linux dependencies | |
| run: sudo apt-get install -y libcairo2-dev libfreetype6-dev libffi-dev libjpeg-dev libpng-dev libz-dev pngquant graphviz | |
| - name: Install the latest Juvix compiler (for latest build-type) | |
| uses: jaxxstorm/[email protected] | |
| if: github.event_name == 'workflow_dispatch' && github.event.inputs.build-type == 'latest' | |
| with: | |
| repo: anoma/juvix | |
| tag: latest | |
| chmod: 0755 | |
| - name: See the dev version in the documentation | |
| id: juvix-version | |
| run: | | |
| echo "number=$(cat VERSION)" >> "$GITHUB_OUTPUT" | |
| - name: Install the corresponding Juvix compiler | |
| uses: jaxxstorm/[email protected] | |
| if: github.event_name != 'workflow_dispatch' || github.event.inputs.build-type == 'dev' | |
| with: | |
| repo: anoma/juvix | |
| tag: v${{ steps.juvix-version.outputs.number }} | |
| - name: See the exact version of the Juvix compiler installed | |
| run: | | |
| juvix --version | |
| - uses: actions/setup-python@v4 | |
| with: | |
| python-version: "3.11.1" | |
| check-latest: true | |
| cache: "pip" | |
| - uses: pre-commit/[email protected] | |
| - name: Generate HTML files from examples | |
| run: | | |
| make html-examples | |
| - name: Install Python dependencies | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install --user -r requirements.txt | |
| - name: Build prerequisites | |
| run: | | |
| make pre-build | |
| - name: Build MkDocs (Pull Request) | |
| if: >- | |
| github.event_name == 'pull_request' | |
| run: | | |
| mkdocs build --clean --config-file mkdocs.yml --site-dir $SITE_DIR | |
| env: | |
| SITE_DIR: pull-${{ github.event.pull_request.number }} | |
| SITE_URL: https://docs.juvix.org/pull-${{ github.event.pull_request.number }} | |
| - name: comment on PR (Pull Request) | |
| if: failure() && github.event_name == 'pull_request' | |
| run: | | |
| gh pr -R anoma/juvix-docs comment ${{ github.event.pull_request.number }} --edit-last --body "The build failed. Please check the logs." || true | |
| - name: Setup Git | |
| run: | | |
| git config --global user.name "${GIT_COMMITTER_NAME}" | |
| git config --global user.email "${GIT_COMMITTER_EMAIL}" | |
| - name: Install material-insiders | |
| if: github.ref == 'refs/heads/main' | |
| run: pip install --user -r insiders.requirements.txt | |
| env: | |
| GH_TOKEN: ${{ secrets.GH_TOKEN }} | |
| - name: Test Build MkDocs Insiders (Pull Request) | |
| if: github.event_name == 'pull_request' | |
| id: test-build-mkdocs-insiders | |
| run: | | |
| mkdocs build --clean --config-file mkdocs.insiders.yml --site-dir $SITE_DIR | |
| env: | |
| SITE_DIR: pull-${{ github.event.pull_request.number }} | |
| SITE_URL: https://docs.juvix.org/pull-${{ github.event.pull_request.number }} | |
| - name: Deploy Preview comment (Pull Request) | |
| if: github.event_name == 'pull_request' && | |
| steps.test-build-mkdocs-insiders.outcome == 'success' | |
| run: | | |
| gh pr -R anoma/juvix-docs comment ${{ github.event.pull_request.number }} --edit-last --body "Basic build successful and build with MkDocs Insiders successful. We are now deploying the preview." || true | |
| - name: Deploy Preview (Pull Request) | |
| if: github.event_name == 'pull_request' && success() | |
| uses: JamesIves/github-pages-deploy-action@v4 | |
| with: | |
| branch: gh-pages | |
| folder: pull-${{ github.event.pull_request.number }} | |
| target-folder: pull-${{ github.event.pull_request.number }} | |
| token: ${{ secrets.GITHUB_TOKEN }} | |
| clean: false | |
| - name: Report PR preview link (Pull Request) | |
| if: >- | |
| github.event_name == 'pull_request' && success() | |
| run: gh pr -R anoma/juvix-docs comment ${{ github.event.pull_request.number }} --edit-last --body "$MSG" || true | |
| env: | |
| MSG: "Success! The preview of this PR will be available at https://docs.juvix.org/pull-${{ github.event.pull_request.number }}/ in a few minutes.\n\nPlease note that this link will be deleted when the PR is closed or merged." | |
| - name: Failed preview build comment (Pull Request) | |
| if: >- | |
| github.event_name == 'pull_request' && failure() | |
| run: | | |
| gh pr -R anoma/juvix-docs comment ${{ github.event.pull_request.number }} --edit-last --body "The preview of this PR failed to build. Please check the logs." || true | |
| - name: Delete the PR preview if the PR is closed or merged (Pull Request) | |
| if: github.event_name == 'pull_request' && (github.event.pull_request.merged == true || github.event.action == 'closed') | |
| run: | | |
| git checkout gh-pages | |
| if [-d "pull-${{ github.event.pull_request.number }}"]; then | |
| rm -rf "pull-${{ github.event.pull_request.number }}" | |
| git add . | |
| git commit -m "Delete preview for PR #${{ github.event.pull_request.number }}" | |
| git push | |
| fi | |
| gh pr -R anoma/juvix-docs comment ${{ github.event.pull_request.number }} --edit-last --body "The preview of this PR has been deleted." || true | |
| # ------------------------------------------------------------- | |
| - name: Run MkDocs Insiders (Main branch Workflow Dispatch) | |
| if: >- | |
| github.ref == 'refs/heads/main' && github.event_name == 'workflow_dispatch' | |
| run: | | |
| MKDOCSCONFIG=mkdocs.insiders.yml make ${{ github.event.inputs.build-type }} | |
| - name: Run MkDocs Insiders (Main branch - Push) | |
| if: >- | |
| github.ref == 'refs/heads/main' && github.event_name != 'workflow_dispatch' | |
| run: | | |
| MKDOCSCONFIG=mkdocs.insiders.yml make dev | |
| env: | |
| SITE_DIR: dev | |
| SITE_URL: https://docs.juvix.org/dev/ |