diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 00000000..4787abc3 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,12 @@ +version: 2 +updates: + - package-ecosystem: github-actions + directory: / + schedule: + interval: weekly + groups: + actions: + patterns: + - '*' + commit-message: + prefix: 'chore' diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5090737a..ce138495 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,5 +1,3 @@ -# This is a basic workflow to help you get started with Actions - name: CI # Controls when the workflow will run @@ -12,137 +10,116 @@ on: tags: - '*' pull_request: - branches: [ master ] + branches: [master] # Allows you to run this workflow manually from the Actions tab workflow_dispatch: +# This workflow builds pull request code, including code from forks, so it holds +# no secrets and only reads. The book HTML leaves here as an artifact, and +# deploy.yml picks it up and publishes it. +permissions: + contents: read + jobs: - Build: + build: + name: Build book runs-on: ubuntu-latest steps: - - - name: Install a C compiler - run: sudo apt-get install -y build-essential - - - name: Checkout - uses: actions/checkout@v2 - - - name: Setup Python - uses: actions/setup-python@v3 - with: - python-version: 3.10.4 - - - name: Setup elan toolchain on this build - run: | - curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh - chmod u+x elan-init.sh - ./elan-init.sh -y --default-toolchain none - - - name: Set elan paths - run: | - echo "$HOME/.elan/bin" >> $GITHUB_PATH - - - name: Install lean toolchain for examples - run: | - cd examples - lean --version - - - name: Install lean toolchain for text - run: | - cd book - lean --version - - - name: Cache examples/.lake - uses: actions/cache@v4 - with: - path: examples/.lake - # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. - key: ${{ runner.os }}-${{ hashFiles('examples/lake-manifest.json') }}-${{ hashFiles('examples/lean-toolchain') }}-${{ steps.shortSHA.outputs.short_sha }} - # Try to restore cache for same OS/Lean/deps, but don't get less specific, because Lake isn't always happy to get build product version mismatches - restore-keys: | - ${{ runner.os }}-${{ hashFiles('examples/lake-manifest.json') }}-${{ hashFiles('examples/lean-toolchain') }}- - - - name: Cache book/.lake - uses: actions/cache@v4 - with: - path: book/.lake - # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. - key: ${{ runner.os }}-${{ hashFiles('book/lake-manifest.json') }}-${{ hashFiles('book/lean-toolchain') }}-${{ steps.shortSHA.outputs.short_sha }} - # Try to restore cache for same OS/Lean/deps, but don't get less specific, because Lake isn't always happy to get build product version mismatches - restore-keys: | - ${{ runner.os }}-${{ hashFiles('book/lake-manifest.json') }}-${{ hashFiles('book/lean-toolchain') }}- - - - name: Build example code - run: | - pushd examples - lake build - lake build subverso-extract-mod - popd - - - name: Save examples/.lake - uses: actions/cache/save@v4 - with: - path: examples/.lake - # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. - key: ${{ runner.os }}-${{ hashFiles('examples/lake-manifest.json') }}-${{ hashFiles('examples/lean-toolchain') }}-${{ steps.shortSHA.outputs.short_sha }} - - - name: Build book - run: | - pushd book - lake exe fp-lean --depth 2 --without-html-single --verbose - popd - - - name: Save book/.lake - uses: actions/cache/save@v4 - with: - path: book/.lake - # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. - key: ${{ runner.os }}-${{ hashFiles('book/lake-manifest.json') }}-${{ hashFiles('book/lean-toolchain') }}-${{ steps.shortSHA.outputs.short_sha }} - - # This is to get the cached highlight JSON files - - name: Save examples/.lake again - uses: actions/cache/save@v4 - with: - path: examples/.lake - # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. - key: ${{ runner.os }}-${{ hashFiles('examples/lake-manifest.json') }}-${{ hashFiles('examples/lean-toolchain') }}-${{ steps.shortSHA.outputs.short_sha }} - - - - name: Zip html contents - run: | - pushd book/_out - cp -r html-multi html - zip -rq html.zip html/ - popd - - - id: deploy-info - name: Compute Deployment Metadata - run: | - set -e - python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT" - echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT" - - - name: Release preview zip if a new tag is pushed - uses: softprops/action-gh-release@v1 - if: ${{ startsWith(github.ref, 'refs/tags/pre-') }} - with: - files: book/_out/html.zip - token: ${{ secrets.GITHUB_TOKEN }} - - - name: Deploy to Netlify hosting - uses: nwtgck/actions-netlify@v2.0 - with: - publish-dir: book/_out/html-multi/ - production-branch: master - github-token: ${{ secrets.GITHUB_TOKEN }} - deploy-message: | - ${{ github.event_name == 'pull_request' && format('pr#{0}: {1}', github.event.number, github.event.pull_request.title) || format('ref/{0}: {1}', github.ref_name, steps.deploy-info.outputs.message) }} - alias: ${{ steps.deploy-info.outputs.alias }} - enable-commit-comment: false - enable-pull-request-comment: false - github-deployment-environment: "lean-lang.org/functional_programming_lean" - fails-without-credentials: true - env: - NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }} - NETLIFY_SITE_ID: "4e471a74-81e0-42f2-b27c-ca8c80a34f7c" + - name: Install a C compiler + run: sudo apt-get install -y build-essential + + - name: Checkout + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + # The book runs a Python interpreter during the build and shows its + # output, so the version is pinned to keep that output stable. + - name: Setup Python + uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0 + with: + python-version: 3.10.4 + + - name: Setup elan toolchain on this build + run: | + curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh + chmod u+x elan-init.sh + ./elan-init.sh -y --default-toolchain none + + - name: Set elan paths + run: | + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + + - name: Install lean toolchain for examples + run: | + cd examples + lean --version + + - name: Install lean toolchain for text + run: | + cd book + lean --version + + - name: Cache examples/.lake + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: examples/.lake + # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. + key: ${{ runner.os }}-${{ hashFiles('examples/lake-manifest.json') }}-${{ hashFiles('examples/lean-toolchain') }}-${{ github.sha }} + # Try to restore cache for same OS/Lean/deps, but don't get less specific, because Lake isn't always happy to get build product version mismatches + restore-keys: | + ${{ runner.os }}-${{ hashFiles('examples/lake-manifest.json') }}-${{ hashFiles('examples/lean-toolchain') }}- + + - name: Cache book/.lake + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: book/.lake + # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. + key: ${{ runner.os }}-${{ hashFiles('book/lake-manifest.json') }}-${{ hashFiles('book/lean-toolchain') }}-${{ github.sha }} + # Try to restore cache for same OS/Lean/deps, but don't get less specific, because Lake isn't always happy to get build product version mismatches + restore-keys: | + ${{ runner.os }}-${{ hashFiles('book/lake-manifest.json') }}-${{ hashFiles('book/lean-toolchain') }}- + + - name: Build example code + run: | + pushd examples + lake build + lake build subverso-extract-mod + popd + + - name: Save examples/.lake + uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: examples/.lake + # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. + key: ${{ runner.os }}-${{ hashFiles('examples/lake-manifest.json') }}-${{ hashFiles('examples/lean-toolchain') }}-${{ github.sha }} + + - name: Build book + run: | + pushd book + lake exe fp-lean --depth 2 --without-html-single --verbose + popd + + - name: Save book/.lake + uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: book/.lake + # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. + key: ${{ runner.os }}-${{ hashFiles('book/lake-manifest.json') }}-${{ hashFiles('book/lean-toolchain') }}-${{ github.sha }} + + # This is to get the cached highlight JSON files + - name: Save examples/.lake again + uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: examples/.lake + # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. + key: ${{ runner.os }}-${{ hashFiles('examples/lake-manifest.json') }}-${{ hashFiles('examples/lean-toolchain') }}-${{ github.sha }} + + - name: Upload book HTML + uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + with: + name: book-html + path: book/_out/html-multi + retention-days: 7 + if-no-files-found: error diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml new file mode 100644 index 00000000..7c62e64a --- /dev/null +++ b/.github/workflows/deploy.yml @@ -0,0 +1,163 @@ +name: Deploy + +# Publishes the HTML that CI built. This workflow runs in the base repository, +# where the Netlify credentials live, and takes the build artifact as its only +# input. +on: + workflow_run: + workflows: [CI] + types: [completed] + +permissions: {} + +jobs: + deploy: + name: Deploy to Netlify + if: github.event.workflow_run.conclusion == 'success' + runs-on: ubuntu-latest + # Publications serialize against each other, previews against their own ref. + concurrency: + group: >- + deploy-${{ (github.event.workflow_run.event == 'push' && + startsWith(github.event.workflow_run.head_branch, 'release-')) + && 'production' || github.event.workflow_run.head_branch }} + cancel-in-progress: false + permissions: + actions: read # download the artifact belonging to the CI run + contents: read # read the commit subject for the deploy message + pull-requests: read # read the pull request title for the deploy message + deployments: write # record the deployment against its environment + statuses: write # report the resulting URL on the commit that was built + env: + REPO: ${{ github.repository }} + HEAD_SHA: ${{ github.event.workflow_run.head_sha }} + HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }} + TRIGGERING_EVENT: ${{ github.event.workflow_run.event }} + ENVIRONMENT: lean-lang.org/functional_programming_lean + steps: + - name: Download book HTML + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + name: book-html + path: html-multi + run-id: ${{ github.event.workflow_run.id }} + github-token: ${{ github.token }} + + - id: info + name: Compute deployment metadata + env: + GH_TOKEN: ${{ github.token }} + run: | + set -euo pipefail + + # Netlify caps an alias at 37 characters. + echo "alias=${HEAD_SHA:0:32}" >> "$GITHUB_OUTPUT" + + # Pushing a release- tag publishes the book. Everything else, master + # included, goes to a preview alias. A tag push arrives here with the + # tag name in head_branch. + case "$TRIGGERING_EVENT:$HEAD_BRANCH" in + push:release-*) echo "production=true" >> "$GITHUB_OUTPUT" ;; + *) echo "production=false" >> "$GITHUB_OUTPUT" ;; + esac + + # The pull request number comes from the commit that was built. The + # message goes to a file because it carries a pull request title or a + # commit subject. + message="" + if [ "$TRIGGERING_EVENT" = pull_request ]; then + message=$(gh api "repos/$REPO/commits/$HEAD_SHA/pulls" \ + --jq 'first(.[] | select(.state == "open")) | "pr#\(.number): \(.title)"') + fi + if [ -z "$message" ]; then + subject=$(gh api "repos/$REPO/commits/$HEAD_SHA" --jq '.commit.message | split("\n")[0]') + message="ref/$HEAD_BRANCH: $subject" + fi + printf '%s' "$message" > deploy-message.txt + + # Search engines index the published book, reached through the release- + # tag path below, which leaves this for the preview deploys. + - name: Keep previews out of search results + if: steps.info.outputs.production != 'true' + run: | + printf '/*\n X-Robots-Tag: noindex\n' > html-multi/_headers + + - name: Install the Netlify CLI + run: npm install --global netlify-cli@27.0.3 + + - id: netlify + name: Deploy to Netlify hosting + env: + NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }} + NETLIFY_SITE_ID: 4e471a74-81e0-42f2-b27c-ca8c80a34f7c + ALIAS: ${{ steps.info.outputs.alias }} + PRODUCTION: ${{ steps.info.outputs.production }} + run: | + set -euo pipefail + + args=(deploy --dir html-multi --no-build --json --message "$(cat deploy-message.txt)") + if [ "$PRODUCTION" = true ]; then + args+=(--prod) + else + args+=(--alias "$ALIAS") + fi + netlify "${args[@]}" > deploy.json + + # The Netlify CLI may precede its result with progress output, so the + # first object carrying the wanted key is the result. + python3 - >> "$GITHUB_OUTPUT" <<'PY' + import json, os, sys + key = "url" if os.environ["PRODUCTION"] == "true" else "deploy_url" + text = open("deploy.json").read() + decoder = json.JSONDecoder() + for start in (i for i, c in enumerate(text) if c == "{"): + try: + deploy, _ = decoder.raw_decode(text[start:]) + except ValueError: + continue + if isinstance(deploy, dict) and key in deploy: + print("url=" + deploy[key]) + break + else: + sys.exit(f"the Netlify CLI output carries no {key}") + PY + + - name: Record the deployment + env: + GH_TOKEN: ${{ github.token }} + URL: ${{ steps.netlify.outputs.url }} + run: | + set -euo pipefail + deployment=$(gh api "repos/$REPO/deployments" --method POST --input - --jq .id <