If I try to load LEAN for this file inside Visual Studio Code: .lean

I get following message:

Imports of 'L01_rfl.lean' are out of date and must be rebuilt. Restarting the file will rebuild them.

I click: Restart File and following error is shown:

`c:\Users\freeman\.elan\toolchains\leanprover--lean4---v4.7.0\bin\lake.exe setup-file D:/Projects/KnightsAndKnaves-Lean4Game/Game/Levels/EquationalReasoning/L01_rfl.lean Init Game.Metadata Game.Doc.doc` failed:

stderr:
info: [4/35] Compiling time.cpp
error: failed to execute `c++`: no such file or directory (error code: 2)

I am not sure how to solve this error as C++ should probably be provided by lake/LEAN.

If I try to load LEAN for this file inside Visual Studio Code: https://github/JadAbouHawili/KnightsAndKnaves-Lean4Game/blob/main/Game/Levels/EquationalReasoning/L01_rfl.lean

I get following message:

Imports of 'L01_rfl.lean' are out of date and must be rebuilt. Restarting the file will rebuild them.

I click: Restart File and following error is shown:

`c:\Users\freeman\.elan\toolchains\leanprover--lean4---v4.7.0\bin\lake.exe setup-file D:/Projects/KnightsAndKnaves-Lean4Game/Game/Levels/EquationalReasoning/L01_rfl.lean Init Game.Metadata Game.Doc.doc` failed:

stderr:
info: [4/35] Compiling time.cpp
error: failed to execute `c++`: no such file or directory (error code: 2)

I am not sure how to solve this error as C++ should probably be provided by lake/LEAN.

• visual-studio-code
• build
• lean
• lake

1 Answer 1

On Linux this should just work.

On Windows I needed to install a C++ compiler and after that it worked successfully.

Run:

lake exe cache get
lake build

in the project folder before opening it in Visual Studio Code.