leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

ERROR: could not execute external process 'cc' #143

Closed Seasawher closed 1 year ago

Seasawher commented 1 year ago

I was working with gitpod in the following repository.

https://github.com/Seasawher/lean-math-workshop/tree/feature/doc-gen4

lake -Kenv=dev build Tutorial:docs fails again. Error message is here:

error: > cc -c -o ./lake-packages/CMark/build/cmark/cmark_ctype.o ./lake-packages/CMark/cmark/cmark_ctype.c -I ./lake-packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: > cc -c -o ./lake-packages/CMark/build/cmark/houdini_html_u.o ./lake-packages/CMark/cmark/houdini_html_u.c -I ./lake-packages/CMark/cmark -fPIC
error: external command `cc` exited with code 255
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[10/46] Compiling inlinesc
[10/46] Compiling referencesc
error: > cc -c -o ./lake-packages/CMark/build/cmark/cmark.o ./lake-packages/CMark/cmark/cmark.c -I ./lake-packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
(omitted...)
hargoniX commented 1 year ago

You are missing a C compiler to compile the C bindings for CMark here. You probably want to install gcc or clang to fix this.

Seasawher commented 1 year ago

Thank you! I did sucessfully build HTML!