`lake exe fp-lean` fails with `bash: doug: command not found` and `Non-zero exit code from 'sort --shared < test-data'`

[euprunin]

lake exe fp-lean fails with bash: doug: command not found and Non-zero exit code from 'sort --shared < test-data':

% git clone https://github.com/leanprover/fp-lean
% cd fp-lean
% lake exe fp-lean
✖ [336/348] Building FPLean.MonadTransformers.ReaderIO
error: FPLean/MonadTransformers/ReaderIO.lean:31:0: Non-zero exit code from 'doug' (127).
  Stdout:
  Stderr:
    bash: doug: command not found
error: Lean exited with code 1
✖ [340/348] Building FPLean.ProgramsProofs.InsertionSort
error: FPLean/ProgramsProofs/InsertionSort.lean:785:0: Mismatched commands output:
  $ expect -f ./run-usage # sort
- Expected single argument, either "--shared" or "--unique"
…
error: FPLean/ProgramsProofs/InsertionSort.lean:818:0: Non-zero exit code from 'sort --shared < test-data' (2).

Environment:

% sw_vers
ProductName:		macOS
ProductVersion:		15.1.1
BuildVersion:		24B2091
% which doug
doug not found
% which sort
/usr/bin/sort

[zipfried]

After checking .github/workflows/ci.yml, I found that running lake build and lake build subverso-extract-mod in the examples directory, then lake exe fp-lean in the book directory, resolves the issue.

[euprunin]

@zipfried Thanks! This seems to be working:

% git clone https://github.com/leanprover/fp-lean
% cd fp-lean/
% cd examples/
% lake build
% lake build subverso-extract-mod
% cd ../book/
% lake exe fp-lean
% open _out/html-multi/index.html

[euprunin]

Suggested fix in: https://github.com/leanprover/fp-lean/issues/197