Update dependency in VSCode

Stream: ecosystem infrastructure

[Michael Stoll]

I've noticed the following behavior (in VSCode).

I have a project depending on Mathlib. Say I have pinned Mathlib to v4.24.0 in the lakefile. Now I want to update and change the revision to v4.25.2 (say). When I then click on "Project Actions... -> Update Dependency..." a message pops up that says "Nothing to update - all dependencies are up-to-date.".

Doing "lake update" manually works, though.

It also works if I first unpin Mathlib and "Update Dependency..." and then pin it to the newer version and "Update Dependency..." again. But this seems like a waste of time and energy.

[Michael Stoll]

Hmm. In this specific case (I did observe the behavior described above when moving from one stable version to the next earlier), there is an additional problem:

• I unpin Mathlib and run lake update. This seems to work OK; lake build only builds the local files.
• I pin Mathlib to v4.25.2 and run lake update again. The output ends with

info: mathlib: running post-update hooks
Not running `lake exe cache get` yet, as the `lake` version does not match the toolchain version in the project.
You should run `lake exe cache get` manually.

Following the advice:

> lake exe cache get
⚠ [9/19] Built Batteries.Data.String.Basic
warning: Batteries/Data/String/Basic.lean:10:22: `Substring` has been deprecated: Use `Substring.Raw` instead
⚠ [11/19] Built 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.
✖ [13/19] Building Batteries.Data.String.Matcher
trace: .> LEAN_PATH=/home/mstoll/lean4/JacobiSum/.lake/packages/Cli/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/packages/batteries/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/packages/Qq/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/packages/aesop/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/packages/importGraph/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/packages/plausible/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/packages/mathlib/.lake/build/lib/lean:/home/mstoll/lean4/JacobiSum/.lake/build/lib/lean /home/mstoll/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /home/mstoll/lean4/JacobiSum/.lake/packages/batteries/Batteries/Data/String/Matcher.lean -o /home/mstoll/lean4/JacobiSum/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Matcher.olean -i /home/mstoll/lean4/JacobiSum/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Matcher.ilean -c /home/mstoll/lean4/JacobiSum/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Matcher.c --setup /home/mstoll/lean4/JacobiSum/.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 what can I do to get to v4.25.2?

[Ruben Van de Velde]

Does 4.25.1 work better? Wondering if this issue is specific to .2 or there's something more going on

[Michael Stoll]

The list of Mathlib4 tags does not show a v4.25.1 tag, only v4.25.0 and v4.25.2.

[Ruben Van de Velde]

What, where did it go? It was on 0df2e3c2047ada0d7a2e33dbc6ba2788a44a6062. @Kim Morrison

[Kim Morrison]

Sorry, some tags needed replacing overnight. Everything should be normal again now!