chore: tell robots not to index non-latest manual (#647)

jcreedcmu · web-flow · commit fe7b1f14f7e8 · 2025-11-06T09:32:36.000Z
Use meta tag to tell robots to not index any version of the manual other than https://lean-lang.org/doc/reference/latest/ . This includes not indexing the version of the manual that is the current referent of `latest`, e.g., at time of writing, https://lean-lang.org/doc/reference/4.25.0-rc2/ would instruct crawlers not to index.
diff --git a/README.md b/README.md
@@ -183,3 +183,30 @@ Therefore we can be careful on both sides:
 - overlays should, ideally, as time goes on, only monotonically
 produce more data, e.g. it should only add fields to injected javascript values and avoid changing the contract of existing fields.
 - documents should, ideally, fail gracefully if injected data they expect to exist is missing
+
+### Local Testing
+
+To test `overlay.py` locally before pushing, do the following.
+- Ensure branches `deploy` and `postdeploy` exist locally.
+- You'll probably want to do
+```
+git fetch
+git checkout deploy
+git reset --hard remotes/upstream/deploy
+git checkout postdeploy
+git reset --hard remotes/upstream/postdeploy
+```
+- From the `reference-manual` checkout directory, on branch `main`, from a clean
+working directory (i.e. make sure to commit any changes you've made) run
+```shell
+python3 -B deploy/overlay.py . deploy postdeploy
+```
+- Inspect whatever `postdeploy` results you're interested in, e.g.
+```
+git show postdeploy:4.25.0-rc2/Type-Classes/Basic-Classes/index.html
+# Expect to see <meta name="robots" content="noindex">
+```
+```
+git show postdeploy:latest/Type-Classes/Basic-Classes/index.html
+# Expect to *not* see <meta name="robots" content="noindex">
+```
diff --git a/deploy/overlay.py b/deploy/overlay.py
@@ -4,6 +4,32 @@
 from release_utils import run_git_command, is_git_ancestor, find_latest_version, find_latest_stable_version
 from pathlib import Path
 
+def add_noindex_meta(directory, extensions=(".html", ".htm")):
+    """
+    Recursively walk through `directory`, find all HTML files,
+    and insert <meta name="robots" content="noindex"> right after <head>.
+    """
+    for root, _, files in os.walk(directory):
+        for filename in files:
+            if filename.lower().endswith(extensions):
+                filepath = os.path.join(root, filename)
+                with open(filepath, "r", encoding="utf-8", errors="ignore") as f:
+                    content = f.read()
+
+                # Only edit if <head> exists and we haven't already added the meta tag
+                if "<head>" in content and 'name="robots"' not in content:
+                    new_content = content.replace(
+                        "<head>",
+                        '<head>\n<meta name="robots" content="noindex">'
+                    )
+
+                    # Write back the modified file
+                    with open(filepath, "w", encoding="utf-8") as f:
+                        f.write(new_content)
+                    print(f"Updated: {filepath}")
+                else:
+                    print(f"Skipped: {filepath}")
+
 # This function is the right thing to change to change the
 # content of the overlays that are applied.
 #
@@ -15,11 +41,12 @@ def apply_overlays(deploy_dir):
     """
     latest_version = find_latest_version(deploy_dir)
     latest_stable_version = find_latest_stable_version(deploy_dir)
-    print (f"LATEST VERSION {latest_version}")
-    print (f"LATEST STABLE VERSION {latest_stable_version}")
+    print (f"overlay.py: the latest lean version is {latest_version}")
+    print (f"overlay.py: the latest stable lean version is {latest_stable_version}")
     header = "// This file was automatically generated by reference-manual/deploy/overlay.py"
     for inner in Path(deploy_dir).iterdir():
       if inner.is_dir() and (inner / "static").is_dir():
+        # Generate some version metadata
         filename = inner / "static" / "metadata.js"
         content = f"{header}\nwindow.metadata = {{versionString: \"{inner}\"}};\n"
         if str(inner) == latest_version or str(inner) == "latest":
@@ -29,6 +56,10 @@ def apply_overlays(deploy_dir):
         with open(filename, 'a') as file:
           file.write(content)
 
+        # Tell robots not to index anything other than latest
+        if str(inner) != "latest":
+           add_noindex_meta(inner)
+
 def deploy_overlays(deploy_dir, src_branch, tgt_branch):
     """
     Apply desired overlays inside deploy_dir
@@ -64,7 +95,7 @@ def deploy_overlays(deploy_dir, src_branch, tgt_branch):
         # (see https://stackoverflow.com/questions/4911794/git-command-for-making-one-branch-like-another/4912267#4912267 for context)
         run_git_command(["git", "merge", "-m", "merge overlays", "--no-ff", "--no-edit", "-s",  "ours", tgt_branch])
         run_git_command(["git", "switch", tgt_branch])
-        run_git_command(["git", "reset", "--hard", src_branch])
+        run_git_command(["git", "reset", "--hard", src_branch, "--"])
         run_git_command(["git", "switch", src_branch])
         # Rewind the src_branch back past the merge commit and the
         # overlay commit. This cleanup probably isn't strictly necessary
