### Build Reference Manual HTML Output with Lake

Source: https://context7.com/leanprover/reference-manual/llms.txt

This snippet demonstrates how to build the Lean reference manual into HTML output using Lake, Lean's build system. It covers compiling the manual generator and then executing it to produce documentation with specified depth. It also includes commands for starting a local development server.

```bash
# Build the manual generator executable
lake build

# Generate HTML documentation with depth 2 (controls section nesting)
lake exe generate-manual --depth 2

# Start local development server on port 8880
python3 ./server.py 8880 &

# View the manual at http://localhost:8880

```

--------------------------------

### Build Lean Reference Manual Locally

Source: https://github.com/leanprover/reference-manual/blob/main/README.md

Command to build the Lean reference manual locally. This process involves generating figures from LaTeX sources and requires specific LaTeX packages and utilities like pdftocairo and Vale. After building, a local web server can be started to view the manual.

```shell
lake exe generate-manual --depth 2
python3 ./server.py 8880 &
```

--------------------------------

### Lean Error Explanation Structure

Source: https://github.com/leanprover/reference-manual/blob/main/Manual/ErrorExplanations/README.md

Demonstrates the basic structure of an error explanation file in Lean. It includes necessary imports, documentation metadata, the error header command, a description, and the Examples section with errorExample directives.

```Lean
/- Manual/ErrorExplanations/Foo.lean -/

import VersoManual
import Manual.Meta.ErrorExplanation

open Lean Doc
open Verso.Genre Manual InlineLean

#doc (Manual) "About: `foo`" =>
%%%
shortTitle := "foo"
%%%

{errorExplanationHeader lean.foo}

...mandatory short description...

# Examples
:::
errorExample "Description Should Use Headline Case"
```broken
example := x
````

```output
Unknown identifier `x`
```

```fixed
def x := 19
example := x
```

...optional short discussion of example...
:::

```

--------------------------------

### Serve Documentation Locally with Python Server

Source: https://context7.com/leanprover/reference-manual/llms.txt

Runs a local HTTP server for testing generated documentation. Disables caching headers for immediate visibility of changes during development. Supports custom bind addresses, directories, and ports.

```bash
# Serve the default output directory on port 8000
python3 ./server.py

# Serve on a custom port with custom directory
python3 ./server.py -p 8880 -d _out/html-multi 8880

# The server adds these headers to all responses:
# Cache-Control: no-cache, no-store, must-revalidate
# Pragma: no-cache
# Expires: 0
```

--------------------------------

### Deploy Versioned Documentation with Release Script

Source: https://context7.com/leanprover/reference-manual/llms.txt

Deploys specific versions of the manual using Git tags (vX.Y.Z) for automated builds and deployments. The release.py script manages deployment branch structure, copies HTML to version-specific directories, and updates the 'latest' symlink.

```bash
# Push a version tag to trigger deployment
git tag v4.27.0
git push origin v4.27.0

# The deployment creates this structure on the deploy branch:
# /4.27.0/          - built HTML for this version
# /4.26.0/          - previous version HTML
# /latest           - symlink to most recent stable version

# Manual deployment process (normally automated):
# 1. Build the manual
./deploy/build.sh

# 2. Generate release-ready HTML
./deploy/generate.sh

# 3. Deploy to the deploy branch
python3 deploy/release.py html 4.27.0 deploy

# 4. Overlay metadata (runs on CI)
python3 deploy/overlay.py . deploy postdeploy
```

--------------------------------

### Configure Lake Package for Verso Manual

Source: https://context7.com/leanprover/reference-manual/llms.txt

Sets up the Lean package with dependencies and build optimizations for the verso-manual. Configures compiler flags for faster builds by disabling time-consuming LLVM optimizations beneficial for documentation generation. Includes workarounds for macOS linker issues and sets Lean options.

```lean
require verso from git "https://github.com/leanprover/verso.git"@"main"

