ITADN

Updates available but manual intervention required

#2499Closedgithub-actions[bot] 创建于 2026-07-03
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 条评论