Zulip Chat Archive
Stream: mathlib4
Topic: Noise ProofWidgets in CI
Michael Stoll (Oct 21 2025 at 19:55):
In a recent CI run, I see (several times, actually)
ℹ [413/527] Replayed proofwidgets/widgetPackageLock
trace: ././widget> npm install
trace: stdout:
added 1 package, changed 2 packages, and audited 367 packages in 2s
67 packages are looking for funding
run `npm fund` for details
1 moderate severity vulnerability
To address all issues, run:
npm audit fix
Run `npm audit` for details.
ℹ [414/527] Replayed proofwidgets/widgetJsAll
trace: /home/runner/work/ProofWidgets4/ProofWidgets4/widget> npm clean-install
trace: stdout:
added 365 packages, and audited 366 packages in 8s
68 packages are looking for funding
run `npm fund` for details
1 low severity vulnerability
To address all issues, run:
npm audit fix
Run `npm audit` for details.
trace: stderr:
npm warn deprecated three-mesh-bvh@0.7.8: Deprecated due to three.js version incompatibility. Please use v0.8.0, instead.
trace: /home/runner/work/ProofWidgets4/ProofWidgets4/widget> npm run build
trace: stdout:
> @leanprover-community/proofwidgets4@0.1.0 build
> npx tsc && rollup --environment NODE_ENV:production --config
trace: stderr:
dist/rubiks.js → ../.lake/build/js...
created ../.lake/build/js in 9.9s
dist/recharts.js → ../.lake/build/js...
(!) Circular dependencies
node_modules/d3-interpolate/src/value.js -> node_modules/d3-interpolate/src/array.js -> node_modules/d3-interpolate/src/value.js
node_modules/d3-interpolate/src/value.js -> node_modules/d3-interpolate/src/object.js -> node_modules/d3-interpolate/src/value.js
node_modules/recharts/es6/util/ChartUtils.js -> node_modules/recharts/es6/util/getLegendProps.js -> node_modules/recharts/es6/util/ChartUtils.js
created ../.lake/build/js in 6.5s
dist/rbTree.js → ../.lake/build/js...
(!) Circular dependencies
node_modules/d3-selection/src/selection/index.js -> node_modules/d3-selection/src/selection/select.js -> node_modules/d3-selection/src/selection/index.js
node_modules/d3-selection/src/selection/index.js -> node_modules/d3-selection/src/selection/selectAll.js -> node_modules/d3-selection/src/selection/index.js
node_modules/d3-selection/src/selection/index.js -> node_modules/d3-selection/src/selection/filter.js -> node_modules/d3-selection/src/selection/index.js
...and 12 more
created ../.lake/build/js in 1.6s
dist/presentSelection.js → ../.lake/build/js...
created ../.lake/build/js in 165ms
dist/penroseDisplay.js → ../.lake/build/js...
(!) Circular dependencies
node_modules/true-myth/dist/es/maybe.js -> node_modules/true-myth/dist/es/result.js -> node_modules/true-myth/dist/es/maybe.js
node_modules/@penrose/core/dist/engine/EngineUtils.js -> node_modules/@penrose/core/dist/utils/Util.js -> node_modules/@penrose/core/dist/engine/EngineUtils.js
node_modules/@penrose/core/dist/engine/BBox.js -> node_modules/@penrose/core/dist/contrib/Queries.js -> node_modules/@penrose/core/dist/engine/BBox.js
...and 14 more
created ../.lake/build/js in 14s
dist/penroseCanvas.js → ../.lake/build/js...
(!) Circular dependencies
node_modules/true-myth/dist/es/maybe.js -> node_modules/true-myth/dist/es/result.js -> node_modules/true-myth/dist/es/maybe.js
node_modules/@penrose/core/dist/engine/EngineUtils.js -> node_modules/@penrose/core/dist/utils/Util.js -> node_modules/@penrose/core/dist/engine/EngineUtils.js
node_modules/@penrose/core/dist/engine/BBox.js -> node_modules/@penrose/core/dist/contrib/Queries.js -> node_modules/@penrose/core/dist/engine/BBox.js
...and 14 more
created ../.lake/build/js in 13.6s
dist/ofRpcMethod.js → ../.lake/build/js...
created ../.lake/build/js in 206ms
dist/makeEditLink.js → ../.lake/build/js...
created ../.lake/build/js in 109ms
dist/interactiveSvg.js → ../.lake/build/js...
created ../.lake/build/js in 158ms
dist/interactiveExpr.js → ../.lake/build/js...
created ../.lake/build/js in 109ms
dist/index.js → ../.lake/build/js...
created ../.lake/build/js in 128ms
dist/htmlDisplayPanel.js → ../.lake/build/js...
created ../.lake/build/js in 129ms
dist/htmlDisplay.js → ../.lake/build/js...
created ../.lake/build/js in 124ms
dist/goalTypePanel.js → ../.lake/build/js...
created ../.lake/build/js in 166ms
dist/filterDetails.js → ../.lake/build/js...
created ../.lake/build/js in 135ms
dist/exprPresentation.js → ../.lake/build/js...
created ../.lake/build/js in 150ms
dist/d3Graph.js → ../.lake/build/js...
(!) Circular dependencies
node_modules/d3-selection/src/selection/index.js -> node_modules/d3-selection/src/selection/select.js -> node_modules/d3-selection/src/selection/index.js
node_modules/d3-selection/src/selection/index.js -> node_modules/d3-selection/src/selection/selectAll.js -> node_modules/d3-selection/src/selection/index.js
node_modules/d3-selection/src/selection/index.js -> node_modules/d3-selection/src/selection/filter.js -> node_modules/d3-selection/src/selection/index.js
...and 12 more
created ../.lake/build/js in 2.9s
dist/cancellable.js → ../.lake/build/js...
created ../.lake/build/js in 116ms
dist/animatedHtml.js → ../.lake/build/js...
created ../.lake/build/js in 136ms
Is this something to worry about?
(I also noticed that it took quite a long time before a runner picked up the "build Mathlib (fork)" job...)
𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 (Oct 21 2025 at 20:11):
"Replayed" means that Lake isn't actually building anything, it's just reprinting the build log that was saved when the package was actually built. I thought that mathlib was supposed to be built with log replays turned off to minimize noise, but I guess that's not the case.
Last updated: Dec 20 2025 at 21:32 UTC