Batteries compatibility issue with Lean 4.26.0-rc2

Stream: mathlib4

[Nick_adfor]

Hey folks! I'm running into some compatibility issues with Batteries and Lean 4.26.0-rc2 and wanted to report it.

The Problem:
After updating to Lean 4.26.0-rc2, I'm getting build failures in Batteries due to breaking changes in the Substring API. It looks like there's been a major refactor that's breaking existing code.

What I'm Seeing:

error: Batteries/Data/String/Matcher.lean:48:50: Invalid field notation: Function `Substring.bsize` does not have a usable parameter of type `Substring`
error: Batteries/Data/String/Matcher.lean:105:16: Invalid field `findSubstr?`: The environment does not contain `Substring.Raw.findSubstr?`
error: Batteries/Data/String/Matcher.lean:109:16: Invalid field `containsSubstr`: The environment does not contain `Substring.Raw.containsSubstr`

Plus a bunch of deprecation warnings saying to use Substring.Raw instead of Substring, but then the Raw version doesn't have the same methods available.

Is there a specific Batteries version tag that's compatible with Lean 4.26.0-rc2? Or are there migration instructions for the Substring API changes?

The deprecation messages suggest using Substring.Raw, but then the required methods like findSubstr? and containsSubstr don't seem to be available in that namespace.

Thanks for any help! :folded_hands:

[Nick_adfor]

Or I should ask, what is Batteries doing? Can I just delete it?

[Nick_adfor]

Okay, since even now I don't know what happened to Battery, I'll reject update and get back to v4.25.0

[Markus Himmel]

Batteries has a v4.26.0-rc2 tag that builds successfully with Lean 4.26.0-rc2. The errors suggest that you are using some other revision of Batteries. Could you share the lakefile.toml of your project?

[Nick_adfor]

I see. It might be my lakefile.toml fixing another version that compatible to v4.25.0

[Nick_adfor]

What I try to update from v4.25.0 to v4.26.0 is just typing lake update and I don't know how it will change lakefile.lean (I do not have lakefile.toml) and lake-manifest.json

[Nick_adfor]

