`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.

[Garmelon]

The issue causing error 2. is that the ls sort order is locale dependent. On my machine, it behaves like this:

$ ls | cat
expected
ForMIO.lean
test-data

$ LC_ALL=C ls | cat
ForMIO.lean
expected
test-data

The test assumes that ls always behaves the same, which I'd consider broken. Ideally, at some point in the test suite, the locale is set to a fixed value.

[Garmelon]

Regarding error 3., I'd expect each test to remove the temporary directories again once it's finished with them, but the temp dirs appear to stick around and quickly fill up my tmpfs /tmp.

[david-christiansen]

I'd really like to find a good way to not fill up /tmp here. I don't have access to a feature in the Lean elaborator that lets me detect when elaboration is finished and go clean up, unfortunately. I can think of a few fragile solutions, like saving the temp directories to a file and then deleting the contents of the file at startup, but it seems a bit risky.

Any suggestions for a good way to go about this?

[satnam6502]

Hello. I get the same error when building on Mac OS X. I could try to locally apply the suggestion, but it would be good if things worked "out of the box"? Thank you kindly.

[david-christiansen]

OK, #229 should have fixed the sort order issue, and #230 the disk space one. It doesn't clean up after itself yet, but it at least only copies a few megabytes instead of 1,7 gigabytes.

Please let me know if there's still issues!

[satnam6502]

Works now! Thank you very much. Very useful on long flights.