lake build --help

Stream: lean4

[Bolton Bailey]

Produces the following line:

  a/+A:c                C file of module `A` of package `a`

Does this mean it builds a .c file? Or a lean file named c.lean?

[Bolton Bailey]

Question 2: What command do I invoke if I want to programmatically check if a particular Mathlib/Path/To/File.lean has no errors in it?

[Damiano Testa]

I think lake env lean file or lake build file. One takes a path, the other the same as import statements. I forget which is which.

[Mario Carneiro]

Q1: It builds a .c file

[Mario Carneiro]

lake build Mathlib.Path.To.File builds the specified module (and all its dependencies if not already built), lake env lean Mathlib/Path/To/File.lean builds the lean file itself but assumes the dependencies are already built