I have already deleted the failed file as I lose patience to check the error. Maybe that every coder has it habit to write code, and also has the right to reject a not so friendly Mathlib update. The "not so friendly" may be just from a compatiable problem. :((((((

[Nick_adfor]

Markus Himmel said:

Batteries has a v4.26.0-rc2 tag that builds successfully with Lean 4.26.0-rc2. The errors suggest that you are using some other revision of Batteries. Could you share the lakefile.toml of your project?

I now see new error about v4.26.0-rc2

error: Lean exited with code 3221225477
Some required targets logged failures:
- Mathlib
Failed to build module dependencies.

[Nick_adfor]

stderr:
✖ [7586/7587] Building Mathlib (12s)
trace: .> LEAN_PATH=G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\packages\Cli\.lake\build\lib\lean;G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\packages\batteries\.lake\build\lib\lean;G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\packages\Qq\.lake\build\lib\lean;G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\packages\aesop\.lake\build\lib\lean;G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\packages\proofwidgets\.lake\build\lib\lean;G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\packages\importGraph\.lake\build\lib\lean;G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\packages\LeanSearchClient\.lake\build\lib\lean;G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\packages\plausible\.lake\build\lib\lean;G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\build\lib\lean c:\Users\A1exa\.elan\toolchains\leanprover--lean4---v4.26.0-rc2\bin\lean.exe G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\Mathlib.lean -o G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\build\lib\lean\Mathlib.olean -i G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\build\lib\lean\Mathlib.ilean -c G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\build\ir\Mathlib.c --setup G:\workspace\Lean_workspace\mathlib4-v4.26.0-rc2\.lake\build\ir\Mathlib.setup.json --json
error: Lean exited with code 3221225477
Some required targets logged failures:
- Mathlib
Failed to build module dependencies.

[Nick_adfor]

Why the v4.26.0-rc2 in https://github.com/leanprover-community/mathlib4/tags has a Archive.lean?????

[Nick_adfor]

The README.md show me something but why my Mathlib need IMO???

# Archive

This is an archive for formalizations which don't have a good place in mathlib, probably because there is (almost) no math depending on these results.

We keep these formalizations here so that when mathlib changes, we can keep these formalizations up to date.

## Contributing

If you have done a formalization which you want to add here, just make a pull request to mathlib.

When you make a pull request, do make sure that you put all lemmas which are generally useful in right place in mathlib (in the `Mathlib/` directory).

Try to adhere to the guidelines for mathlib. They will be much less strictly enforced for the archive, but we still want you to adhere to all the conventions that make maintenance easier. This ensures that when mathlib is changing, the mathlib maintainers can fix these contributions without much effort. Here are the guidelines:
- The [style guide](https://leanprover-community.github.io/contribute/style.html) for contributors.
- The [git commit conventions](https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md).
- You don't have to follow the [naming conventions](https://leanprover-community.github.io/contribute/naming.html).

[Nick_adfor]

In this way, I cannot even import Mathlib in a .lean file just because of the 7586 and 7587

[Nick_adfor]

@Joël Riou I may want an assistance from the origin developer, very well thanks.

[Nick_adfor]

Now I just have a very silly way to deal with it: first open lean 4 web and second #min_imports and third paste it to my file.

[Nick_adfor]

I really do not know what happens to 7586 and 7587. Maybe I do not need them. But I cannot promise that I will never add new import when writing my code (So in this way I always import the whole Mathlib).

[Markus Himmel]

We can only help you if you share your lakefile.

[Nick_adfor]

lakefile.lean
lake-manifest.json
lean-toolchain

[Markus Himmel]

Ah, so you're working on mathlib itself, not on a project that is downstream of mathlib. Is your code on a branch somewhere on GitHub? That would make it even easier to take a look.

[Nick_adfor]

All right. I really do not know how to work on some branch :(

[Nick_adfor]

Should I download something else?

[Nick_adfor]

I download it all. https://github.com/leanprover-community/mathlib4/releases/tag/v4.26.0-rc2

[Markus Himmel]

Downloading mathlib as a zip file from the GitHub releases page is not a supported way of using it.

If you want to create a new formalization project that uses mathlib, you should install Lean as laid out in https://lean-lang.org/install/ and then follow the setup guide, which will tell you how to create a project using mathlib.

If you want to work on mathlib itself instead, you should install Lean as laid out in https://lean-lang.org/install/ and then follow mathlib's contribution guide: https://leanprover-community.github.io/contribute/index.html#working-on-mathlib

[Nick_adfor]

You mean that my work now is trying to add new theorem in Mathlib rather than do my own project, where the latter is exactly what I hope to do and the former is I mistakenly do.

[Ruben Van de Velde]

If you want to create a project that depends on mathlib, follow the setup guide as Markus explains in the second paragraph

[Nick_adfor]

Markus Himmel said:

Downloading mathlib as a zip file from the GitHub releases page is not a supported way of using it.

If you want to create a new formalization project that uses mathlib, you should install Lean as laid out in https://lean-lang.org/install/ and then follow the setup guide, which will tell you how to create a project using mathlib.

If you want to work on mathlib itself instead, you should install Lean as laid out in https://lean-lang.org/install/ and then follow mathlib's contribution guide: https://leanprover-community.github.io/contribute/index.html#working-on-mathlib

Error while checking Lean version: error: error during download info: caused by: [28] Timeout was reached ( Failed to connect to raw.githubusercontent.com port 443 after 21056 ms: Could not connect to server)

[Nick_adfor]

I may say that Americans and Europeans will never know that why I prefer using edge to download a mathlib.

[Nick_adfor]

Because the network problem in mainland China makes it hard to connect github through git bash or vs code so every time I will refuse download anything using it.

[Nick_adfor]

So the "supported" method in Europe might not be a supported method in China.

[Nick_adfor]

No!!!!!!!!!!!!!!!!!!!!! Why it cannot just read the file I've just copied from mathlib to the new project path ".lake/packages"???