lake replay on a new project

Stream: lean4

[Damiano Testa]

I just created a new project not depending on Mathlib (I created it using the ∀ in VSCode and clicking on "New Standalone Project").

The project seems to have been created correctly, I added

require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"

to the lakefile and then a few rounds of lake update and lake build.

I am at a stage where now opening a file I can see that there is a linter warning, the file is imported by the "import all" file in the root dir, but lake build does not report the warning of the file.

[Damiano Testa]

How can I get the (now colored) warnings that lake prints on Mathlib?

[Sebastian Ullrich]

Are you on 4.8.0?

[Damiano Testa]

I was not: I had leanprover/lean4:stable in my lean-toolchain -- thanks!!

[Marc Huisinga]

Damiano Testa said:

I was not: I had leanprover/lean4:stable in my lean-toolchain -- thanks!!

(VS Code creates new projects with leanprover/lean4:stable. Once https://github.com/leanprover/elan/pull/106 is merged, this will resolve to the most recent stable toolchain.)

[Damiano Testa]

Oh, that would be awesome!