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

Link

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