配置 Clangd 为 Lean 写 FFI

问题

target ffi.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let srcJob <- inputTextFile <| pkg.dir / "c" / "ffi.c"
  let weakArgs := #["-I", (<- getLeanIncludeDir).toString]
  buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace

分析

• 一种办法是开 -v , --verbose 来手动把 Lake 打印出的命令手动转换成一个 ~.json ，可是过于麻烦，和手写也没什么区别。

-MJ<arg> Write a compilation database entry per input

$ lake build ffi.o
trace: .> c++ -c -o ././.lake/build/c/ffi.o.json ././c/ffi.cpp -I /Users/notch1p/.elan/toolchains/leanprover--lean4---v4.17.0/include -fPIC -MJ././.lake/build/c/ffi.o.json

$ cat ffi.o.json | jq
{
  "directory": ...,
  "file": "././c/ffi.cpp",
  "arguments": [...]
}
jq: parse error: Expected value before ',' at line 1, column 1396

输出条目

target gen_compdb pkg : FilePath := do
  let prefixp := pkg.buildDir / "c"
  let ( jsonp, artp ) :=
      ( pkg.dir / "compile_commands.json"
      , prefixp / "ffi.o.json")
  let srcJob <- inputTextFile <| pkg.dir / "c" / "ffi.c"
  let weakArgs := #["-I", (<- getLeanIncludeDir).toString]
  let some cc <- IO.getEnv "CC"
               | logError "No C compiler is set via $CC" *> pure Job.nil
  unless <- FilePath.pathExists prefixp do createDirAll prefixp
  buildO
    artp srcJob
    weakArgs #["-fPIC", "-fsyntax-only", s!"-MJ{artp}"] cc
    getLeanTrace

• 因为 lake clean 相当暴力，单纯是删除 .lake/build 目录，所以最好把生成的中间产物 *.o.json 全部放在和 *.o 一个路径下面，这样能够一起删除；

• 也正是因为它很暴力，所以在 lake clean 之后跑这个 target 会报错——目录没了，因而还要加一个 createDirAll

• -fsyntax-only 的好处是类似 lint，不输出产物。

• 不是 default_target ， lake build 不会编译。

构建 DB

• 通过 proc 生成 subprocess，用其他工具解决这一问题（sed, jq）。显然这并不 portable，而且写着也麻烦，不如干脆套一层 Makefile (sh) 来解决算了。

# GNU sed
sed -e '1s/^/[\n/' -e '$s/,$/\n]/' *.o.json > compile_commands.json 

# BSD sed
sed -e '1s/^/[\'$'\n''/' -e '$s/,$/\'$'\n'']/' *.o.json > compile_commands.json

#reduce (types := true) FetchM
fun α =>
  IndexBuildFn RecBuildM ->
    CallStack BuildKey ->
      ST.Ref IO.RealWorld BuildStore ->
        BuildContext -> Log -> IO.RealWorld -> EStateM.Result Empty PUnit (EResult Log.Pos Log α)

open IO.FS in 
-- target [...] (body of target gen_compdb)
<* concatJsonWriteFile jsonp pkg

where concatJsonWriteFile (p : FilePath) (pkg : Package) : IO Unit := do
  let dir := pkg.buildDir / "c"
  let jsons := (<-dir.walkDir).filter λ path =>
    path.toString.endsWith r".o.json"
  let cat_json <- jsons.foldlM (init := "") λ acc path =>
      readFile path >>= pure ∘ (· ++ acc)
  pure s!"[{cat_json.dropFirstRight (· == ',')}]" >>= writeFile p

def String.dropFirstRight (s : String) (p : Char -> Bool) (recursor := s.endPos) :=
  match recursor with
  | ⟨0⟩ => s
  | pos @ ⟨next + 1⟩ =>
    if p $ s.get pos then s.set pos ' '
    else dropFirstRight s p ⟨next⟩
termination_by recursor.1

坑

同步问题

• 写下 build0 的时候只是创建一个 SpawnM (Job FilePath) ，

• 直接 lift 到 FetchM

• 关键 通过 runBuild 手动来确保 synchronous 的 build.

两种可行的解决办法

script "compdb" := do
  pure 0 <* runBuild (gen_compdb.fetch) <* concatJsonWriteFile "compile_commands.json" _package

  -- target [...]
  ( runBuild
  $ buildO
      artp srcJob weakArgs
      #["-fPIC", "-fsyntax-only", s!"-MJ{artp}"] "cc" getLeanTrace
  )
  *>pure Job.nil
  <*concatJsonWriteFile jsonp pkg

• 一种顾虑是会有各种 call 带来的性能损失，不过大部分函数都被标注了 @[inline] @[always_inline] 所以也不成问题；

• 还有一种顾虑是因为我们最后返回的是一个 dummy job 而不是真实 Job，所以编译器报错是不会经过 IO 输出到 stdin 上的，会被直接丢弃。
后者的话没有太多办法，因为只是处理 compdb，至于编译器之类的报错不输出应该也没什么影响。直接调 lake build 构建 FFI target 就能看到输出了。

open IO.FS String in target gen_compdb pkg : Unit := do
  let prefixp := pkg.buildDir / "c"
  let ( jsonp, artp ) :=
      ( pkg.dir / "compile_commands.json"
      , prefixp / "ffi.o.json")
  let srcJob <- inputTextFile <| pkg.dir / "c" / "ffi.c"
  let weakArgs := #["-I", (<- getLeanIncludeDir).toString, "-I", "/usr/local/include"]
  let some cc <- IO.getEnv "CC"
               | logError "No C compiler is set via $CC" *> pure Job.nil

  unless <- FilePath.pathExists prefixp do createDirAll prefixp
  ( runBuild
  $ buildO
      artp srcJob weakArgs
      #["-fPIC", "-fsyntax-only", s!"-MJ{artp}"] cc getLeanTrace
  )
  *> pure Job.nil
  <* concatJsonWriteFile jsonp pkg.config where
concatJsonWriteFile (p : FilePath) (pkg : PackageConfig) : LogIO Unit := do
  let dir := pkg.buildDir / "c"
  let jsons := (<-dir.walkDir).filter λ path =>
    path.toString.endsWith r".o.json"

  let cat_json <- jsons.foldlM (init := "") λ acc path =>
      readFile path >>= pure ∘ (· ++ acc)

  logInfo $ reprStr jsons
  liftM <| pure s!"[{dropFirstRight cat_json (· == ',')}]" >>= writeFile p

dropFirstRight (s : String) (p : Char -> Bool) : (r : _ := endPos s) -> String
  | ⟨0⟩ => s
  | pos@⟨next + 1⟩ =>
    if p $ s.get pos then s.set pos ' '
    else dropFirstRight s p ⟨next⟩
  termination_by r => r.1

后记

• 这玩意真的是 LSP 协议么？我原来是用它的，debug 其实挺不错的，但是真的不快，而且没有 intellisense-as-I-type，每次需要 cmd + s 保存一下才行。这实在是太反直觉了。

• 不 Portable. 颠覆本文主旨。那万一我不用 VSCode，我喜欢用 Vim 和 Emacs 呢？实际上我三个换着用呢？至少这三家 Clangd 全行。