Lake and 'cc'

Stream: lean4

[Chris Lovett]

Why is Lake hard coded to look for 'cc' to build .c files? This means on Windows I can't build this really cool lean library that wraps cmark https://github.com/xubaiw/CMark.lean/

But lean toolchain ships clang, and this works, see below, so why can't lake use that?

cd xubaiw/CMark.lean\cmark
C:\Users\clovett\.elan\toolchains\leanprover--lean4---nightly-2022-08-09\bin\clang.exe *.c -IC:\Users\clovett\.elan\toolchains\leanprover--lean4---nightly-2022-08-09\include\clang -I. -c

[Chris Lovett]

I checked the sysroot that Lake is using and it looks right

c:\\Users\\clovett\\.elan\\toolchains\\leanprover--lean4---nightly-2022-08-08

so I wonder if the problem is this line in Lake is not taking into account the executable on windows is 'clang.exe'

if (← cc.pathExists) then cc else "cc"

[Henrik Böving]

It looks for:

def leanCcExe (sysroot : FilePath) :=
  sysroot / "bin" / "clang" |>.withExtension FilePath.exeExtension

which sounds to me like it would respect the exe. I do also remember that Mac is working on Windows himself so I would be surprised if this was truly completely broken on Windows.

[Chris Lovett]

Ah, FilePath.exeExtension, missed that, thanks.

[Chris Lovett]

Hmmm, weird then that I get this:

git clone https://github.com/xubaiw/CMark.lean/
cd CMark.lean
lake build
error: failed to execute `cc`: no such file or directory

[Chris Lovett]

And weirder, Lake InstallPath.lean is finding it:

def check : IO Unit := do
  let x ← findLeanInstall?
  match (x) with
  | some leanInstall => IO.println leanInstall.cc.normalize.toString
  | none => IO.println  "Could not find cc exe"

/-
c:\users\clovett\.elan\toolchains\leanprover--lean4---nightly-2022-08-05\bin\clang.exe
-/
#eval check

Guess I'll have to debug more of Lake to figure out why the cmark *.c files in CMark.lean repo are not trying to use this compiler. There is nothing customizing the .c buld in the CMark.lean lakefile.lean. Unfortunately lake build --verbose is no help here...

[Chris Lovett]

Oh this is weird, in Actions.lean it is hard coded to "cc" and "ar" and ignores all the above LeanInstall information?

def compileO (name : String) (oFile srcFile : FilePath)
(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : LogIO Unit := do
  logInfo s!"Compiling {name}"
  createParentDirs oFile
  proc {
    cmd := compiler.toString
    args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs
  }

def compileStaticLib (name : String) (libFile : FilePath)
(oFiles : Array FilePath) (ar : FilePath := "ar") : LogIO Unit := do
  logInfo s!"Creating {name}"
  createParentDirs libFile
  proc {
    cmd := ar.toString
    args := #["rcs", libFile.toString] ++ oFiles.map toString
  }

def compileSharedLib (name : String) (libFile : FilePath)
(linkArgs : Array String) (linker : FilePath := "cc") : LogIO Unit := do
  logInfo s!"Linking {name}"
  createParentDirs libFile
  proc {
    cmd := linker.toString
    args := #["-shared", "-o", libFile.toString] ++ linkArgs
  }

def compileExe (name : String) (binFile : FilePath) (linkFiles : Array FilePath)
(linkArgs : Array String := #[]) (linker : FilePath := "cc") : LogIO Unit := do
  logInfo s!"Linking {name}"
  createParentDirs binFile
  proc {
    cmd := linker.toString
    args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
  }

[Chris Lovett]

and as expected when I change these strings to "clang" and "llvm-ar" everything starts working... just have to remove fPic options from cmake lakefile.lean and leanc gets a link error ld.lld: error: undefined symbol: __chkstk from libleancmark.a...

[Chris Lovett]

Oh, but weirder and weirder, the lake ffi sample builds just fine in VS Code:
image.png

[Chris Lovett]

Apparently it can build "c++" but not "c" files...

[Chris Lovett]

https://github.com/leanprover/lake/issues/118

[Mac]

@Chris Lovett I am never confused by the discussion here and on lake#116.

First, Lake does not hard code the compiler for building FFI code. Providing a different value for compiler / linker / ar is how you change it. Second, I am on Windows and have built doc-gen4 (which depends on CMark) multiple times successfully. So unless something has changed recently (I admittedly have not built it since the Lake v4 update of doc-gen4), it should be possible to build FFI code just fine on Windows.

[Chris Lovett]

Never mind, Sebasitan already answered my questions in the bug - I was wrongly thinking the clang we ship in the leantoolchain can also be used to build ffi plugins, but it is not a complete version of clang, it is stripped down minimal just enough to build .lean generated .c code. So if my ffi plugin contains complex C or C++ code then that version of clang would not be sufficient. I understand this now. So ignore my line of questioning about the toolchain clang.

[Chris Lovett]

However, when I build CMark in MSYS2 then try and use it in vscode I get this error:

Lean server printed an error: libc++abi: terminating with uncaught exception of type lean::exception: could not find native implementation of external declaration 'CMark.renderHtml' (symbols 'l_CMark_renderHtml___boxed' or 'l_CMark_renderHtml')

[Mac]

@Chris Lovett Do you have a #mwe of the error?

[Chris Lovett]

Yep, from regular windows command prompt (not MSYS2)

git clone git@github.com:xubaiw/CMark.lean.git
cd CMark.lean
lake build

and you should see this:
image.png

Note that I have Strawberry Perl installed which means I do have a compatible c++ compiler here:
image.png

So the lake/example/ffi/lib builds fine :
image.png

and it works in VS Code (so the plugin loads and runs):
image.png