admin管理员组

文章数量:1305474

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
Share Improve this question asked Feb 3 at 19:21 Răzvan Flavius PandaRăzvan Flavius Panda 22.1k18 gold badges119 silver badges175 bronze badges
Add a comment  | 

1 Answer 1

Reset to default 0

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.

本文标签： buildLEAN lake error failed to execute c no such file or directory (error code 2)Stack Overflow

版权声明：本文标题：build - LEAN lake error: failed to execute `c++`: no such file or directory (error code: 2) - Stack Overflow 内容由网友自发贡献，该文观点仅代表作者本人， 转载请联系作者并注明出处：http://www.betaflare.com/web/1741803176a2398344.html， 本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌抄袭侵权/违法违规的内容，一经查实，本站将立刻删除。