lean-to icon indicating copy to clipboard operation
lean-to copied to clipboard

Can't make

Open icarosadero opened this issue 2 years ago • 0 comments

I am having trouble executing the makefile. The following is the output of make. Also trying make run-cpp-notebook yields a similar error.

info: downloading component 'lean'
error: binary package was not provided for 'linux'
mkdir -p build
# bear to generate compile_commands.json
# from lean/lake: |supportInterpreter:| Whether to
# expose symbols within the executable to the Lean interpreter. This allows
# the executable to interpret Lean files (e.g., via Lean.Elab.runFrontend).
# Implementation-wise, this passes -rdynamic to the linker when building on
# a non-Windows systems. Defaults to false.
bear -- clang++ -g -O0 asm-kernel.cpp build/ir/REPLLib.c -DLEAN_EXPORTING -o build/asm-kernel-cpp  -std=c++17 \
        -fsanitize=address -fsanitize=undefined -lzmq -lssl -lcrypto \
        -rdynamic \
        -Wl,--export-dynamic \

clang: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated [-Wdeprecated]
clang: error: no such file or directory: 'build/ir/REPLLib.c'
make: *** [makefile:18: build-cpp-kernel] Error 1

When I specify the proper parameters for LEANLDFLAGS in the makefile, I still get "clang: error: no such file or directory: 'build/ir/REPLLib.c'".

Specs:

OS: Kubuntu 22.04.1 LTS x86_64 
Host: A320M-S2H 
Kernel: 5.15.0-57-generic 
Uptime: 2 hours, 12 mins 
Packages: 3425 (dpkg), 47 (nix-default), 31 (snap) 
Shell: zsh 5.8.1 
Resolution: 1920x1080 
DE: Plasma 5.24.7 
WM: KWin 
Theme: [Plasma], Breeze [GTK2/3] 
Icons: [Plasma], breeze-dark [GTK2/3] 
Terminal: yakuake 
CPU: AMD Ryzen 5 3500X (6) @ 3.593GHz 
GPU: NVIDIA GeForce GTX 1650 
Memory: 4054MiB / 32048MiB 

icarosadero avatar Jan 08 '23 16:01 icarosadero