Building the docs locally

Stream: Brownian motion

[Kexing Ying]

Im trying to build the docs for for the Brownian motion project locally with docgen and following the instructions from the docgen readme, I always get a bunch of errors with battery files and some low level mathlib files: e.g:

error: Mathlib/Tactic/Linter/Header.lean:102:59: Invalid field notation: Function `Substring.toString` does not have a usable parameter of type `Substring` for which to substitute `upToHere`

Can anyone try to reproduce this as I'm not sure if its just an issue with my machine

[Kexing Ying]

What I'm doing it this:
1 - git clone https://github.com/RemyDegenne/brownian-motion
2 - Making the folder docbuild and adding the lakefile.toml in the folder
3 - MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 in the docbuild folder
4 - lake build BrownianMotion:docs in the docbuild folder

[Kexing Ying]

This is the start of the output I get:

jason@Jasons-MacBook-Air-5 docbuild % lake build BrownianMotion:docs
✖ [54/160] Building Mathlib.Tactic.Linter.Header
trace: .> LEAN_PATH=/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Qq/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/aesop/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/importGraph/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/plausible/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/kolmogorov_extension4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/checkdecls/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/subverso/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/MD4Lean/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/BibtexQuery/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Cli/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/doc-gen4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/docbuild/.lake/build/lib/lean /Users/jason/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/Mathlib/Tactic/Linter/Header.lean -o /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Header.olean -i /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Header.ilean -c /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Header.c --setup /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Header.setup.json --json
warning: Mathlib/Tactic/Linter/Header.lean:100:17: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Mathlib/Tactic/Linter/Header.lean:102:68: `Substring.toString` has been deprecated: Use `Substring.Raw.toString` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.toString` to `Substring.Raw.toString x`).
error: Mathlib/Tactic/Linter/Header.lean:102:59: Invalid field notation: Function `Substring.toString` does not have a usable parameter of type `Substring` for which to substitute `upToHere`

Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation
warning: Mathlib/Tactic/Linter/Header.lean:108:45: `String.endPos` has been deprecated: Use `String.rawEndPos` instead
warning: Mathlib/Tactic/Linter/Header.lean:109:58: `String.endPos` has been deprecated: Use `String.rawEndPos` instead
warning: Mathlib/Tactic/Linter/Header.lean:212:89: `String.endPos` has been deprecated: Use `String.rawEndPos` instead
error: Lean exited with code 1
⚠ [138/227] Built Batteries.Control.AlternativeMonad
warning: Batteries/Control/AlternativeMonad.lean:107:13: `seq_eq_bind` has been deprecated: Use `seq_eq_bind_map` instead
✖ [166/248] Building Batteries.Linter.UnreachableTactic
trace: .> LEAN_PATH=/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Qq/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/aesop/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/importGraph/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/plausible/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/kolmogorov_extension4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/checkdecls/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/subverso/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/MD4Lean/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/BibtexQuery/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Cli/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/doc-gen4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/docbuild/.lake/build/lib/lean /Users/jason/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/Batteries/Linter/UnreachableTactic.lean -o /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Linter/UnreachableTactic.olean -i /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Linter/UnreachableTactic.ilean -c /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Linter/UnreachableTactic.c --setup /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Linter/UnreachableTactic.setup.json --json
warning: Batteries/Linter/UnreachableTactic.lean:38:35: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`).
error: Batteries/Linter/UnreachableTactic.lean:38:23: failed to synthesize
  BEq String.Range

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
warning: Batteries/Linter/UnreachableTactic.lean:69:26: declaration uses 'sorry'
warning: Batteries/Linter/UnreachableTactic.lean:69:26: declaration uses 'sorry'
warning: Batteries/Linter/UnreachableTactic.lean:74:18: unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Batteries/Linter/UnreachableTactic.lean:80:12: declaration uses 'sorry'
warning: Batteries/Linter/UnreachableTactic.lean:80:12: declaration uses 'sorry'
warning: Batteries/Linter/UnreachableTactic.lean:84:12: declaration uses 'sorry'
warning: Batteries/Linter/UnreachableTactic.lean:87:18: unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Batteries/Linter/UnreachableTactic.lean:113:15: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`).
warning: Batteries/Linter/UnreachableTactic.lean:114:17: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`).
error: Batteries/Linter/UnreachableTactic.lean:115:59: Invalid field notation: Type of
  unreachable
is not known; cannot resolve field `qsort`
error: Batteries/Linter/UnreachableTactic.lean:115:2: failed to construct 'ForIn' instance for collection
  ?m.252
and monad
  ReaderT Context (StateRefT' IO.RealWorld State (EIO Exception))
warning: Batteries/Linter/UnreachableTactic.lean:111:2: declaration uses 'sorry'
error: Lean exited with code 1
✖ [181/278] Building Batteries.Lean.Meta.UnusedNames

........

[Kexing Ying]

Full output:
PastedText.txt

[Pietro Monticone]

I’ll take a look at it tomorrow

[Pietro Monticone]

Hey @Kexing Ying, sorry for the delay (busy with #ItaLean 2025 stuff).

The instructions on the doc-gen4 README are perfectly fine, but you should remember to pin its compatible version, namely the docbuild/lakefile.toml should be:

name = "docbuild"
reservoir = false
version = "0.1.0"
packagesDir = "../.lake/packages"

[[require]]
name = "BrownianMotion"
path = "../"

[[require]]
scope = "leanprover"
name = "doc-gen4"
rev = "v4.25.0"

[Pietro Monticone]

In case you want to download the docs directly, here they are doc.zip.

[Kexing Ying]

Ah, changing the version in lakefile.toml worked! Thanks a lot!