You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
lake build
error: failed to execute `cc`: no such file or directory (error code: 2)
I can built it iusing msys2, and I get libleancmark.dll but then the binaries don't work on windows either...
#eval main ["README.md"]
results in a crash in the lean --server saying:
libc++abi: terminating with uncaught exception of type lean::exception: could not find native implementation of external declaration 'CMark.renderHtml' (symbols 'l_CMark_renderHtml___boxed' or 'l_CMark_renderHtml')
The text was updated successfully, but these errors were encountered:
@lovettchris
For the first problem, it's that cc (clang) is not installed on your machine.
The second one arises as that the native part is statically linked, which makes interactive #eval impossible.
Maybe reimplment a parser with pure Lean can be a better idea than fixing this. I'll take some time to do it in my spare time this week.
Is this a cmark, lean or lake problem?
I can built it iusing msys2, and I get
libleancmark.dll
but then the binaries don't work on windows either...results in a crash in the lean --server saying:
The text was updated successfully, but these errors were encountered: