diff --git a/.github/workflows/overlay.yml b/.github/workflows/overlay.yml index fc3b54549..b11ee4606 100644 --- a/.github/workflows/overlay.yml +++ b/.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 diff --git a/.github/workflows/release-tag.yml b/.github/workflows/release-tag.yml index f83ef0347..6e574863f 100644 --- a/.github/workflows/release-tag.yml +++ b/.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 diff --git a/.github/workflows/upload-snapshots.yml b/.github/workflows/upload-snapshots.yml index 4ebe20a68..f15e31878 100644 --- a/.github/workflows/upload-snapshots.yml +++ b/.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" diff --git a/deploy/overlay.py b/deploy/overlay.py index e452d3b19..9829be465 100644 --- a/deploy/overlay.py +++ b/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 ``. @@ -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 exists and we haven't already added the meta tag if "" 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' new_content = content.replace( "", @@ -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() diff --git a/deploy/release.py b/deploy/release.py index 9581a9c5e..527328e08 100644 --- a/deploy/release.py +++ b/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)")