feat: use separate tutorials site

.github/workflows/ci.yml

@@ -161,7 +161,7 @@ jobs:
             - name: Generate HTML (non-release)
               if: github.event_name != 'release'
               run: |
-                  lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --without-html-single
+                  ./generate-html.sh --mode preview
 
             - name: Generate HTML (release)
               if: github.event_name == 'release'
@@ -172,11 +172,16 @@ jobs:
               run: |
                   scripts/check-examples-isolated.sh
 
+            - name: Verify tutorial project zip files build
+              if: github.event_name != 'release'
+              run: |
+                  scripts/check-tutorial-zips.sh
+
             - name: Generate proofreading HTML
               if: github.event_name == 'pull_request'
               id: generate
               run: |
-                  lake --quiet exe generate-manual --depth 2 --verbose --draft --without-html-single --output "_out/draft"
+                  ./generate-html.sh --mode preview --draft --output _out/draft-site
 
             - name: Report status to Lean PR
               if: always() && github.repository == 'leanprover/reference-manual'

.github/workflows/overlay.yml

@@ -1,5 +1,12 @@
 name: Apply Overlays
 
+# This workflow applies HTML overlays (canonical URLs, robots noindex, metadata.js) to
+# deployed content and pushes to the postdeploy branches.
+#
+# In normal operation, the workflow_run trigger fires when release-tag.yml completes.
+# Pushes made by release-tag.yml using GITHUB_TOKEN do NOT trigger the push events
+# (GitHub prevents this to avoid infinite loops).
+
 on:
     workflow_run:
         workflows: ["Deploy Tagged Version"]
@@ -9,6 +16,7 @@ on:
     push:
         branches:
             - "deploy"
+            - "deploy-tutorials"
 
     workflow_dispatch:
 
@@ -34,27 +42,31 @@ 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
+                  git fetch origin deploy-tutorials:deploy-tutorials
+                  git fetch origin postdeploy-tutorials:postdeploy-tutorials
 
+            # Run reference overlay if triggered by workflow_run, workflow_dispatch, or push to deploy
             - name: Run overlay script
+              if: github.event_name != 'push' || github.ref == 'refs/heads/deploy'
               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 --site-dir reference
 
             - name: Push deploy branch
+              if: github.event_name != 'push' || github.ref == 'refs/heads/deploy'
               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
+            # Run tutorials overlay if triggered by workflow_run, workflow_dispatch, or push to deploy-tutorials
+            - name: Run overlay script for tutorials
+              if: github.event_name != 'push' || github.ref == 'refs/heads/deploy-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
+              if: github.event_name != 'push' || github.ref == 'refs/heads/deploy-tutorials'
+              run: |
+                  git push origin postdeploy-tutorials

.github/workflows/release-tag.yml

@@ -115,7 +115,11 @@ jobs:
             - name: Detect deployment structure
               id: detect-structure
               run: |
-                  # Check if we have the new combined site structure or old single-site structure
+                  # Check if we have the new combined site structure or old single-site structure.
+                  # The single-site structure is used for older builds that don't have tutorials.
+                  # Because this workflow runs on tag push, it runs in the context of the tagged
+                  # commit; after tutorial deployments are confirmed working, we can get rid of this
+                  # conditional and just assume the new structure in this workflow.
                   if [ -d "html/site/reference" ]; then
                       STRUCTURE="new"
                       REFERENCE_DIR="html/site/reference"
@@ -134,11 +138,13 @@ jobs:
                   echo "Making deployment from tag: '$TAG_NAME'"
 
                   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
+                  if [ "${{ steps.detect-structure.outputs.structure }}" = "new" ]; then
+                      python deploy/release.py html/site/tutorials "$VERSION" deploy-tutorials
+                  fi
 
             - name: Push deploy branch
               run: |
                   git push origin deploy
-                  # TODO: Push tutorials branch when ready for production:
-                  # git push origin deploy-tutorials
+                  if [ "${{ steps.detect-structure.outputs.structure }}" = "new" ]; then
+                      git push origin deploy-tutorials
+                  fi

.github/workflows/upload-snapshots.yml

@@ -42,31 +42,30 @@ jobs:
                   # 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-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"

.linkchecker/linkcheckerrc

@@ -1,2 +1,6 @@
 [filtering]
 ignorewarnings=url-content-too-large,url-too-long
+
+[checking]
+# Moderate rate limit for localhost - higher values overwhelm Python's simple HTTP server
+maxrequestspersecond=30

