merge official

.github/workflows/ci.yml

@@ -17,17 +17,17 @@ name: "Build and check HTML"
 jobs:
   build:
     name: Build site and generate HTML
-    runs-on: ubuntu-latest
+    runs-on: nscloud-ubuntu-22.04-amd64-8x16
 
     steps:
       - name: Install deps for figures (OS packages)
         run: |
           sudo apt update && sudo apt install -y poppler-utils
 
       - name: Install deps for figures (TeX)
-        uses: teatimeguest/setup-texlive-action@v3
+        uses: zauguin/install-texlive@v4
         with:
-          version: 2024
+          texlive_version: 2024
           packages: |
             scheme-small
             latex-bin

.github/workflows/merge-main-nightly.yml

@@ -14,7 +14,7 @@ env:
 
 jobs:
   merge-to-nightly:
-    runs-on: ubuntu-latest
+    runs-on: nscloud-ubuntu-22.04-amd64-8x16
     if: github.repository == 'leanprover/reference-manual'
     steps:
       - name: Checkout repository
@@ -51,9 +51,9 @@ jobs:
           sudo apt update && sudo apt install -y poppler-utils
 
       - name: Install deps for figures (TeX)
-        uses: teatimeguest/setup-texlive-action@v3
+        uses: zauguin/install-texlive@v4
         with:
-          version: 2024
+          texlive_version: 2024
           packages: |
             scheme-small
             latex-bin

.github/workflows/pr-testing.yml

@@ -9,17 +9,17 @@ name: "Report PR testing status to the lean4 repository"
 jobs:
   build:
     name: Build site and generate HTML
-    runs-on: ubuntu-latest
+    runs-on: nscloud-ubuntu-22.04-amd64-8x16
 
     steps:
       - name: Install deps for figures (OS packages)
         run: |
           sudo apt update && sudo apt install -y poppler-utils
 
       - name: Install deps for figures (TeX)
-        uses: teatimeguest/setup-texlive-action@v3
+        uses: zauguin/install-texlive@v4
         with:
-          version: 2024
+          texlive_version: 2024
           packages: |
             scheme-small
             latex-bin

.github/workflows/release-tag.yml

@@ -41,9 +41,9 @@ jobs:
           ./deploy/prep.sh
 
       - name: Install deps for figures (TeX)
-        uses: teatimeguest/setup-texlive-action@v3
+        uses: zauguin/install-texlive@v4
         with:
-          version: 2024
+          texlive_version: 2024
           packages: |
             scheme-small
             latex-bin

.github/workflows/update-nightly.yml

@@ -14,7 +14,7 @@ jobs:
   # This job checks whether there's been a new nightly since the last
   # successful automatic update
   check-update:
-    runs-on: ubuntu-latest
+    runs-on: nscloud-ubuntu-22.04-amd64-8x16
     if: github.repository == 'leanprover/reference-manual'
     outputs:
       update-needed: ${{ steps.check-update.outputs.update-needed }}
@@ -96,9 +96,9 @@ jobs:
         sudo apt update && sudo apt install -y poppler-utils
 
     - name: Install deps for figures (TeX)
-      uses: teatimeguest/setup-texlive-action@v3
+      uses: zauguin/install-texlive@v4
       with:
-        version: 2024
+        texlive_version: 2024
         packages: |
           scheme-small
           latex-bin

.vale/scripts/rewrite_html.py

@@ -30,6 +30,13 @@ def process_html_file(filepath, output_filepath):
         elif code_tag.attrs and 'class' in code_tag.attrs and 'hl' in code_tag['class'] and 'lean' in code_tag['class']:
             code_tag.decompose()
 
+    # Delete all content in error explanation pages. This comes from the lean4 repo
+    # and shouldn't be linted here.
+    for element in soup.find_all(class_='error-example-container'):
+        in_sections = element.find_parents('section')
+        if in_sections:
+            in_sections[-1].decompose()
+
     # Delete docstring content (for now)
     for element in soup.find_all(class_="namedocs"):
         element.decompose()

.vale/styles/Lean/Names.yml

@@ -1,20 +1,23 @@
+# This file suggests correct capitalizations / accents for names.
 extends: substitution
 message: Use '%s' instead of '%s'.
 level: error
 ignorecase: true
+# In this list, the key is case-insensitive, and the value should contain the correct case.
 swap:
   - 'de moura': 'de Moura'
   - 'de bruijn': 'de Bruijn'
   - 'blott': 'Blott'
   - 'carneiro': 'Carneiro'
   - 'collatz': 'Collatz'
   - 'lua': 'Lua'
-  - 'Madelaine': 'Madelaine'
+  - 'madelaine': 'Madelaine'
   - 'mathlib': 'Mathlib'
   - 'merkin': 'Merkin'
   - 'peano': 'Peano'
   - 'selsam': 'Selsam'
   - 'simons': 'Simons'
   - 'ullrich': 'Ullrich'
   - 'wadler': 'Wadler'
+  - 'grober': 'Gröbner'
 

.vale/styles/config/ignore/names.txt