package "verso-manual" where
  -- Disable expensive optimizations for faster builds
  moreLeancArgs := #["-O0", "-mllvm", "-fast-isel", "-mllvm", "-fast-isel-abort=0"]
  -- Work around clang linker optimization hint issues on macOS
  moreLinkArgs :=
    if System.Platform.isOSX then
      #["-Wl,-ignore_optimization_hints"]
    else #[]
  -- Set Lean options for the package
  leanOptions := #[⟨`weak.verso.code.warnLineLength, .ofNat 72⟩, ⟨`experimental.module, true⟩]

@[default_target]
lean_lib Manual where

@[default_target]
lean_exe "generate-manual" where
  needs := #[`@/figures, `@/subversoExtractMod]
  root := `Main
```

--------------------------------

### Define Documentation Sections in Lean

Source: https://context7.com/leanprover/reference-manual/llms.txt

This Lean code snippet illustrates how to define structured documentation sections using the `#doc` directive. It includes metadata such as tags and titles, and hierarchical content that can reference other manual modules using the `{include}` directive.

```lean
#doc (Manual) "The Lean Language Reference" =>
%%% 
tag := "lean-language-reference"
shortContextTitle := "Lean Reference"
%%%

This is the _Lean Language Reference_.
It is intended to be a comprehensive, precise description of Lean.
This manual covers Lean version {versionString}[].

{include 0 Manual.Intro}
{include 0 Manual.Elaboration}
{include 0 Manual.Interaction}
{include 0 Manual.Types}
{include 0 Manual.SourceFiles}

```

--------------------------------

### Configure Manual Generation Output in Lean

Source: https://context7.com/leanprover/reference-manual/llms.txt

This Lean code snippet configures the manual generation process. It specifies extra files, head elements (like JavaScript and CSS), output formats, and repository/issue links. The configuration is passed to the `manualMain` function from VersoManual.

```lean
def main :=
  manualMain (%doc Manual) (config := config) (extraSteps := [extractExamples])
where
  config :=
    { extraFiles := [("static", "static")],
      extraHead := #[plausible, staticJs, staticCss],
      emitTeX := false,
      emitHtmlSingle := true,
      logo := some "/static/lean_logo.svg",
      sourceLink := some "https://github.com/leanprover/reference-manual",
      issueLink := some "https://github.com/leanprover/reference-manual/issues",
    }

```

--------------------------------

### Vale Linting Command

Source: https://github.com/leanprover/reference-manual/blob/main/CONTRIBUTING.md

Command to run the Vale linter on preprocessed HTML files. Assumes the HTML has been converted to the 'html-vale' directory using the `rewrite_html.py` script.

```bash
vale html-vale
```

--------------------------------

### Lean Code Block with Options

Source: https://github.com/leanprover/reference-manual/blob/main/CONTRIBUTING.md

Defines a code block containing Lean commands. It supports naming for `leanOutput` references, and options to `keep` environment changes (default true) or mark the code as expected to contain an `error` (default false).

```lean
```lean
name := "myCodeBlock"
keep := true
error := false

-- Lean commands here
```
```

--------------------------------

### Python Script for HTML Preprocessing

Source: https://github.com/leanprover/reference-manual/blob/main/CONTRIBUTING.md

A Python script utilizing the BeautifulSoup library to rewrite HTML, preparing it for processing by the Vale linter. It outlines the steps for setting up the virtual environment and running the script.

```python
# .vale/scripts/rewrite_html.py
# Requires BeautifulSoup4
# Example usage:
# cd _out
# python ../.vale/scripts/rewrite_html.py html-multi html-vale
```

--------------------------------

### Build LaTeX Figures with Lake in Lean

Source: https://context7.com/leanprover/reference-manual/llms.txt

This Lean code snippet defines a custom Lake target for processing LaTeX files to generate SVG and PDF figures. It uses `lualatex` for compilation and `pdftocairo` for conversion, ensuring that only changed files are rebuilt. The process includes reading directory contents, filtering for `.tex` files, and managing output directories.