.linkchecker/server.py

@@ -0,0 +1,23 @@
+#!/usr/bin/env python3
+"""
+Simple HTTP server that adds a LinkChecker header to allow unlimited request rate.
+"""
+import http.server
+import sys
+
+class LinkCheckerHTTPRequestHandler(http.server.SimpleHTTPRequestHandler):
+    def end_headers(self):
+        # Add LinkChecker header to allow maxrequestspersecond > 10
+        self.send_header('LinkChecker', 'allowed')
+        super().end_headers()
+
+if __name__ == '__main__':
+    port = int(sys.argv[1]) if len(sys.argv) > 1 else 8877
+    directory = sys.argv[2] if len(sys.argv) > 2 else '.'
+
+    import os
+    os.chdir(directory)
+
+    with http.server.HTTPServer(('', port), LinkCheckerHTTPRequestHandler) as httpd:
+        print(f"Serving at port {port} with LinkChecker header enabled")
+        httpd.serve_forever()

Main.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
@@ -44,7 +44,7 @@ where
     extraFiles := [("static", "static")],
     extraHead := #[plausible, staticJs, staticCss],
     emitTeX := false,
-    emitHtmlSingle := true, -- for proofreading
+    emitHtmlSingle := .no,
     logo := some "/static/lean_logo.svg",
     sourceLink := some "https://github.com/leanprover/reference-manual",
     issueLink := some "https://github.com/leanprover/reference-manual/issues",

Manual.lean

@@ -18,7 +18,6 @@ import Manual.ErrorExplanations
 import Manual.Tactics
 import Manual.Simp
 import Manual.Grind
-import Manual.VCGen
 import Manual.BasicTypes
 import Manual.Iterators
 import Manual.BasicProps
@@ -31,6 +30,7 @@ import Manual.Releases
 import Manual.Namespaces
 import Manual.Runtime
 import Manual.SupportedPlatforms
+import Manual.VCGen
 
 open Verso.Genre Manual
 open Verso.Genre.Manual.InlineLean
@@ -58,7 +58,7 @@ Along with many other parts of Lean, the tactic language is user-extensible, so
 Tactics are written in Lean itself, and can be used immediately upon definition; rebuilding the prover or loading external modules is not required.
 
 Lean is also a pure *functional programming language*, with features such as a run-time system based on reference counting that can efficiently work with packed array structures, multi-threading, and monadic {name}`IO`.
