max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: avoid warning by dropping '#pragma once'

Browse source 
Before this change, we would see the warning:

	"#pragma once in main file"
This commit is contained in:
Tobias Grosser 2023-01-04 05:35:48 +00:00 • committed by Sebastian Ullrich
parent 905d3204ae
commit d74d4230b7
2 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/runtime/CMakeLists.txt
View file

@ -24,6 +24,8 @@ if(LLVM)
FILE(READ "${CMAKE_CURRENT_SOURCE_DIR}/../include/lean/lean.h" LEAN_H)
# generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend
string(REPLACE "static inline" "__attribute__((always_inline))" LEAN_H "${LEAN_H}")
# drop '#pragma once' in .c file to avoid warning
string(REPLACE "#pragma once" "" LEAN_H "${LEAN_H}")
file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c" "${LEAN_H}")
message("Generating LLVM bitcode file for Lean runtime at '${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/lean.h.bc'")
add_custom_command(

2
stage0/src/runtime/CMakeLists.txt generated
View file

@ -24,6 +24,8 @@ if(LLVM)
FILE(READ "${CMAKE_CURRENT_SOURCE_DIR}/../include/lean/lean.h" LEAN_H)
# generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend
string(REPLACE "static inline" "__attribute__((always_inline))" LEAN_H "${LEAN_H}")
# drop '#pragma once' in .c file to avoid warning
string(REPLACE "#pragma once" "" LEAN_H "${LEAN_H}")
file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c" "${LEAN_H}")
message("Generating LLVM bitcode file for Lean runtime at '${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/lean.h.bc'")
add_custom_command(