chore: parameterize deployment scripts over sub-site

.github/workflows/overlay.yml

@@ -34,14 +34,27 @@ jobs:
           git config --global user.email "41898282+github-actions[bot]@users.noreply.github.com"
           git fetch origin deploy:deploy
           git fetch origin postdeploy:postdeploy
+          # TODO: Fetch tutorials branches when ready for production deployment:
+          # git fetch origin deploy-tutorials:deploy-tutorials
+          # git fetch origin postdeploy-tutorials:postdeploy-tutorials
 
       - name: Run overlay script
         run: |
           echo "Adding overlays to predeploy"
           # -B to prevent creation of __pycache__ directory
           # which would get committed due to lack of .gitignore
-          python -B deploy/overlay.py . deploy postdeploy
+          python -B deploy/overlay.py . deploy postdeploy --site-dir reference
 
       - name: Push deploy branch
         run: |
           git push origin postdeploy
+
+      # TODO: Add these steps when tutorials are ready for production deployment:
+      # - name: Run overlay script for tutorials
+      #   run: |
+      #     echo "Adding overlays to tutorials predeploy"
+      #     python -B deploy/overlay.py . deploy-tutorials postdeploy-tutorials --site-dir tutorials
+      #
+      # - name: Push tutorials deploy branch
+      #   run: |
+      #     git push origin postdeploy-tutorials

.github/workflows/release-tag.yml

@@ -107,15 +107,33 @@ jobs:
         run: |
           ./deploy/generate.sh
 
+      - name: Detect deployment structure
+        id: detect-structure
+        run: |
+          # Check if we have the new combined site structure or old single-site structure
+          if [ -d "html/site/reference" ]; then
+            STRUCTURE="new"
+            REFERENCE_DIR="html/site/reference"
+          else
+            STRUCTURE="old"
+            REFERENCE_DIR="html/html-multi"
+          fi
+          echo "structure=$STRUCTURE" >> "$GITHUB_OUTPUT"
+          echo "reference_dir=$REFERENCE_DIR" >> "$GITHUB_OUTPUT"
+          echo "Detected $STRUCTURE structure, using $REFERENCE_DIR"
+
       - name: Run deployment script
         run: |
           # The tag name is simply GITHUB_REF_NAME
           TAG_NAME=$GITHUB_REF_NAME
           echo "Making deployment from tag: '$TAG_NAME'"
 
-
-          python deploy/release.py html/html-multi "$VERSION" deploy
+          python deploy/release.py ${{ steps.detect-structure.outputs.reference_dir }} "$VERSION" deploy
+          # TODO: Add tutorials deployment when ready for production (requires new structure):
+          # python deploy/release.py html/site/tutorials "$VERSION" deploy-tutorials
 
       - name: Push deploy branch
         run: |
           git push origin deploy
+          # TODO: Push tutorials branch when ready for production:
+          # git push origin deploy-tutorials

.github/workflows/upload-snapshots.yml

@@ -40,3 +40,30 @@ jobs:
           NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
           # This is the site called 'lean-reference-manual-versions'
           NETLIFY_SITE_ID: "91dc33ef-6016-4ac7-bac1-d574e2254405"
+
+  # TODO: Add parallel job for tutorials when ready for production deployment:
+  # deploy-tutorials:
+  #   name: Deploy tutorials release branch to hosting
+  #   runs-on: ubuntu-latest
+  #   if: ${{ github.event_name != 'workflow_run' || github.event.workflow_run.conclusion == 'success' }}
+  #   steps:
+  #     - name: Checkout postdeploy-tutorials branch
+  #       uses: actions/checkout@v4
+  #       with:
+  #         ref: 'postdeploy-tutorials'
+  #
+  #     - name: Upload the current state of the postdeploy-tutorials branch
+  #       uses: nwtgck/actions-netlify@v2.0
+  #       with:
+  #         publish-dir: '.'
+  #         production-branch: postdeploy-tutorials
+  #         production-deploy: true
+  #         github-token: ${{ secrets.GITHUB_TOKEN }}
+  #         deploy-message: |
+  #           Deploy tutorials from ${{ github.ref }}
+  #         enable-commit-comment: false
+  #         enable-pull-request-comment: false
+  #         fails-without-credentials: true
+  #       env:
+  #         NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
+  #         NETLIFY_SITE_ID: "e76b4246-fee7-491e-91ef-a87fffff6ce1"

deploy/overlay.py

@@ -4,7 +4,7 @@
 from release_utils import run_git_command, is_git_ancestor, find_latest_version, find_latest_stable_version
 from pathlib import Path
 
-def add_metadata(directory, version_name, extensions=(".html", ".htm")):
+def add_metadata(directory, version_name, site_dir, extensions=(".html", ".htm")):
     """
     Recursively walk through `directory`, find all HTML files,
     and insert extra elements at the beginning of `<head>`.
@@ -13,7 +13,8 @@ def add_metadata(directory, version_name, extensions=(".html", ".htm")):
 
     Args:
       directory (Path): The directory in which to recursively modify files
-      version_name (str): The version name of the reference manual, e.g. "4.25.0-rc2", "latest", "stable".
+      version_name (str): The version name (e.g. "4.25.0-rc2", "latest", "stable")
+      site_dir (str): The site directory for canonical URLs ("reference" or "tutorials")
     """
     for root, _, files in os.walk(directory):
         for filename in files:
