search

tydeu / lean4-alloy

Write C shims from within Lean code.
Apache License 2.0
42 stars 11 forks source link

How to ensure that C_INCLUDE_PATH is respected by clangd started by Alloy? #6

Closed badly-drawn-wizards closed 4 months ago

badly-drawn-wizards commented 4 months ago

My Lean4 LSP starts with a C_INCLUDE_PATH variable set. This is inherited by the clangd server started by alloy (checked through /proc/<clang-pid>/environ), but it doesn't pick up on the sqlite.h file in that include path.

If I edit a c file using the clangd LSP directly, it finds the header.

A lake build is fine though. :shrug:

tydeu commented 4 months ago

@badly-drawn-wizards After some testing, it appears that Alloy respects additional include paths via CPATH, but not C_INCLUDE_PATH. This is because Alloy's clangd server does not run in C language mode. While it is possible to change this by passing a --language=c to as part of the clang configuration, I am not sure the Alloy server should guarantee it is running in C mode. I am hoping to eventually add C++ support and files may thus end up interleaving C and C++ code in the same shim (which would be impossible with a --langauge=c). Is CPATH a viable solution for your use case?

badly-drawn-wizards commented 4 months ago

I ended up manually adding it to a .clangd file, but then discovered the CPATH. This fits my use case.