Zulip Chat Archive

Stream: new members

Topic: Question about build Lean 4


Jason He (Jun 14 2022 at 18:59):

Following build instruction, I ran into below error.
Anyone can give me some hint on how to resolve this?
This is a new enlistment.

Zifeng@hzfpro MINGW64 ~/lean4/build/release
$ cmake ../..
-- Configuring done
-- Generating done
CMake Error:
Running
'E:/mysys64/mingw64/bin/ninja.exe' '-C' 'E:/mysys64/home/Zifeng/lean4/build/release' '-t' 'recompact'
failed with:
ninja: error: build.ninja:459: bad $-escape (literal $ must be written as $$)
CMake Generate step failed. Build files cannot be regenerated correctly.


Last updated: Dec 20 2023 at 11:08 UTC