-As befits a programming language, Lean is primarily implemented in itself, including the language server, build tool, {tech}[elaborator], and tactic system.
+As befits a programming language, Lean is primarily implemented in itself, including the language server, build tool, {tech (key := "Lean elaborator") -normalize}[elaborator], and tactic system.
 This very book is written in [Verso](https://github.com/leanprover/verso), a documentation authoring tool written in Lean.
 
 Familiarity with Lean's programming features is valuable even for users whose primary interest is in writing proofs, because Lean programs are used to implement new tactics and proof automation.

Manual/BuildTools/Lake/CLI.lean

@@ -308,7 +308,7 @@ Single-character flags cannot be combined; `-HR` is not equivalent to `-H -R`.
 
 :  {lakeOptDef flag}`--reconfigure` or {lakeOptDef flag}`-R`
 
-  Normally, the {tech}[package configuration] file is {tech (key := "elaborator")}[elaborated] when a package is first configured, with the result cached to a {tech}[`.olean` file] that is used for future invocations until the package configuration
+  Normally, the {tech}[package configuration] file is {tech (key := "elaborator") -normalize}[elaborated] when a package is first configured, with the result cached to a {tech}[`.olean` file] that is used for future invocations until the package configuration
   Providing this flag causes the configuration file to be re-elaborated.
 
 : {lakeOptDef flag}`--keep-toolchain`

Manual/Defs.lean

@@ -30,7 +30,7 @@ The following commands in Lean are definition-like: {TODO}[Render commands as th
  * {keyword}`theorem`
  * {keyword}`opaque`
 
-All of these commands cause Lean to {tech (key := "elaborator")}[elaborate] a term based on a {tech}[signature].
+All of these commands cause Lean to {tech (key := "elaborator") -normalize}[elaborate] a term based on a {tech}[signature].
 With the exception of {keywordOf Lean.Parser.Command.example}`example`, which discards the result, the resulting expression in Lean's core language is saved for future use in the environment.
 The {keywordOf Lean.Parser.Command.declaration}`instance` command is described in the {ref "instance-declarations"}[section on instance declarations].
 

Manual/Elaboration.lean

@@ -39,7 +39,7 @@ Roughly speaking, Lean's processing of a source file can be divided into the fol
 
 : Elaboration
 
-  {deftech (key := "elaborator")}[Elaboration] is the process of transforming Lean's user-facing syntax into its core type theory.
+  {deftech (key := "Lean elaborator") -normalize}[Elaboration] is the process of transforming Lean's user-facing syntax into its core type theory.
   This core theory is much simpler, enabling the trusted kernel to be very small.
   Elaboration additionally produces metadata, such as proof states or the types of expressions, used for Lean's interactive features, storing them in a side table.
 
@@ -105,7 +105,7 @@ tag := "macro-and-elab"
 %%%
 
 Having parsed a command, the next step is to elaborate it.
-The precise meaning of {deftech}_elaboration_ depends on what is being elaborated: elaborating a command effects a change in the state of Lean, while elaborating a term results in a term in Lean's core type theory.
+The precise meaning of {deftech -normalize}_elaboration_ depends on what is being elaborated: elaborating a command effects a change in the state of Lean, while elaborating a term results in a term in Lean's core type theory.
 Elaboration of both commands and terms may be recursive, both because of command combinators such as {keywordOf Lean.Parser.Command.in}`in` and because terms may contain other terms.
 
 Command and term elaboration have different capabilities.
@@ -293,7 +293,7 @@ The compiler stores an intermediate representation in an environment extension.
 
 For straightforwardly structurally recursive functions, the translation will use the type's recursor.
 These functions tend to be relatively efficient when run in the kernel, their defining equations hold definitionally, and they are easy to understand.
-Functions that use other patterns of recursion that cannot be captured by the type's recursor are translated using {deftech}[well-founded recursion], which is structural recursion on a proof that some {deftech}_measure_ decreases at each recursive call, or using {ref "partial-fixpoint"}[partial fixpoints], which logically capture at least part of a function's specification by appealing to domain-theoretic constructions.
+Functions that use other patterns of recursion that cannot be captured by the type's recursor are translated using {tech}[well-founded recursion], which is structural recursion on a proof that some {tech}[measure] decreases at each recursive call, or using {ref "partial-fixpoint"}[partial fixpoints], which logically capture at least part of a function's specification by appealing to domain-theoretic constructions.
 Lean can automatically derive many of these termination proofs, but some require manual proofs.
 Well-founded recursion is more flexible, but the resulting functions are often slower to execute in the kernel due to the proof terms that show that a measure decreases, and their defining equations may hold only propositionally.
 To provide a uniform interface to functions defined via structural and well-founded recursion and to check its own correctness, the elaborator proves {deftech}[equational lemmas] that relate the function to its original definition.

Manual/Grind/EMatching.lean

@@ -32,7 +32,7 @@ Each fact added to the whiteboard by E-matching is referred to as an {deftech (k
 Annotating theorems for E-matching, thus adding them to the index, is essential for enabling {tactic}`grind` to make effective use of a library.
 
 In addition to user-specified theorems, {tactic}`grind` uses automatically generated equations for {keywordOf Lean.Parser.Term.match}`match`-expressions as E-matching theorems.
-Behind the scenes, the {tech}[elaborator] generates auxiliary functions that implement pattern matches, along with equational theorems that specify their behavior.
+Behind the scenes, the {tech (key := "Lean elaborator")}[elaborator] generates auxiliary functions that implement pattern matches, along with equational theorems that specify their behavior.
 Using these equations with E-matching enables {tactic}`grind` to reduce these instances of pattern matching.
 
 

Manual/Grind/ExtendedExamples.lean

@@ -12,7 +12,6 @@ import Manual.Meta
 
 import Manual.Grind.ExtendedExamples.Integration
 import Manual.Grind.ExtendedExamples.IfElseNorm
-import Manual.Grind.ExtendedExamples.IndexMap
 
 open Verso.Genre Manual
 open Verso.Genre.Manual.InlineLean
@@ -27,8 +26,10 @@ open Lean.Grind
 tag := "grind-bigger-examples"
 %%%
 
+:::TODO
+Properly link to tutorial section
+:::
+
 {include 1 Manual.Grind.ExtendedExamples.Integration}
 
 {include 1 Manual.Grind.ExtendedExamples.IfElseNorm}
-
-{include 1 Manual.Grind.ExtendedExamples.IndexMap}