```lean
target figures : Array FilePath := do
  let files := (← figureDir.readDir).filterMap fun f => do
    let some "tex" := f.path.extension | throw ()
    let some fn := f.path.fileName | throw ()
    if ".#".isPrefixOf fn then throw ()
    return f.path

  let files := files.qsort (toString · < toString ·)
  let srcs := Job.collectArray (← liftM <| files.mapM inputTextFile)
  srcs.mapM fun srcInfo => do
    buildUnlessUpToDate traceFile (← getTrace) traceFile do
      for src in srcInfo do
        let some f := src.fileStem | continue
        proc { cmd := "lualatex", args := #[f], cwd := some figureDir} (quiet := true)
        proc { cmd := "pdftocairo", args := #["-svg", s!"{f}.pdf", s!"{f}.svg"], cwd := some figureDir} (quiet := true)
        ensureDir figureOutDir
        for fmt in ["pdf", "svg"] do
          let built := s!"{f}.{fmt}"
          IO.FS.withFile (figureDir.join built) .read fun h =>
            IO.FS.withFile (figureOutDir.join built) .write fun h' => do
              let mut buf ← h.read 1024
              while !buf.isEmpty do
                h'.write buf
                buf ← h.read 1024
    pure srcInfo

```

--------------------------------

### Add Custom HTML Elements with Lean

Source: https://context7.com/leanprover/reference-manual/llms.txt

Injects custom JavaScript and CSS into the generated documentation using Lean helper functions. These functions create HTML elements for the document head, including analytics scripts, custom styling, and version-aware metadata.

```lean
open Verso.Output.Html in
def plausible := {{ \
    <script defer="defer" data-domain="lean-lang.org" src="https://plausible.io/js/script.outbound-links.js"></script> \
  }}

open Verso.Output.Html in
def staticJs := {{ \
    <script src="static/metadata.js"></script> \
    <script src="static/print.js"></script> \
  }}

open Verso.Output.Html in
def staticCss := {{ \
    <link rel="stylesheet" href="static/colors.css" /> \
    <link rel="stylesheet" href="static/theme.css" /> \
    <link rel="stylesheet" href="static/fonts/source-serif/source-serif-text.css" /> \
    <link rel="stylesheet" href="static/fonts/source-code-pro/source-code-pro.css" /> \
  }}
```

--------------------------------

### Lean Output Reference

Source: https://github.com/leanprover/reference-manual/blob/main/CONTRIBUTING.md

Represents a code block containing output from a prior `lean` block. The `severity` argument can filter the output to 'information', 'warning', or 'error'.

```lean
```leanOutput "myCodeBlock"
severity := "information"
```
```

--------------------------------

### Lean Term Code Block with Options

Source: https://github.com/leanprover/reference-manual/blob/main/CONTRIBUTING.md

Specifies a code block containing a Lean term. Similar to the `lean` block, it allows naming for `leanOutput`, controlling environment changes with `keep` (default true), and indicating expected errors with `error` (default false).

```lean
```leanTerm
name := "myTerm"
keep := false
error := true

-- Lean term here
```
```

--------------------------------

### Syntax Error Code Block

Source: https://github.com/leanprover/reference-manual/blob/main/CONTRIBUTING.md

Used for code blocks that are expected to contain invalid Lean syntax. The error message is saved under a specified `NAME` for later use with `leanOutput`. The `category` argument defaults to 'term' but can specify other syntactic categories.

```lean
```syntaxError "mySyntaxError"
category := "command"

-- Invalid Lean syntax here
```
```

--------------------------------

### Signature Code Block

Source: https://github.com/leanprover/reference-manual/blob/main/CONTRIBUTING.md

A code block designated for containing the signature of an existing constant in Lean.

```lean
```signature
-- Signature of a Lean constant
```
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.