VScode Restart File does full compile

Stream: lean4

[Ralf Stephan]

After downloading new lean files via lake exe cache get VScode tells me to rebuild by pressing Restart File. Which I did. But now it does a full compile, is this intended? I thought what was downloaded is already compiled?

12630 ?        S      0:00  |   |   \_ /home/ralf/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lake se
rve -- /home/ralf/Lean/formal_book
12677 ?        Sl     3:01  |   |       \_ /home/ralf/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lea
n --server /home/ralf/Lean/formal_book
12757 ?        Ssl    0:02  |   |           \_ /home/ralf/.elan/toolchains/leanprover--lean4---v4.7.0/bin
/lean --worker file:///home/ralf/Lean/formal_book/Nat_sandbox.lean
12760 ?        Sl     0:19  |   |               \_ /home/ralf/.elan/toolchains/leanprover--lean4---v4.7.0
/bin/lake setup-file /home/ralf/Lean/formal_book/Nat_sandbox.lean Init Mathlib Mathlib.NumberTheory.Prime
Counting
16346 ?        R      0:18  |   |                   \_ /home/ralf/.elan/toolchains/leanprover--lean4---v4
.7.0/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit
=false ./.lake/packages/mathlib/././Mathlib/Topology/Algebra/UniformGroup.lean -R ./.lake/packages/mathli
b/./. -o ./.lake/packages/mathlib/.lake/build/lib/Mathlib/Topology/Algebra/UniformGroup.olean -i ./.lake/
packages/mathlib/.lake/build/lib/Mathlib/Topology/Algebra/UniformGroup.ilean -c ./.lake/packages/mathlib/
.lake/build/ir/Mathlib/Topology/Algebra/UniformGroup.c

[Yaël Dillies]

Are you sure you restarted the Lean server since you last changed Lean version?

[Ralf Stephan]

In VScode, yes.

[Yaël Dillies]

And was lake exe cache get done decompressing the files when you pressed Restart File?

[Ralf Stephan]

How would I know? If that's an issue why is it not checked by VScode?

[Yaël Dillies]

Well, how did you run lake exe cache get?

[Yaël Dillies]

Ralf Stephan said:

If that's an issue why is it not checked by VScode?

As I said previously, the Restart File button really should tell us (a rough estimate of) how many files will be recompiled. cc @Marc Huisinga

[Ralf Stephan]

On the command line, in the project directory, and as user not root.

[Yaël Dillies]

So you would know because the command line will say Decompressing X files and eventually give you back control

[Ralf Stephan]

It did.

[Yaël Dillies]

Okay then the files were decompressed :smile:

[Yaël Dillies]

Try lake exe cache get! to force a redownload of the entire cache

[Ralf Stephan]

should I kill all lean processes before I do that?

[Kevin Buzzard]

Sure

[Ralf Stephan]

OK that solved it. Thanks.

[Ralf Stephan]

But I'm sure the download before was the same. Hidden state change?