Am I generating library docs the right way?

Stream: general

[Stuart Hungerford]

I'm trying to generate docs for a test library project. This is the lakefile:

name    = "foundations"
version = "0.1.0"

[[lean_lib]]
name = "Foundations"

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[require]]
name = "doc-gen4"
git = "https://github.com/leanprover/doc-gen4.git"
rev = "main"

[[require]]
name = "REPL"
git = "https://github.com/leanprover-community/repl"

I'm doing a lake update and a lake build Foundations:docs but I'm seeing these errors:

⟩ lake build Foundations:docs
ℹ [131/443] Replayed «doc-gen4»/bibPrepass
info: stdout:
INFO: reference page disabled
✖ [154/443] Running foundations:srcUri.github
error: Failed to find a git remote in your project, consider reading: https://github.com/leanprover/doc-gen4#source-locations
git exited with code 2 while looking for the git remote in /Users/stu/projects/foundations
ℹ [867/1156] Replayed ImportGraph.Imports:docs
info: stdout:
WARNING: Failed to calculate equational lemmata for Lean.Name.findHome: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
ℹ [932/1394] Replayed Qq.Match:docs
info: stdout:
WARNING: Failed to calculate equational lemmata for Qq.Impl.makeMatchCode: failed
WARNING: Failed to obtain information for: Qq.Impl.withLetHave: failed
WARNING: Failed to calculate equational lemmata for Qq.Impl.mkQqLets: failed
...
Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
ℹ [1191/1394] Replayed «doc-gen4»/coreDocs
info: stdout:
WARNING: Failed to calculate equational lemmata for Std.Time.DateTime.weekday: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Std.Time.PlainDateTime.weekday: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Std.Time.Timestamp.toPlainDateTimeAssumingUTC: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
info: stdout:
WARNING: Failed to calculate equational lemmata for Lean.Elab.Command.elabElabRulesAux: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Server.FileWorker.setupFile: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Server.Watchdog.tryWriteMessage: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Meta.FindSplitImpl.visit: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
WARNING: Failed to calculate equational lemmata for Lean.Meta.Grind.simpForall: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
WARNING: Failed to calculate equational lemmata for Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs: failed to generate equational theorem for `Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs`
case succ
α : Type
m : Type → Type
inst : Monad m
inst_1 : MonadReaderOf Lean.SubExpr m
inst_2 : MonadWithReaderOf Lean.SubExpr m
xf : m α
xa : α → m α
n : Nat
⊢ (do
      let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr
      (match (motive := (maxArgs : Nat) → Lean.Expr → Nat.rec PUnit (fun n n_ih => m α ×' n_ih) maxArgs → m α) n.succ,
            __do_lift with
          | maxArgs'.succ, fn.app arg => fun x => do
            let acc ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn x.1
            Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg (xa acc)
          | x, x_1 => fun x => xf)
          (Nat.rec
            ⟨do
              let _ ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr
              xf, PUnit.unit⟩
            (fun n n_ih =>
              ⟨do
                let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr
                (match (motive := (maxArgs : Nat) → Lean.Expr → Nat.rec PUnit (fun n n_ih => m α ×' n_ih) maxArgs → m α)
                      n.succ, __do_lift with
                    | maxArgs'.succ, fn.app arg => fun x => do
                      let acc ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn x.1
                      Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg (xa acc)
                    | x, x_1 => fun x => xf)
                    n_ih,
                n_ih⟩)
            n)) =
    do
    let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr
    match n.succ, __do_lift with
      | maxArgs'.succ, fn.app arg => do
        let acc ←
          Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn
              (Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs maxArgs' xf xa)
        Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg (xa acc)
      | x, x_1 => xf
WARNING: Failed to calculate equational lemmata for Lean.Elab.Term.mkCoe: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Meta.Grind.pushNot: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Meta.Grind.Arith.isInterpretedTerm: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Server.Completion.dotIdCompletion: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Server.moduleFromDocumentUri: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.CodeAction.holeCodeActionProvider: failed to generate equality theorems for `match` expression `_private.Lean.Server.CodeActions.Provider.0.Lean.CodeAction.holeCodeActionProvider.match_5`
case isTrue
motive✝ : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo) → Sort u_1
x✝¹ : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo)
h_1✝ : (ctx : Lean.Elab.ContextInfo) → (info : Lean.Elab.TermInfo) → motive✝ #[(ctx, info)]
h_2✝ : (x : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo)) → motive✝ x
x✝ : ∀ (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.TermInfo), x✝¹ = #[(ctx, info)] → False
h✝ : x✝¹.size = 1
⊢ (⋯ ▸ fun h => ⋯ ▸ Prod.casesOn (x✝¹.getLit 0 ⋯ ⋯) fun fst snd => h_1✝ fst snd) ⋯ = h_2✝ x✝¹
WARNING: Failed to calculate equational lemmata for Lean.Elab.Tactic.evalGrindCore: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Meta.Tactic.TryThis.addRewriteSuggestion: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Expr.name?: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
ℹ [1192/1394] Ran mathlib:srcUri.github
info: Found git remote for mathlib at https://github.com/leanprover-community/mathlib4 @ 6b1d0f08cb89b784bfb1bb9cabf8016cc8059f07
ℹ [1213/1403] Built Mathlib.Tactic.Simproc.ExistsAndEq:docs
info: stdout:
WARNING: Failed to calculate equational lemmata for ExistsAndEq.withNestedExistsIntro: unquoteExpr: __result.1 : Lean.Expr
WARNING: Failed to calculate equational lemmata for ExistsAndEq.withNestedExistsElim: unquoteExpr: __result.1 : Lean.Expr
Some required targets logged failures:
- foundations:srcUri.github
error: build failed

Can anyone advise?

[Henrik Böving]

The warnings are not important, they just tell you that it failed to compute some equational lemma so it won't appear in the HTML. As for the src URI error the link that the error message tells you in your trace should hopefully be enough to help you figure it out. If not please do tell what part of the instructions there is unclear.

[Stuart Hungerford]

I think that this message:

[138/141] Running mathe:srcUri.github
error: Failed to find a git remote in your project, consider reading: https://github.com/leanprover/doc-gen4#source-locations
git exited with code 2 while looking for the git remote in /Users/stu/projects/mathe/lean
Some required targets logged failures:
- mathe:srcUri.github

This seems to work:

DOCGEN_SRC="file" lake build Mathe:docs

[Stuart Hungerford]

I think that error message is suggesting DOCGEN_SRC="file" lake build Mathe:docs for local file references rather than github remotes