Skip to content

Bumping mathlib to 8319c83 would break the build #247

Description

@github-actions

mathlib incompatibility detected

An incompatibility has been detected between this project and recent changes in mathlib.
In other words, this project can't advance to the tip of mathlib without breaking.

First incompatible mathlib commit: 8319c83 — refactor(MeasureTheory): define eLpNorm f to be infinite when not AEStronglyMeasurable (#42406) (2026-09-11 (Felix Pernegger)).

Last-known-good mathlib commit: 5089c57 — chore: simplify proofs with grind (#41903) (2026-09-11 (Felix Pernegger))

Verified when LeanMachineLearning/LML was at: dde3322 — bump referee (2026-09-16 (Remy Degenne)).
You can reproduce this break by:

  • updating mathlib to 8319c83af32e262ad477c8a896a0859cdd061b16
  • running lake update mathlib
  • running lake build

downstream-reports reported at 2026-09-22T00:28:18Z · Workflow run · Job log · Failure log


This issue was last updated on 2026-09-22 by this workflow run. It is maintained automatically by downstream-reports/track-incompatibility. When the incompatibility is resolved, the issue is closed automatically with a comment.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions