`lake exe fp-lean` fails with `error: FPLean/MonadTransformers/Do.lean:356:0: Mismatched commands output:`

[DacrydiumGracile]

Hello. I encountered several problems while compiling the book.

1. lake exe fp-lean fails with bash: doug: command not found and Non-zero exit code from 'sort --shared < test-data' #191
   And the suggested solution helped with this error.

2. However, the following error occurred:

✖ [340/348] Building FPLean.MonadTransformers.Do
trace: .> LEAN_PATH= ...

error: FPLean/MonadTransformers/Do.lean:356:0: Mismatched commands output:
  $ ls
  expected
  test-data
  $ cp ../ForMIO.lean .
  $ ls
- ForMIO.lean
  expected
+ ForMIO.lean
  test-data
 


Hint: Replace with actual value
  $ ls
  expected
  test-data
  $ cp ../ForMIO.lean .
  $ ls
  e̲x̲p̲e̲c̲t̲e̲d̲
  ̲ForMIO.lean
  e̵x̵p̵e̵c̵ted̵
  ̵t̵e̵st-data
error: Lean exited with code 1
Some required builds logged failures:
- FPLean.MonadTransformers.Do
error: build failed

If you take the advice and change

$ ls
ForMIO.lean
expected
test-data

to

$ ls
expected
ForMIO.lean
test-data

then this error will disappear.

3. However, another error can occur:

✖ [340/348] Building FPLean.MonadTransformers.Do
trace: .> LEAN_PATH= ...

error: FPLean/MonadTransformers/Do.lean:167:0: resource exhausted (error code: 28, no space left on device)
error: FPLean/MonadTransformers/Do.lean:175:0: resource exhausted (error code: 28, no space left on device)
error: FPLean/MonadTransformers/Do.lean:181:0: resource exhausted (error code: 28, no space left on device)
error: FPLean/MonadTransformers/Do.lean:259:46: resource exhausted (error code: 28, no space left on device)
error: FPLean/MonadTransformers/Do.lean:324:0: resource exhausted (error code: 28, no space left on device)
error: FPLean/MonadTransformers/Do.lean:343:0: resource exhausted (error code: 28, no space left on device)
error: FPLean/MonadTransformers/Do.lean:355:0: resource exhausted (error code: 28, no space left on device)
error: FPLean/MonadTransformers/Do.lean:366:8: Not found: 'formio'
error: FPLean/MonadTransformers/Do.lean:375:0: resource exhausted (error code: 28, no space left on device)
error: FPLean/MonadTransformers/Do.lean:761:55: resource exhausted (error code: 28, no space left on device)
error: Lean exited with code 1
Some required builds logged failures:
- FPLean.MonadTransformers.Do
error: build failed

As far as I understood, this error is caused by the /tmp folder being full, because during the book building process, temporary files with a total size of several gigabytes are created in this folder. Therefore, before building, you should make sure that the allocated space for /tmp is sufficient.

After troubleshooting these issues, the build completed successfully.

Environment:

$ hostnamectl
Operating System: Arch Linux                        
          Kernel: Linux 6.15.2-arch1-1
    Architecture: x86-64

[david-christiansen]

Thanks for the report!

This happens because the build products from the examples are copied to a fresh temporary directory when testing the executables. I think a better fix here would be to use symlinks for the directories in question rather than copying them, or alternatively to split the example code project into small projects.