building the book for offline reading is broken

[dimpase]

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?

[dimpase]

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 into book/.

One extra caveat is that expect needs to be installed for it to work.

I'll make a PR updating README with these details