L4YAML

6.1. Recommended Build🔗

cmake -B build -S . -DL4YAML_BUILD_RUST=ON
cmake --build build -j
cmake --install build --prefix /path/to/stage

The --install step is optional; it stages the artifacts into a standard ${prefix}/{bin,lib,include} layout plus the compiled Lean module tree under ${prefix}/lib/lean/.

The build produces, in order:

  • The Lean library, proof modules, compile-time guards, and every executable in the L4YAML_EXES list (a superset of the defaultTargets from lakefile.toml), driven by lake build.

  • libl4yaml.so and the C example tryparse_c, defined in ffi/CMakeLists.txt.

  • The Rust workspace (l4yaml-sys, l4yaml) and the tryparse_rs example, driven by cargo build --release --workspace --examples.

The installed C and Rust binaries have RPATHs that resolve libl4yaml.so via $ORIGIN/../lib and libleanshared.so from the Lean toolchain, so they work directly out of the install tree.