Std Error

Stream: lean4

[Shreyas Srinivas]

I get the following build error on a fresh 4.3.0 project :

failed to read file '.\.lake/packages\std\.lake\build\lib\Std\Util\ExtendedBinder.olean', invalid header

[Mario Carneiro]

What is the rest of the output?

[Mario Carneiro]

try deleting .lake and retry

[Shreyas Srinivas]

That is the whole error message.

[Mario Carneiro]

what did you do before this?

[Mario Carneiro]

are there other output lines?

[Shreyas Srinivas]

I downgraded from 4.4.0-rc1 for the second time. First time was flawless.

[Mario Carneiro]

ok so not fresh

[Shreyas Srinivas]

fresh in the sense that the project is brand new.

[Mario Carneiro]

but the .lake directory isn't

[Mario Carneiro]

is this a project depending on mathlib?

[Mario Carneiro]

this is not enough information to reproduce

[Shreyas Srinivas]

yeah
I tried doing the "delete ./.lake" solution from within vscode. Now vscode wants to rebuild everything

[Mario Carneiro]

well yes

[Shreyas Srinivas]

I thought the extension started by getting the cache first these days.

[Mario Carneiro]

is this a project depending on mathlib?

[Shreyas Srinivas]

yes it is a math project

[Shreyas Srinivas]

I am now going to try deleting ./.lake the old school way. On the terminal with vscode closed.

[Mario Carneiro]

• delete .lake
• run lake exe cache get
• run lake build

[Shreyas Srinivas]

The following worked :

• close vscode on that project
• delete .lake
• run lake update

[Marc Huisinga]

Shreyas Srinivas said:

I thought the extension started by getting the cache first these days.

The extension grabs the cache after and before several project-level commands. E.g. the "Build project" command pulls it before building. It doesn't attempt to fetch the cache every time when opening a project in case you touched the build directory in the mean time.
I hope to make this smoother in the future, especially so that working with Git is less painful.

[Shreyas Srinivas]

To make sure I have a working procedure I created another project called "TestAgain". The following works:

• lake new TestAgain math
• cd TestAgain
• open lakefile.lean in a simple text editor (vim,nano,notepad, gedit)
• Change "https://github.com/leanprover-community/mathlib4.git" to "https://github.com/leanprover-community/mathlib4.git" @ "stable"
• close text editor and run lake update
• Open vscode, import Mathlib/Std/Qq and everything works.

This is basically what I was hoping to automate away in the other thread (in a way that involves no extra steps for users who don't care about stable). The first downgrade I did (yesterday I think) worked because I didn't do it from within vscode. There are still some issues to resolve about the way the build inside vscode works.