Repository navigation
building the book for offline reading is broken #283
Description
cd book && lake exe fp-lean always breaks down with something missing in ../examples/, like
✖ [144/233] Running exampleBinaries
error: no such file or directory (error code: 2)
file: <WHATEVER>/fp-lean/book/../examples/.lake/build/bin
This is on Linux, with ~/.elan/ already populated via VSCode, and working Lean in VSCode.
Further, lake exe fp-lean downloads newer versions of Lean (acurally, different ones) for the reason I don't understand. Shouldn't it be using the one installed?
Activity
dimpase commentedon Jul 25, 2026
I am able to build the book following steps in the CI script, where first one runs a build in
examples/, and only then goes intobook/.One extra caveat is that
expectneeds to be installed for it to work.I'll make a PR updating README with these details