Lake update (?) broke VSCode integration

Stream: lean4

[Sebastian Reichelt]

Apparently, an update of Lean 4 to the 2021-12-13 version broke compilation in VSCode when importing a module from a foreign project.

In lakefile.lean, I have

  dependencies := #[{
    name := `Qq
    src := Source.git "https://github.com/gebner/quote4.git" "9ba80778ff2ae5ff47672f6de081985a5efe3d73"
  }]

After some minor adaptations to the Qq project, lake build works normally, but if I open a file starting with import Qq.Typ in VSCode, I get

`/home/sebastian/.elan/toolchains/leanprover--lean4---nightly-2021-12-13/bin/lake print-paths Init Lean Qq.Typ Qq.Macro` failed:

stderr:
info: Qq: trying to update ./lean_packages/Qq to revision 9ba80778ff2ae5ff47672f6de081985a5efe3d73
error: no such file or directory (error code: 2)
  file: ././Qq/Typ.lean
error: build failed

I suppose this should be ./lean_packages/Qq/Qq/Typ.lean instead (unless the current directory points somewhere else).

[Mac]

@Sebastian Reichelt Yep, new Lake is broken. :sad: It should be fixed once PR #872 is merged.

[Tomas Skrivan]

I also had an issues recently where I was rebuilding the whole mathlib every time I have changed a single file in my project. Switching back to older version solved the issue.