broken blueprint

Stream: lean4

[Kevin Buzzard]

My blueprint is broken on the FLT repo. I've just bumped mathlib so I'm on leanprover/lean4:v4.6.0-rc1 and every time I push to master I get a build error in CI:

Run ~/.elan/bin/lake -Kenv=dev build FLT
error: dependency '«doc-gen4»' not in manifest; use `lake update «doc-gen4»` to add it
Error: Process completed with exit code 1.

I've typed those commands locally and they have no effect: stuff gets downloaded but no changes are made to any file according to git. Is this a Lean problem or a blueprint problem?

[Mauricio Collares]

You should bump mathlib by running lake -R -Kenv=dev update. If you run a bare lake update, the doc-gen dependencies get deleted from lake-manifest.json.

[Mauricio Collares]

This UX is being improved in lean4#3174.

[Kevin Buzzard]

I now have this:

...
[2264/4031] Documenting module: Std.Lean.Meta.InstantiateMVars
stdout:
WARNING: Failed to calculate equational lemmata for Lean.Level.substParams.go: (deterministic) timeout at 'whnf', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
WARNING: Failed to calculate equational lemmata for Lean.Expr.data: (deterministic) timeout at 'whnf', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
WARNING: Failed to calculate equational lemmata for Lean.ForEachExpr.visit: (deterministic) timeout at 'whnf', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
WARNING: Failed to calculate equational lemmata for Lean.Elab.Eqns.removeUnusedEqnHypotheses.go: tactic 'simp' failed, nested error:
(deterministic) timeout at 'simp', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
WARNING: Failed to calculate equational lemmata for Lean.Meta.caseValues.loop: (deterministic) timeout at 'whnf', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
WARNING: Failed to calculate equational lemmata for Lean.Expr.stripArgsN: tactic 'simp' failed, nested error:
(deterministic) timeout at 'simp', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
WARNING: Failed to calculate equational lemmata for Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs: failed to generate equational theorem for 'Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs'
...

[Henrik Böving]

That's perfectly normal, there are many equational lemma that are too large to compute in reasonable time so it will just not do it, it's just a warning for that reason @Kevin Buzzard

[Kevin Buzzard]

Oh yes I see! In fact they did not cause an error in CI! Thanks!