search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

failed to execute `c++` #241

Closed linonetwo closed 5 months ago

linonetwo commented 5 months ago 
> lake build    
[0/25] Compiling time.cpp
error: failed to execute `c++`: no such file or directory (error code: 2)

A fresh new repo generated from this template. I search the c++ in the repo but not found.

joneugster commented 5 months ago

What OS are you on? if you're on Linux, what does which c++ say?

The error message says that your system has no c++ executable, for example on my machine, which c++ says /usr/bin/c++. And one of the dependencies (lean-i18n) uses Lean's Foreign-function-interface to execute some C++-code.

If we get a bit more info, I think it would be really useful to figure out what to do and add this in the installation instructions

linonetwo commented 5 months ago

I'm using my gaming PC at night.

Today I try it on the dev Mac, it works fine. I just need to figure out how to install c++ on Windows PC, since I already have Visual Stusio 2022 installed, it should have c++ in its toolchain.

joneugster commented 5 months ago

I asked this on Zulip.

joneugster commented 5 months ago

I removed the need to install c++ in the dependent package: https://github.com/hhu-adam/lean-i18n/commit/a761839228816a99e0012c6cd061d3485dd0c637

So it will work without after the next update. Meanwhile, the thread above explains how to install c++

linonetwo commented 5 months ago

Very cool, that will make things easier, thanks.