Can't update BrownianMotion project

Stream: general

[Etienne Marion]

Hi! I'm trying to update the BrownianMotion project to the last version of mathlib. But when I run Update dependency > mathlib through the VSCode interface, it fails with

info: mathlib: checking out revision '766e19e781a0992344fd4f24d2662858b6b87250'
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
⚠ [3/19] Replayed Batteries.Data.String.Basic
warning: Batteries/Data/String/Basic.lean:28:12: `String.Pos` has been deprecated: Use `String.Pos.Raw` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Pos` to `Pos.Raw x`).
warning: Batteries/Data/String/Basic.lean:29:11: `String.atEnd` has been deprecated: Use `String.Pos.Raw.atEnd` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.atEnd` to `Pos.Raw.atEnd x`).
warning: Batteries/Data/String/Basic.lean:30:13: `String.get` has been deprecated: Use `String.Pos.Raw.get` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.get` to `Pos.Raw.get x`).
warning: Batteries/Data/String/Basic.lean:31:29: `String.next` has been deprecated: Use `String.Pos.Raw.next` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.next` to `Pos.Raw.next x`).
warning: Batteries/Data/String/Basic.lean:34:10: `String.next` has been deprecated: Use `String.Pos.Raw.next` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.next` to `Pos.Raw.next x`).
✖ [7/19] Building Batteries.Data.Array.Match (443ms)
trace: .> LEAN_PATH=/Users/etienne/Lean/brownian-motion/.lake/packages/Cli/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/Qq/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/aesop/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/importGraph/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/plausible/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/kolmogorov_extension4/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/packages/checkdecls/.lake/build/lib/lean:/Users/etienne/Lean/brownian-motion/.lake/build/lib/lean /Users/etienne/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/bin/lean /Users/etienne/Lean/brownian-motion/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o /Users/etienne/Lean/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i /Users/etienne/Lean/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c /Users/etienne/Lean/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup /Users/etienne/Lean/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.setup.json --json
warning: Batteries/Data/Array/Match.lean:64:43: `Stream` has been deprecated: Use `Std.Stream` instead

Note: The updated constant has a different type:
  Type u → outParam (Type v) → Type (max u v)
instead of
  Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)
warning: Batteries/Data/Array/Match.lean:85:30: `Stream` has been deprecated: Use `Std.Stream` instead

Note: The updated constant has a different type:
  Type u → outParam (Type v) → Type (max u v)
instead of
  Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)
warning: Batteries/Data/Array/Match.lean:93:35: `Stream` has been deprecated: Use `Std.Stream` instead

Note: The updated constant has a different type:
  Type u → outParam (Type v) → Type (max u v)
instead of
  Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)
error: Batteries/Data/Array/Match.lean:129:62: Invalid `⟨...⟩` notation: The expected type
  Std.Internal.idOpaque✝.1 (PlausibleIterStep fun step => ∃ step', m.modifyStep it step' = step)
is not an inductive type

Note: This notation can only be used when the expected type is an inductive type with a single constructor
error: Lean exited with code 1
✔ [11/19] Built Cache.IO (741ms)
✔ [12/19] Built Cache.Hashing (472ms)
✔ [18/19] Built Cache.IO:c.o (1.1s)
Some required targets logged failures:
- Batteries.Data.Array.Match
error: build failed
=> Operation failed. Exit code: 1.

So roughly it looks like batteries are not updated along mathlib. But I don't understand why this happens or how I am supposed to deal with this. Help appreciated!

[Rémy Degenne]

Something that might or might not be relevant: BrownianMotion also imports another repository that imports Mathlib, KolmogorovExtension4 (https://github.com/RemyDegenne/kolmogorov_extension4). When I update, I first update Kolmogorov extension, then Brownian motion.

[Etienne Marion]

Thanks for your answer. I updated KolmogorovExtension4 first, it worked, but then the update with Mathlib failed with the same error. And now when I try to re-update KolmogorovExtension4 it fails with the same error too, so it looks like things go wrong when the lean-toolchain is updated.

[Rémy Degenne]

I just merged a bump into KolmogorovExtension4 (https://github.com/RemyDegenne/kolmogorov_extension4/pull/67) and then tried an update of BrownianMotion and everything went smoothly.

[Rémy Degenne]

https://github.com/RemyDegenne/brownian-motion/pull/178

[Rémy Degenne]

I did all of that with the command line and always used lake update (I don't know what the VSCode command does, but maybe lake update mathlib?)

[Etienne Marion]

Oh okay I misunderstood what you said, I though you meant update KolmogorovExtension as a dependency of BrownianMotion. But obviously if KolmogorovExtension is not itself up to date with mathlib it makes sense that I can't update BrownianMotion :man_facepalming:

[Etienne Marion]

Rémy Degenne said:

I did all of that with the command line and always used lake update (I don't know what the VSCode command does, but maybe lake update mathlib?)

Yes I am pretty sure it's the same.

[Rémy Degenne]

Rémy Degenne said:

https://github.com/RemyDegenne/brownian-motion/pull/178

Oh well, the blueprint failed in CI. But it worked locally, and the error has nothing to do with what you reported above, so that's another issue. I'll retry the job, perhaps it's nothing.

[Rémy Degenne]

Running it again did not work. It looks like we have an issue with the blueprint build step, which comes from docgen-action: https://github.com/RemyDegenne/brownian-motion/actions/runs/18802781358/job/53652797867?pr=178

[Rémy Degenne]

We get a no such option: --global-option error, which seems to come from this line: https://github.com/leanprover-community/docgen-action/blob/9bac8404c6aaa222eaa32901302d85f5342294d5/action.yml#L104

[Bryan Gin-ge Chen]

I've opened docgen-action#11 to hopefully fix this. If you'd like to help test it, you could temporarily replace this line with:

        uses: leanprover-community/docgen-action@1417dc7f90338c875da5e5870c03a287d8348896 # docgen-action#11

[Rémy Degenne]

Thanks for looking at the issue so quickly! I pushed this fix. CI is running at https://github.com/RemyDegenne/brownian-motion/actions/runs/18803660313/job/53654567046?pr=178

[Riccardo Brasca]

Sorry, wrong button

[Rémy Degenne]

The fix worked!

[Etienne Marion]

Great, thanks!

[Rémy Degenne]

I merged the BrownianMotion bump PR. I'll open another PR to BrownianMotion to change the docgen-action line again once the fix PR is merged there.

[Bryan Gin-ge Chen]

Thanks for testing! I'll let @Anne Baanen merge the PR when they're back.

[Kevin Buzzard]

I'm hitting the same no such option: --global-option error in the ClassFieldTheory repo (main is currently not passing CI). We have

      - if: github.ref == 'refs/heads/main'
        name: Build project documentation
        id: build-docgen
        uses: leanprover-community/docgen-action@main
        with:
          blueprint: true

in .github/workflows.push.yml. What do I change it to?

[Rémy Degenne]

You can change the "uses" line to the one Bryan wrote above. But once the docgen-action PR is merged you'll want to revert that change to follow main again.