Add Netlify deployment

.github/workflows/ci.yml

@@ -71,8 +71,16 @@ jobs:
 
     - name: Zip html contents
       run: |
-        cd functional-programming-lean/book/
+        pushd functional-programming-lean/book/
         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
@@ -89,3 +97,20 @@ jobs:
         publish_branch: gh-pages
         external_repository: leanprover/functional_programming_in_lean
         personal_token: ${{ secrets.PUBLISH_GITHUB_TOKEN }}
+
+    - name: Deploy to Netlify hosting
+      uses: nwtgck/actions-netlify@v2.0
+        with:
+          publish-dir: functional-programming-lean/book/html
+          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"