Wolfram/LeanLink | Paclet Repository

Wolfram`LeanLink`

LeanBuild

LeanBuild [dir,{"Module1",...}]
	builds those modules of the Lake project in dir and returns Success or a Failure carrying lake's output.

LeanBuild [dir]
	builds the project's default targets.

Details and Options

▪

LeanImport

loads a project's compiled

.olean

files, so the modules must be built first;

LeanBuild

does that from the Wolfram Language.

▪

The build uses the

lake

of the toolchain that the project's

lean-toolchain

file pins, called directly rather than through elan's proxy, so a build never downloads a toolchain. A pin that is not installed returns a

"ToolchainNotInstalled"

Failure

naming the

elantoolchaininstall

command.

▪

A failed build returns a

"LeanBuildFailed"

Failure

whose

"Output"

holds lake's messages and whose

"ExitCode"

is lake's exit code.

▪

A successful build drops LeanLink's cached environments for that project, so the next

LeanImport

loads the new

.olean

files.

▪

The project should pin the same Lean version as LeanLink's runtime (

leanprover/lean4:v4.35.0

); otherwise

LeanBuild

warns, since

LeanImport

cannot load the result.

Examples

(2)

Basic Examples

(1)

Build a module of a small Lake project, then import it:

In[1]:=

dir=CreateDirectory[];Export[FileNameJoin[{dir,"lakefile.toml"}],{"name = \"demo\"","[[lean_lib]]","name = \"Demo\""},"Lines"];Export[FileNameJoin[{dir,"lean-toolchain"}],"leanprover/lean4:v4.35.0","Text"];Export[FileNameJoin[{dir,"Demo.lean"}],"theorem two_eq : 1 + 1 = 2 := rfl","Text"];