@@ -24,7 +25,7 @@ def add_metadata(directory, version_name, extensions=(".html", ".htm")):
 
                 # Only edit if <head> exists and we haven't already added the meta tag
                 if "<head>" in content and 'name="robots"' not in content:
-                    href = f"https://lean-lang.org/doc/reference/{root}/{filename}".removesuffix("index.html")
+                    href = f"https://lean-lang.org/doc/{site_dir}/{root}/{filename}".removesuffix("index.html")
                     noindex = '' if version_name == "latest" else '\n<meta name="robots" content="noindex">'
                     new_content = content.replace(
                         "<head>",
@@ -45,9 +46,13 @@ def add_metadata(directory, version_name, extensions=(".html", ".htm")):
 #
 # See the README.md in this directory for more about the contract
 # that should be satisfied by how overlays change over time.
-def apply_overlays(deploy_dir):
+def apply_overlays(deploy_dir, site_dir):
     """
     Apply desired overlays inside current directory.
+
+    Args:
+        deploy_dir (str): Directory containing all versions
+        site_dir (str): The site directory for canonical URLs ("reference" or "tutorials")
     """
     latest_version = find_latest_version(deploy_dir)
     latest_stable_version = find_latest_stable_version(deploy_dir)
@@ -67,18 +72,19 @@ def apply_overlays(deploy_dir):
           file.write(content)
 
         # Add appropriate metadata to every file at every version
-        add_metadata(inner, str(inner))
+        add_metadata(inner, str(inner), site_dir)
 
-def deploy_overlays(deploy_dir, src_branch, tgt_branch):
+def deploy_overlays(deploy_dir, src_branch, tgt_branch, site_dir):
     """
     Apply desired overlays inside deploy_dir
     Args:
-        deploy_dir (str): Directory that contains all versions of the manual.
+        deploy_dir (str): Directory that contains all versions of the site.
         This is the content we expect to find at branch `src_branch`, and
         this function modifies it in place to produce a repository state
         suitable for committing to branch `tgt_branch`.
         src_branch (str): Git branch to apply overlays to
         tgt_branch (str): Git branch to commit to
+        site_dir (str): The site directory for canonical URLs ("reference" or "tutorials")
     """
     os.chdir(deploy_dir)
     # Save current git commit to restore later
@@ -88,7 +94,7 @@ def deploy_overlays(deploy_dir, src_branch, tgt_branch):
           raise Exception(f"Git merge will have bad behavior if {tgt_branch} is an ancestor of {src_branch}, try creating a vacuous commit on {tgt_branch} first.")
         run_git_command(["git", "switch", src_branch])
         print(f"Applying overlays...")
-        apply_overlays(deploy_dir)
+        apply_overlays(deploy_dir, site_dir)
         print(f"Creating merge commit...")
         # This is fragile but more specific than "git add ."
         run_git_command(["git", "add", "4*", "latest", "stable"])
@@ -115,16 +121,19 @@ def deploy_overlays(deploy_dir, src_branch, tgt_branch):
         run_git_command(["git", "switch", current_branch])
 
 def main():
-    parser = argparse.ArgumentParser(description="Applies overlays to a manual predeployment branch")
+    parser = argparse.ArgumentParser(description="Applies overlays to a site predeployment branch")
     parser.add_argument("deploy_dir", help="Directory to operate on")
     parser.add_argument("src_branch", help="Git branch to apply overlays to")
     parser.add_argument("tgt_branch", help="Git branch to commit to")
+    parser.add_argument("--site-dir", default="reference",
+                        choices=["reference", "tutorials"],
+                        help="Site directory for canonical URLs (default: reference)")
 
     args = parser.parse_args()
 
     print(f"Applying overlays to directory {args.deploy_dir} branch {args.src_branch} to produce {args.tgt_branch}")
 
-    deploy_overlays(args.deploy_dir, args.src_branch, args.tgt_branch)
+    deploy_overlays(args.deploy_dir, args.src_branch, args.tgt_branch, args.site_dir)
 
 if __name__ == "__main__":
     main()

deploy/release.py

@@ -99,8 +99,8 @@ def deploy_version(source_dir, version, branch):
     print(f"Deployment of version {version} completed successfully.")
 
 def main():
-    parser = argparse.ArgumentParser(description="Deploys a build of the manual to the deployment branch")
-    parser.add_argument("source_dir", help="Source directory to copy content from on the current branch")
+    parser = argparse.ArgumentParser(description="Deploys a build of the reference manual or tutorials to the deployment branch")
+    parser.add_argument("source_dir", help="Source directory to copy content from on the current branch (e.g., html/site/reference or html/site/tutorials)")
     parser.add_argument("version", help="Lean version string (will be used as the directory name)")
     parser.add_argument("branch", help="Git branch for deployment (should be an orphan branch a la gh-pages)")