Updates available but manual intervention required
auto-update-lean-fail
Try `lake update` and then investigate why this update causes `lake build`, `lake test`, or `lake lint` to fail.
Files changed in update:
- lake-manifest.json
## Build Output
````
⚠ [1636/1687] Replaying LeanByExample.Diagnostic.Html.GraphDisplay
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Diagnostic/Html/GraphDisplay.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Diagnostic/Html/GraphDisplay.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Diagnostic/Html/GraphDisplay.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Diagnostic/Html/GraphDisplay.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Diagnostic/Html/GraphDisplay.setup.json --json
warning: LeanByExample/Diagnostic/Html/GraphDisplay.lean:6:36: `ProofWidgets.GraphDisplay.Edge` has been deprecated: Namespace moved to ForceGraphDisplay.
warning: LeanByExample/Diagnostic/Html/GraphDisplay.lean:9:29: `ProofWidgets.GraphDisplay.Vertex` has been deprecated: Namespace moved to ForceGraphDisplay.
warning: LeanByExample/Diagnostic/Html/GraphDisplay.lean:13:3: `ProofWidgets.GraphDisplay` has been deprecated: Use `ProofWidgets.ForceGraphDisplay` instead
Some required targets logged failures:
- LeanByExample.Diagnostic.Html.GraphDisplay
error: build failed
````
关闭于 2026-07-04 0 条评论