Issue adding LeanCopilot as dependency

[fourfactorial]

I am doing this inside VS Code on Windows 11. In a fresh project with the only other dependency as mathlib, doing step 4 of the instructions, "Run lake update LeanCopilot", I get the following output (actual path to project has been redacted, otherwise this is copy-pasted):

PS [path to project]> lake update LeanCopilot
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
⚠ [3/19] Replayed Batteries.Data.Array.Match
warning: Batteries/Data/Array/Match.lean:61:36: `Nat.lt_succ` has been deprecated: Use `Nat.lt_succ_iff` instead

Note: `Nat.lt_succ_iff` is protected. References to this constant must include its prefix `Nat` even when inside its namespace.
⚠ [4/19] Replayed Batteries.Data.String.Basic
warning: Batteries/Data/String/Basic.lean:10:22: `Substring` has been deprecated: Use `Substring.Raw` instead
✖ [13/19] Building Batteries.Data.String.Matcher
trace: .> LEAN_PATH=[path to project]\.lake\packages\Cli\.lake\build\lib\lean;[path to project]\.lake\packages\Qq\.lake\build\lib\lean;[path to project]\.lake\packages\proofwidgets\.lake\build\lib\lean;[path to project]\.lake\packages\importGraph\.lake\build\lib\lean;[path to project]\.lake\packages\LeanSearchClient\.lake\build\lib\lean;[path to project]\.lake\packages\plausible\.lake\build\lib\lean;[path to project]\.lake\packages\batteries\.lake\build\lib\lean;[path to project]\.lake\packages\aesop\.lake\build\lib\lean;[path to project]\.lake\packages\mathlib\.lake\build\lib\lean;[path to project]\.lake\packages\LeanCopilot\.lake\build\lib\lean;[path to project]\.lake\build\lib\lean c:\Users\silas\.elan\toolchains\leanprover--lean4---v4.26.0-rc2\bin\lean.exe [path to project]\.lake\packages\batteries\Batteries\Data\String\Matcher.lean -o [path to project]\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\String\Matcher.olean -i [path to project]\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\String\Matcher.ilean -c [path to project]\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Matcher.c --setup [path to project]\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Matcher.setup.json --json
warning: Batteries/Data/String/Matcher.lean:36:12: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:39:45: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:48:60: `Substring.bsize` has been deprecated: Use `Substring.Raw.bsize` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.bsize` to `Substring.Raw.bsize x`).
error: Batteries/Data/String/Matcher.lean:48:50: Invalid field notation: Function `Substring.bsize` does not have a usable parameter of type `Substring` for which to substitute `m.pattern`

Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation
warning: Batteries/Data/String/Matcher.lean:51:47: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:51:66: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:55:12: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:55:63: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:55:82: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:64:37: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:64:57: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:79:41: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:79:41: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:79:60: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:86:39: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:86:39: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:86:59: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:92:42: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:92:42: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:100:45: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:100:64: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:104:43: `Substring` has been deprecated: Use `Substring.Raw` instead
warning: Batteries/Data/String/Matcher.lean:104:63: `Substring` has been deprecated: Use `Substring.Raw` instead
error: Batteries/Data/String/Matcher.lean:105:16: Invalid field `findSubstr?`: The environment does not contain `Substring.Raw.findSubstr?`
  s.toSubstring
has type
  Substring.Raw
warning: Batteries/Data/String/Matcher.lean:108:46: `Substring` has been deprecated: Use `Substring.Raw` instead
error: Batteries/Data/String/Matcher.lean:109:16: Invalid field `containsSubstr`: The environment does not contain `Substring.Raw.containsSubstr`
  s.toSubstring
has type
  Substring.Raw
error: Lean exited with code 1
Some required targets logged failures:
- Batteries.Data.String.Matcher
error: build failed

So, possibly recent batteries updates cause compatibility issues for right now? But if I am doing something wrong, any guidance would be appreciated!

In the project I have a lakefile.toml as below. I also tried changing rev to "v4.24.0" for LeanCopilot and got what seems to be the same output.

name = "my_project"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["my_project"]
moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[require]]
name = "LeanCopilot"
git = "https://github.com/lean-dojo/LeanCopilot.git"
rev = "main"

[[lean_lib]]
name = "my_project"