@@ -14,3 +14,9 @@ Streicher
 Streicher's
 Ullrich
 Wadler
+Wojciech
+Nawrocki
+Nawrocki's
+Rustan
+Leino
+Leino's

.vale/styles/config/ignore/terms.txt

@@ -24,6 +24,7 @@ constructorless
 conv
 cumulative
 cumulativity
+cutsat
 deallocate
 deallocated
 deallocates
@@ -195,3 +196,4 @@ unparenthesized
 uploader
 upvote
 walkthrough
+zulip

ExtractExplanationExamples.lean

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joseph Rotella
+-/
+
+import Lean.ErrorExplanations
+import SubVerso.Highlighting
+
+/-!
+Tool for extracting rendering data from a batch of error-explanation MWEs with
+identical imports. We use this in a preprocessing step rather than during the
+manual's elaboration so that we can group MWEs with the same imports, which
+avoids the sizable performance overhead of reloading the environment for each
+example.
+-/
+
+open Lean Meta Elab Term SubVerso Highlighting
+
+structure ExtractedExample where
+  highlighted : Highlighted
+  messages : Array (MessageSeverity × String)
+  hash : UInt64
+  version : String
+  deriving ToJson, FromJson
+
+/-- Returns the result of processing this example as well as the environment and message log
+produced *only* by the header-processing step (which is taken to be `envWithMsgs?` if it's supplied) -/
+def processMWE (input : String) (inputHash : UInt64) (envWithMsgs? : Option (Environment × MessageLog)) :
+    IO (ExtractedExample × Environment × MessageLog) := do
+  let fileName   := "Main.lean"
+  let inputCtx   := Parser.mkInputContext input fileName
+  let (hdrStx, s, msgs) ← Parser.parseHeader inputCtx
+  let (env, msgs') ← envWithMsgs?.getDM <| processHeader hdrStx {} {} inputCtx
+  let msgs := msgs ++ msgs'
+  let cmdState := Command.mkState env msgs
+
+  -- If header processing failed, don't try to elaborate the body; however, we
+  -- must still parse it for the syntax highlighter
+  let shouldElab := !msgs.hasErrors
+  let mut (cmdState, stxs) ← processCommands inputCtx s cmdState shouldElab
+  stxs := #[hdrStx] ++ stxs
+  let nonSilentMsgs := cmdState.messages.toArray.filter (!·.isSilent)
+  let hls ← mkHighlights cmdState nonSilentMsgs inputCtx stxs
+  let msgs ← mkMessages nonSilentMsgs
+  let ex := {
+    highlighted := hls
+    messages := msgs
+    hash := inputHash
+    version := Lean.versionString
+  }
+  return (ex, env, msgs')
+where
+  processCommands (inputCtx : Parser.InputContext) (s : Parser.ModuleParserState) (cmdState : Command.State) (doElab : Bool) := do
+    let mut s := s
+    let mut cmdState := cmdState
+    let mut stxs := #[]
+    repeat
+      let scope := cmdState.scopes.head!
+      let pmctx : Parser.ParserModuleContext := {
+        env := cmdState.env,
+        options := scope.opts,
+        currNamespace := scope.currNamespace,
+        openDecls := scope.openDecls
+      }
+      let (stx, s', msgs') := Parser.parseCommand inputCtx pmctx s cmdState.messages
+      s := s'
+      cmdState := {cmdState with messages := msgs'}
+      stxs := stxs.push stx
+      if doElab then
+        (_, cmdState) ← runCommandElabM (Command.elabCommandTopLevel stx) inputCtx cmdState s
+      if Parser.isTerminalCommand stx then
+        break
+    return (cmdState, stxs)
+
+  withNewline (str : String) :=
+    if str == "" || str.back != '\n' then str ++ "\n" else str
+
+  mkHighlights (cmdState : Command.State) (nonSilentMsgs : Array Message)
+      (inputCtx : Parser.InputContext) (cmds : Array Syntax) :
+      IO Highlighted :=
+    let termElab : TermElabM Highlighted := do
+      let mut hls := Highlighted.empty
+      let mut lastPos : String.Pos := 0
+      for cmd in cmds do
+        let hl ← highlightIncludingUnparsed cmd nonSilentMsgs cmdState.infoState.trees [] lastPos
+        hls := hls ++ hl
+        lastPos := (cmd.getTrailingTailPos?).getD lastPos
+      return hls
+    Prod.fst <$> runCommandElabM (Command.liftTermElabM termElab) inputCtx cmdState
+
+  mkMessages (nonSilentMsgs : Array Message) := do
+    nonSilentMsgs.mapM fun msg => do
+      let head := if msg.caption != "" then msg.caption ++ ":\n" else ""
+      let txt := withNewline <| head ++ (← msg.data.toString)
+      pure (msg.severity, txt)
+
+  runCommandElabM {α} (x : Command.CommandElabM α) (ictx : Parser.InputContext)
+      (cmdState : Command.State) (s? : Option Parser.ModuleParserState := none) :
+      IO (α × Command.State) := do
+    let ctx : Command.Context := {
+      cmdPos := s?.map (·.pos) |>.getD 0
+      fileName := ictx.fileName
+      fileMap := ictx.fileMap
+      snap? := none
+      cancelTk? := none
+    }
+    let eio := x.run ctx |>.run cmdState
+    match (← eio.toIO') with
+    | .ok res => return res
+    | .error e => throw <| IO.userError (← e.toMessageData.toString)
+
+def writeEx (outDir : System.FilePath) (id : String) (json : String) : IO Unit := do
+  if ! (← System.FilePath.pathExists outDir) then
+    IO.FS.createDir outDir
+  let path := outDir / (id ++ ".json")
+  IO.FS.writeFile path json
+
+unsafe def main (args : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  enableInitializersExecution
+  let outDir :: inFiles := args |
+    throw <| IO.userError "Usage: extract_explanation_examples <out-dir> <input-files...>\n\
+      where all input files have the same imports"
+  let mut envWithMsgs? : Option (Environment × MessageLog) := none
+  for file in inFiles do
+    let input ← IO.FS.readFile file
+    let inputHash := hash input
+    let some exampleName := (file : System.FilePath).fileStem |
+      throw <| IO.userError s!"Malformed file path: {file}"
+    let (ex, env, msgs) ← processMWE input inputHash envWithMsgs?
+    envWithMsgs? := some (env, msgs)
+    let json := (toJson ex).compress
+    writeEx outDir exampleName json
+  return 0

Main.lean

@@ -15,14 +15,11 @@ def searchModule := {{
     <script type="module" src="/static/search/search-init.js"></script>
   }}
 
-
 open Verso.Output.Html in
 def plausible := {{
     <script defer="defer" data-domain="lean-lang.org/doc/reference/latest" src="https://plausible.io/js/script.outbound-links.js"></script>
   }}
 
-
-
 def fuzzysortLicense : LicenseInfo where
   identifier := "MIT"
   dependency := "fuzzysort v3.1.0"
@@ -81,23 +78,25 @@ def scarfPixel := {{
 def main :=
   manualMain (%doc Manual) (config := config)
 where
-  config := Config.addKaTeX {
+  config := Config.addSearch <| Config.addKaTeX {
     extraFiles := [("static", "static")],
     extraCss := [
       "/static/colors.css",
       "/static/theme.css",
       "/static/print.css",
       "/static/search/search-box.css",
+      "/static/search/search-highlight.css",
       "/static/fonts/source-serif/source-serif-text.css",
       "/static/fonts/source-code-pro/source-code-pro.css",
       "/static/fonts/source-sans/source-sans-3.css",
       "/static/fonts/noto-sans-mono/noto-sans-mono.css"
     ],
     extraJs := [
       -- Search box
-      "/static/search/fuzzysort.js",
+      {filename := "/static/search/fuzzysort.js"},
+      {filename := "/static/search/search-highlight.js", after := #["searchIndex.js"], defer := true},
       -- Print stylesheet improvements
-      "/static/print.js"
+      {filename := "/static/print.js"}
     ],
     extraHead := #[searchModule, plausible],
     extraContents := #[scarfPixel],

Manual.lean

@@ -14,8 +14,10 @@ import Manual.Defs
 import Manual.Classes
 import Manual.Axioms
 import Manual.Terms
+import Manual.ErrorExplanations
 import Manual.Tactics
 import Manual.Simp
+import Manual.Grind
 import Manual.BasicTypes
 import Manual.BasicProps
 import Manual.NotationsMacros
@@ -26,6 +28,7 @@ import Manual.BuildTools
 import Manual.Releases
 import Manual.Namespaces
 import Manual.Runtime
+import Manual.ModuleSystem
 
 open Verso.Genre Manual
 open Verso.Genre.Manual.InlineLean
@@ -36,6 +39,7 @@ set_option maxRecDepth 1024
 #doc (Manual) "The Lean Language Reference" =>
 %%%
 tag := "lean-language-reference"
+shortContextTitle := "Lean Reference"
 %%%
 
 This is the _Lean Language Reference_.
@@ -92,6 +96,8 @@ Thus, this reference manual does not draw a barrier between the two aspects, but
 
 {include 0 Manual.Simp}
 
+{include 0 Manual.Grind}
+
 {include 0 Manual.BasicProps}
 
 {include 0 Manual.BasicTypes}
@@ -129,6 +135,10 @@ Overview of the standard library, including types from the prelude and those tha
 
 {include 0 Manual.BuildTools}
 
+{include 0 Manual.ErrorExplanations}
+
+{include 0 Manual.ModuleSystem}
+
 {include 0 Manual.Releases}
 
 # Index

Manual/Axioms.lean

@@ -147,7 +147,7 @@ partial def List.length' : List α → Nat
   | _ :: xs => xs.length' + 1
 ```
 ```leanOutput otherZero2
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Nat.otherZero', and it does not have executable code
+axiom 'Nat.otherZero' not supported by code generator; consider marking definition as 'noncomputable'
 ```
 
 Axioms used in proofs rather than programs do not prevent a function from being compiled.