leantar is very slow when .lake directory is on nfs network

[tobiasgrosser]

leantar seems to be not very efficient in its filesystem usage, which slows it down when running on an NFS mount. Instead of 10 seconds, a mathlib lake exe cache get takes over two minutes. Some major inefficiencies seem to be:

• use of io:write instead of buffered writes
• redundant querying of directories

Here an strace snippet.

[pid  2544] write(4, "lse {\n lean_dec_ref(x_5152);\n x_"..., 7470) = 7470
[pid  2544] write(4, ");\nlean_dec(x_6);\nlean_dec(x_5);"..., 8192) = 8192
[pid  2544] write(4, "0);\n}\nlean_ctor_set(x_11, 0, x_6"..., 8192) = 8192
[pid  2544] write(4, "(x_118, 1);\nlean_inc(x_134);\nif "..., 8192) = 8192
[pid  2544] write(4, "tor_set(x_3, 0, x_1);\nlean_ctor_"..., 8192) = 8192
[pid  2544] write(4, "_13 = l_Lean_instantiateMVars___"..., 7916) = 7916
[pid  2544] write(4, "om_bytes(\"=>\", 2);\nreturn x_1;\n}"..., 8192) = 8192
[pid  2544] write(4, "ject* x_49; \nx_47 = lean_ctor_ge"..., 8192) = 8192
[pid  2544] write(4, "(x_4);\nlean_dec(x_3);\nlean_dec(x"..., 4034) = 4034
[pid  2544] write(4, "__closed__2;\nx_2 = lean_unsigned"..., 8192) = 8192
[pid  2544] write(4, "s(builtin, lean_io_mk_world());\n"..., 8192) = 8192
[pid  2544] write(4, "ic_PushNeg_transformNegationStep"..., 1686) = 1686
[pid  2544] write(4, "7 = _init_l_Mathlib_Tactic_PushN"..., 8192) = 8192
[pid  2544] write(4, "losed__55();\nlean_mark_persisten"..., 8192) = 8192
[pid  2544] write(4, "actic_PushNeg_tacticPush__neg___"..., 4672) = 4672
[pid  2544] munmap(0x7f28a4086000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a406e000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "./.lake/build/ir/Mathlib/Tactic/"..., 8192) = 56
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Tactic", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/Tactic", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/ir/Mathlib/Tactic/PushNeg.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "3435227558959846131", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "", 8192)           = 0
[pid  2544] munmap(0x7f28a3f9b000, 487424) = 0
[pid  2544] munmap(0x7f28a40f4000, 28672) = 0
[pid  2544] munmap(0x7f28a40a7000, 86016) = 0
[pid  2544] madvise(0x7f28a40ff000, 4096, MADV_FREE) = 0
[pid  2544] close(3)                    = 0
[pid  2544] open("/home/tcg40/.cache/mathlib/62613bacc64ec046.ltar", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
[pid  2544] fcntl(3, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] read(3, "LTAR\2056\217ff:\352\240./.lake/build/lib/Ma"..., 8192) = 4653
[pid  2544] open("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid/Basic.trace", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = -1 ENOENT (No such file or directory)
[pid  2544] mkdir("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid/Basic.trace", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "11595144402100500101", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mmap(NULL, 28672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f4000
[pid  2544] mmap(NULL, 486270, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3f9b000
[pid  2544] mkdir("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f3000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a4000
[pid  2544] open("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid/Basic.olean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] mmap(NULL, 53248, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4097000
[pid  2544] mmap(NULL, 8192, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f1000
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a40a4000, 98304) = 0
[pid  2544] munmap(0x7f28a40f1000, 8192) = 0
[pid  2544] write(4, "olean\1dcccfb73cb247e9478220375ab"..., 50016) = 50016
[pid  2544] munmap(0x7f28a4097000, 53248) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid/Basic.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "1802707849272209310", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid/Basic.ilean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "{\"version\":3,\"references\":{\"{\\\"c"..., 2520) = 2520
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid/Basic.ilean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "9103878379656972136", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/CategoryTheory/Groupoid/Basic.log.json", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "[{\"message\":\n  \".> LEAN_PATH=./."..., 769) = 769
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/CategoryTheory/Groupoid", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/CategoryTheory/Groupoid", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/ir/Mathlib/CategoryTheory/Groupoid/Basic.c", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "// Lean compiler output\n// Modul"..., 1528) = 1528
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/CategoryTheory/Groupoid", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/CategoryTheory/Groupoid", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/ir/Mathlib/CategoryTheory/Groupoid/Basic.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "3457069701603641635", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "", 8192)           = 0
[pid  2544] munmap(0x7f28a3f9b000, 487424) = 0
[pid  2544] munmap(0x7f28a40f4000, 28672) = 0
[pid  2544] munmap(0x7f28a40f3000, 4096) = 0
[pid  2544] madvise(0x7f28a40ff000, 4096, MADV_FREE) = 0
[pid  2544] close(3)                    = 0
[pid  2544] open("/home/tcg40/.cache/mathlib/88d9c7407c8faf84.ltar", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
[pid  2544] fcntl(3, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] read(3, "LTAR\1\362\367\264Sd+\365./.lake/build/lib/Ma"..., 8192) = 8192
[pid  2544] open("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule/Norm.trace", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = -1 ENOENT (No such file or directory)
[pid  2544] mkdir("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule/Norm.trace", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "17666324273972113921", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mmap(NULL, 28672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f4000
[pid  2544] mmap(NULL, 486270, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3f9b000
[pid  2544] mkdir("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f0000
[pid  2544] read(3, "\33\360\23\303;\24\2339G\272\353Z v\230\227\227\1\363\221\204,k\20\202\362\313|\33\3312\t"..., 8192) = 8192
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a4000
[pid  2544] open("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule/Norm.olean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] mmap(NULL, 318788, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3ed8000
[pid  2544] mmap(NULL, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ec000
[pid  2544] munmap(0x7f28a40ec000, 16384) = 0
[pid  2544] mmap(NULL, 20480, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40eb000
[pid  2544] madvise(0x7f28a40ff000, 4096, MADV_FREE) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a40a4000, 98304) = 0
[pid  2544] munmap(0x7f28a40eb000, 20480) = 0
[pid  2544] write(4, "olean\1dcccfb73cb247e9478220375ab"..., 318768) = 318768
[pid  2544] munmap(0x7f28a3ed8000, 319488) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule/Norm.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "6139352895691670367", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] read(3, "\343\233'\246\23C\245\0160\254\37\30\nS\216\333\300\234\373{_\376\336o\340;\276Y\16\337W\273"..., 8192) = 2631
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule/Norm.ilean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "{\"version\":3,\"references\":{\"{\\\"c"..., 8192) = 8192
[pid  2544] write(4, "effs\\\",\\\"m\\\":\\\"Mathlib.LinearAlg"..., 5247) = 5247
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule/Norm.ilean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "8431209901306686581", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/LinearAlgebra/FreeModule/Norm.log.json", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "[{\"message\":\n  \".> LEAN_PATH=./."..., 769) = 769
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/LinearAlgebra/FreeModule", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/LinearAlgebra/FreeModule", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/ir/Mathlib/LinearAlgebra/FreeModule/Norm.c", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "// Lean compiler output\n// Modul"..., 1540) = 1540
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/LinearAlgebra/FreeModule", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/LinearAlgebra/FreeModule", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/ir/Mathlib/LinearAlgebra/FreeModule/Norm.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "16532589874570378081", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "", 8192)           = 0
[pid  2544] munmap(0x7f28a3f9b000, 487424) = 0
[pid  2544] munmap(0x7f28a40f4000, 28672) = 0
[pid  2544] munmap(0x7f28a40f0000, 16384) = 0
[pid  2544] madvise(0x7f28a4101000, 4096, MADV_FREE) = 0
[pid  2544] close(3)                    = 0
[pid  2544] open("/home/tcg40/.cache/mathlib/ac9652b5ed3772f7.ltar", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
[pid  2544] fcntl(3, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] read(3, "LTARm\6Q\212\374\267\262\214./.lake/build/lib/Ma"..., 8192) = 6394
[pid  2544] open("././.lake/build/lib/Mathlib/Algebra/Ring/Semiconj.trace", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = -1 ENOENT (No such file or directory)
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Algebra/Ring", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Algebra/Ring", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Algebra/Ring/Semiconj.trace", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "10138368006444615277", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mmap(NULL, 28672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f4000
[pid  2544] mmap(NULL, 486270, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3f9b000
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Algebra/Ring", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Algebra/Ring", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f3000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a4000
[pid  2544] open("././.lake/build/lib/Mathlib/Algebra/Ring/Semiconj.olean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] mmap(NULL, 81920, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4090000
[pid  2544] mmap(NULL, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ef000
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a40a4000, 98304) = 0
[pid  2544] munmap(0x7f28a40ef000, 16384) = 0
[pid  2544] write(4, "olean\1dcccfb73cb247e9478220375ab"..., 79512) = 79512
[pid  2544] munmap(0x7f28a4090000, 81920) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Algebra/Ring", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Algebra/Ring", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Algebra/Ring/Semiconj.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "3452588565034128634", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Algebra/Ring", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Algebra/Ring", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/Algebra/Ring/Semiconj.ilean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "{\"version\":3,\"references\":{\"{\\\"c"..., 6581) = 6581
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Algebra/Ring", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Algebra/Ring", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Algebra/Ring/Semiconj.ilean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "15968027506446588116", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Algebra/Ring", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Algebra/Ring", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/Algebra/Ring/Semiconj.log.json", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "[{\"message\":\n  \".> LEAN_PATH=./."..., 737) = 737
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Algebra/Ring", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/Algebra/Ring", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/ir/Mathlib/Algebra/Ring/Semiconj.c", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "// Lean compiler output\n// Modul"..., 1497) = 1497
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Algebra/Ring", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/Algebra/Ring", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/ir/Mathlib/Algebra/Ring/Semiconj.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "11088323786201423125", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "", 8192)           = 0
[pid  2544] munmap(0x7f28a3f9b000, 487424) = 0
[pid  2544] munmap(0x7f28a40f4000, 28672) = 0
[pid  2544] munmap(0x7f28a40f3000, 4096) = 0
[pid  2544] madvise(0x7f28a40ff000, 4096, MADV_FREE) = 0
[pid  2544] close(3)                    = 0
[pid  2544] open("/home/tcg40/.cache/mathlib/c8a0d61581ce2888.ltar", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
[pid  2544] fcntl(3, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] read(3, "LTAR\"A\210\272t\274\272\374./.lake/build/lib/Ma"..., 8192) = 8192
[pid  2544] open("././.lake/build/lib/Mathlib/Topology/Compactification/OnePoint.trace", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = -1 ENOENT (No such file or directory)
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Topology/Compactification", 0777) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Topology/Compactification/OnePoint.trace", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "18211075252757741858", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mmap(NULL, 28672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f4000
[pid  2544] mmap(NULL, 486270, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3f9b000
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Topology/Compactification", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Topology/Compactification", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 32768, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ec000
[pid  2544] read(3, "\332\365{o&\205l\362\"e\347\37n?\367v\352\345BD\367\r\203JUB\306\336\300\v\235\305"..., 21064) = 21064
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a4000
[pid  2544] open("././.lake/build/lib/Mathlib/Topology/Compactification/OnePoint.olean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] mmap(NULL, 499756, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3eab000
[pid  2544] mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40eb000
[pid  2544] mmap(NULL, 8192, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40e4000
[pid  2544] munmap(0x7f28a40eb000, 4096) = 0
[pid  2544] mmap(NULL, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a0000
[pid  2544] munmap(0x7f28a40a0000, 16384) = 0
[pid  2544] mmap(NULL, 20480, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409f000
[pid  2544] madvise(0x7f28a40ff000, 4096, MADV_FREE) = 0
[pid  2544] mmap(NULL, 36864, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4096000
[pid  2544] munmap(0x7f28a409f000, 20480) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a40a4000, 98304) = 0
[pid  2544] munmap(0x7f28a4096000, 36864) = 0
[pid  2544] munmap(0x7f28a40e4000, 8192) = 0
[pid  2544] write(4, "olean\1dcccfb73cb247e9478220375ab"..., 499736) = 499736
[pid  2544] munmap(0x7f28a3eab000, 503808) = 0
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "./.lake/build/lib/Mathlib/Topolo"..., 8192) = 8192
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Topology/Compactification", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Topology/Compactification", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Topology/Compactification/OnePoint.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "14606761143606316903", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Topology/Compactification", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Topology/Compactification", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] read(3, "\205\t$\262K\r\316\250\326\26\307\222h\275XdT[l\341#\203\211}\302$.Iq\220~\271"..., 8192) = 3532
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/Topology/Compactification/OnePoint.ilean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "{\"version\":3,\"references\":{\"{\\\"c"..., 8192) = 8192
[pid  2544] write(4, "efinition\":null},\"{\\\"c\\\":{\\\"n\\\":"..., 8192) = 8192
[pid  2544] write(4, "instTopologicalSpace\",185,0,201,"..., 8192) = 8192
[pid  2544] write(4, "isOpen_range_coe\",274,0,275,32,2"..., 8192) = 8192
[pid  2544] write(4, "lib.Topology.Compactification.On"..., 8192) = 8192
[pid  2544] write(4, "\"OnePoint.infinite\",81,0,82,39,8"..., 8192) = 8192
[pid  2544] write(4, ".Order.Heyting.Basic\\\"}}\":{\"usag"..., 8192) = 8192
[pid  2544] write(4, "\"c\\\":{\\\"n\\\":\\\"Filter.tendsto_map"..., 8192) = 8192
[pid  2544] write(4, "_coe\",397,0,398,46,397,8,397,23]"..., 6404) = 6404
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Topology/Compactification", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Topology/Compactification", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Topology/Compactification/OnePoint.ilean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "16588740904912602912", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Topology/Compactification", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Topology/Compactification", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/Topology/Compactification/OnePoint.log.json", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "[{\"message\":\n  \".> LEAN_PATH=./."..., 789) = 789
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Topology/Compactification", 0777) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/ir/Mathlib/Topology/Compactification/OnePoint.c", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "// Lean compiler output\n// Modul"..., 8192) = 8192
[pid  2544] write(4, ", x_3);\nreturn x_4;\n}\n}\nstatic l"..., 8192) = 8192
[pid  2544] write(4, "((void*)(l_OnePoint_instFintype_"..., 8192) = 8192
[pid  2544] write(4, "instCoeTC___closed__1();\nlean_ma"..., 295) = 295
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Topology/Compactification", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/Topology/Compactification", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/ir/Mathlib/Topology/Compactification/OnePoint.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "2034497151601112697", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "", 8192)           = 0
[pid  2544] munmap(0x7f28a3f9b000, 487424) = 0
[pid  2544] munmap(0x7f28a40f4000, 28672) = 0
[pid  2544] munmap(0x7f28a40ec000, 32768) = 0
[pid  2544] madvise(0x7f28a4101000, 4096, MADV_FREE) = 0
[pid  2544] close(3)                    = 0
[pid  2544] open("/home/tcg40/.cache/mathlib/0e205f11149fc3ec.ltar", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
[pid  2544] fcntl(3, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] read(3, "LTAR\374\314\376\7\356v\264\276.lake/packages/batte"..., 8192) = 3467
[pid  2544] open("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes/BEq.trace", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = -1 ENOENT (No such file or directory)
[pid  2544] mkdir("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes/BEq.trace", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "13741739127722659068", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mmap(NULL, 28672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f4000
[pid  2544] mmap(NULL, 486270, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3f9b000
[pid  2544] mkdir("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a4000
[pid  2544] open("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes/BEq.olean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] mmap(NULL, 36864, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40eb000
[pid  2544] mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ea000
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a40a4000, 98304) = 0
[pid  2544] munmap(0x7f28a40ea000, 4096) = 0
[pid  2544] write(4, "olean\1dcccfb73cb247e9478220375ab"..., 32880) = 32880
[pid  2544] munmap(0x7f28a40eb000, 36864) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes/BEq.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "16828809938514049720", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes/BEq.ilean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "{\"version\":3,\"references\":{\"{\\\"c"..., 654) = 654
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes/BEq.ilean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "9998139319454875553", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("./.lake/packages/batteries/.lake/build/lib/Batteries/Classes/BEq.log.json", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "[{\"message\":\n  \".> LEAN_PATH=./."..., 810) = 810
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("./.lake/packages/batteries/.lake/build/ir/Batteries/Classes", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("./.lake/packages/batteries/.lake/build/ir/Batteries/Classes", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("./.lake/packages/batteries/.lake/build/ir/Batteries/Classes/BEq.c", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "// Lean compiler output\n// Modul"..., 959) = 959
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("./.lake/packages/batteries/.lake/build/ir/Batteries/Classes", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("./.lake/packages/batteries/.lake/build/ir/Batteries/Classes", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("./.lake/packages/batteries/.lake/build/ir/Batteries/Classes/BEq.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "8047277692801181038", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "", 8192)           = 0
[pid  2544] munmap(0x7f28a3f9b000, 487424) = 0
[pid  2544] munmap(0x7f28a40f4000, 28672) = 0
[pid  2544] madvise(0x7f28a40ff000, 4096, MADV_FREE) = 0
[pid  2544] close(3)                    = 0
[pid  2544] open("/home/tcg40/.cache/mathlib/1f5bdef9d4b1a032.ltar", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
[pid  2544] fcntl(3, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] read(3, "LTAR\332\177\377Z\275o\240\220./.lake/build/lib/Ma"..., 8192) = 8192
[pid  2544] open("././.lake/build/lib/Mathlib/Data/Nat/Cast/Field.trace", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = -1 ENOENT (No such file or directory)
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Data/Nat/Cast", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Data/Nat/Cast", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Data/Nat/Cast/Field.trace", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "10421452396801523674", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mmap(NULL, 28672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f4000
[pid  2544] mmap(NULL, 486270, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3f9b000
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Data/Nat/Cast", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Data/Nat/Cast", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 8192, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f2000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a4000
[pid  2544] open("././.lake/build/lib/Mathlib/Data/Nat/Cast/Field.olean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] mmap(NULL, 131072, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4084000
[pid  2544] mmap(NULL, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ee000
[pid  2544] munmap(0x7f28a40ee000, 16384) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a40a4000, 98304) = 0
[pid  2544] madvise(0x7f28a40ff000, 4096, MADV_FREE) = 0
[pid  2544] write(4, "olean\1dcccfb73cb247e9478220375ab"..., 129848) = 129848
[pid  2544] munmap(0x7f28a4084000, 131072) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Data/Nat/Cast", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Data/Nat/Cast", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Data/Nat/Cast/Field.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "14517944822514754731", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Data/Nat/Cast", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Data/Nat/Cast", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] read(3, "\344\233g\317^C\6\300)-\247\0\23\331\20\315\363\3724.\356\203\205\304\237Czi\25\276\363\265"..., 8192) = 1388
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/Data/Nat/Cast/Field.ilean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "{\"version\":3,\"references\":{\"{\\\"c"..., 7236) = 7236
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Data/Nat/Cast", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Data/Nat/Cast", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Data/Nat/Cast/Field.ilean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "1713791321975731806", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Data/Nat/Cast", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Data/Nat/Cast", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/Data/Nat/Cast/Field.log.json", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "[{\"message\":\n  \".> LEAN_PATH=./."..., 729) = 729
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Data/Nat/Cast", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/Data/Nat/Cast", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/ir/Mathlib/Data/Nat/Cast/Field.c", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "// Lean compiler output\n// Modul"..., 2003) = 2003
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Data/Nat/Cast", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/Data/Nat/Cast", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/ir/Mathlib/Data/Nat/Cast/Field.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "17284979658508345768", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "", 8192)           = 0
[pid  2544] munmap(0x7f28a3f9b000, 487424) = 0
[pid  2544] munmap(0x7f28a40f4000, 28672) = 0
[pid  2544] munmap(0x7f28a40f2000, 8192) = 0
[pid  2544] madvise(0x7f28a4101000, 4096, MADV_FREE) = 0
[pid  2544] close(3)                    = 0
[pid  2544] open("/home/tcg40/.cache/mathlib/f4d1635444df8826.ltar", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
[pid  2544] fcntl(3, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] read(3, "LTAR%\237\205\247h^\302\344./.lake/build/lib/Ma"..., 8192) = 8192
[pid  2544] open("././.lake/build/lib/Mathlib/Order/Bounded.trace", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = -1 ENOENT (No such file or directory)
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Order", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Order", {st_mode=S_IFDIR|0775, st_size=12288, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Order/Bounded.trace", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "16483841389709598501", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mmap(NULL, 28672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f4000
[pid  2544] mmap(NULL, 486270, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3f9b000
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Order", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Order", {st_mode=S_IFDIR|0775, st_size=12288, ...}) = 0
[pid  2544] mmap(NULL, 20480, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ef000
[pid  2544] read(3, "\24\235Q\357\242\177\273%\366tZ'\\\330\346\3004\31#p\7\22{\33G\300\242\205V(\27\363"..., 8384) = 8384
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a4000
[pid  2544] open("././.lake/build/lib/Mathlib/Order/Bounded.olean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] mmap(NULL, 343812, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3ed2000
[pid  2544] mmap(NULL, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40eb000
[pid  2544] munmap(0x7f28a40eb000, 16384) = 0
[pid  2544] mmap(NULL, 20480, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ea000
[pid  2544] madvise(0x7f28a4101000, 4096, MADV_FREE) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a40a4000, 98304) = 0
[pid  2544] munmap(0x7f28a40ea000, 20480) = 0
[pid  2544] write(4, "olean\1dcccfb73cb247e9478220375ab"..., 343792) = 343792
[pid  2544] munmap(0x7f28a3ed2000, 344064) = 0
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "./.lake/build/lib/Mathlib/Order/"..., 8192) = 6560
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Order", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Order", {st_mode=S_IFDIR|0775, st_size=12288, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Order/Bounded.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "5478690150042757764", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Order", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Order", {st_mode=S_IFDIR|0775, st_size=12288, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/Order/Bounded.ilean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "{\"version\":3,\"references\":{\"{\\\"c"..., 8192) = 8192
[pid  2544] write(4, ",\"{\\\"c\\\":{\\\"n\\\":\\\"Set.unbounded_"..., 8192) = 8192
[pid  2544] write(4, "1]],\"definition\":[300,8,300,25]}"..., 8192) = 8192
[pid  2544] write(4, "unded_lt_Ioo\",210,0,211,49,210,8"..., 8192) = 8192
[pid  2544] write(4, "2,55,\"Set.bounded_ge_Ioc\",262,0,"..., 8192) = 8192
[pid  2544] write(4, "}}\":{\"usages\":[[156,34,156,44,\"S"..., 3246) = 3246
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Order", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Order", {st_mode=S_IFDIR|0775, st_size=12288, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Order/Bounded.ilean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "8853050875326108960", 19) = 19
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Order", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Order", {st_mode=S_IFDIR|0775, st_size=12288, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/lib/Mathlib/Order/Bounded.log.json", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "[{\"message\":\n  \".> LEAN_PATH=./."..., 705) = 705
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Order", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/Order", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 131095, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a409b000
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a4083000
[pid  2544] open("././.lake/build/ir/Mathlib/Order/Bounded.c", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] write(4, "// Lean compiler output\n// Modul"..., 1469) = 1469
[pid  2544] munmap(0x7f28a409b000, 135168) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a4083000, 98304) = 0
[pid  2544] close(4)                    = 0
[pid  2544] mkdir("././.lake/build/ir/Mathlib/Order", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/ir/Mathlib/Order", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/ir/Mathlib/Order/Bounded.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "16726536706777008877", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "", 8192)           = 0
[pid  2544] munmap(0x7f28a3f9b000, 487424) = 0
[pid  2544] munmap(0x7f28a40f4000, 28672) = 0
[pid  2544] munmap(0x7f28a40ef000, 20480) = 0
[pid  2544] madvise(0x7f28a40ff000, 4096, MADV_FREE) = 0
[pid  2544] close(3)                    = 0
[pid  2544] open("/home/tcg40/.cache/mathlib/f51135fb07991089.ltar", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
[pid  2544] fcntl(3, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] read(3, "LTAR\362G\316\354i\210\357\336./.lake/build/lib/Ma"..., 8192) = 8192
[pid  2544] open("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition/Tagged.trace", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = -1 ENOENT (No such file or directory)
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition/Tagged.trace", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] write(4, "16064208384379734002", 20) = 20
[pid  2544] close(4)                    = 0
[pid  2544] mmap(NULL, 28672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40f4000
[pid  2544] mmap(NULL, 486270, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3f9b000
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] mmap(NULL, 24576, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ee000
[pid  2544] read(3, "\312\352\264\250,v\340<=\320.\363\347\20pb\377\333\221H^\335q\1783o\274z\362%\220"..., 14449) = 14449
[pid  2544] mmap(NULL, 98304, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40a4000
[pid  2544] open("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition/Tagged.olean", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4
[pid  2544] fcntl(4, F_SETFD, FD_CLOEXEC) = 0
[pid  2544] mmap(NULL, 8781908, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a319c000
[pid  2544] mmap(NULL, 416876, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a3ec0000
[pid  2544] mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40ed000
[pid  2544] mmap(NULL, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40e2000
[pid  2544] munmap(0x7f28a40e2000, 16384) = 0
[pid  2544] mmap(NULL, 20480, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f28a40e1000
[pid  2544] madvise(0x7f28a4101000, 4096, MADV_FREE) = 0
[pid  2544] munmap(0x7f28a40ed000, 4096) = 0
[pid  2544] munmap(0x7f28a319c000, 8785920) = 0
[pid  2544] munmap(0x7f28a40a4000, 98304) = 0
[pid  2544] munmap(0x7f28a40e1000, 20480) = 0
[pid  2544] write(4, "olean\1dcccfb73cb247e9478220375ab"..., 416856) = 416856
[pid  2544] munmap(0x7f28a3ec0000, 417792) = 0
[pid  2544] close(4)                    = 0
[pid  2544] read(3, "./.lake/build/lib/Mathlib/Analys"..., 8192) = 8192
[pid  2544] mkdir("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition", 0777) = -1 EEXIST (File exists)
[pid  2544] stat("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0
[pid  2544] open("././.lake/build/lib/Mathlib/Analysis/BoxIntegral/Partition/Tagged.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_LARGEFILE|O_CLOEXEC, 0666) = 4

[digama0]

I don't see evidence that it's not doing buffered writes in that log. AFAIK it is buffering writes, which is why the writes there have sizes like 4096 or 8192.

As for redundant file ops, this seems likely, although (1) I'm not sure how much control rust actually gives over doing those operations more economically without significantly complicating things and (2) I'd like to confirm that these extra stat calls are actually causing the problem. Do you know if tar performs significantly better in this situation than leantar?

Note that there is some known slowness, especially on Windows, which is due mainly to the way Windows handles file system operations and is equally bad in all programs that create many files. Two minutes is not out of the realm of possibility AFAIK. See "NTFS really isn't that bad" - Robert Collins (LCA 2020).

[digama0]

I made some modifications in bf72a45 which should decrease the number of calls to mkdir and stat on directories that already exist. On my machine the strace looks like this now:

openat(AT_FDCWD, "/home/mario/.cache/mathlib/01ab41acd110bb6b.ltar", O_RDONLY|O_CLOEXEC) = 3
read(3, "LTAR\375~\316\3767R\332\34./.lake/build/lib/Ma"..., 8192) = 2317
openat(AT_FDCWD, "././.lake/build/lib/Mathlib/Data/Rbtree/Insert.trace", O_RDONLY|O_CLOEXEC) = -1 ENOENT (No such file or directory)
mkdir("././.lake/build/lib/Mathlib/Data/Rbtree", 0777) = -1 ENOENT (No such file or directory)
mkdir("././.lake/build/lib/Mathlib/Data", 0777) = -1 ENOENT (No such file or directory)
mkdir("././.lake/build/lib/Mathlib", 0777) = -1 ENOENT (No such file or directory)
mkdir("././.lake/build/lib", 0777)      = -1 ENOENT (No such file or directory)
mkdir("././.lake/build", 0777)          = -1 ENOENT (No such file or directory)
mkdir("././.lake", 0777)                = 0
mkdir("././.lake/build", 0777)          = 0
mkdir("././.lake/build/lib", 0777)      = 0
mkdir("././.lake/build/lib/Mathlib", 0777) = 0
mkdir("././.lake/build/lib/Mathlib/Data", 0777) = 0
mkdir("././.lake/build/lib/Mathlib/Data/Rbtree", 0777) = 0
openat(AT_FDCWD, "././.lake/build/lib/Mathlib/Data/Rbtree/Insert.trace", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 4
write(4, "2079064578436529917", 19)     = 19
close(4)                                = 0
mmap(NULL, 487424, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x787001e7b000
brk(0x5bb5cbbda000)                     = 0x5bb5cbbda000
openat(AT_FDCWD, "././.lake/build/lib/Mathlib/Data/Rbtree/Insert.olean", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 4
mmap(NULL, 8785920, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x786ffb79f000
munmap(0x786ffb79f000, 8785920)         = 0
write(4, "olean\1dcccfb73cb247e9478220375ab"..., 15112) = 15112
close(4)                                = 0
openat(AT_FDCWD, "././.lake/build/lib/Mathlib/Data/Rbtree/Insert.olean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 4
write(4, "5129390526386888840", 19)     = 19
close(4)                                = 0
brk(0x5bb5cbbfe000)                     = 0x5bb5cbbfe000
openat(AT_FDCWD, "././.lake/build/lib/Mathlib/Data/Rbtree/Insert.ilean", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 4
brk(0x5bb5cc45e000)                     = 0x5bb5cc45e000
write(4, "{\"version\":3,\"references\":{},\"mo"..., 67) = 67
close(4)                                = 0
openat(AT_FDCWD, "././.lake/build/lib/Mathlib/Data/Rbtree/Insert.ilean.hash", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 4
write(4, "14815318170663550241", 20)    = 20
close(4)                                = 0
openat(AT_FDCWD, "././.lake/build/lib/Mathlib/Data/Rbtree/Insert.log.json", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 4
write(4, "[{\"message\":\n  \".> LEAN_PATH=./."..., 725) = 725
close(4)                                = 0
mkdir("././.lake/build/ir/Mathlib/Data/Rbtree", 0777) = -1 ENOENT (No such file or directory)
mkdir("././.lake/build/ir/Mathlib/Data", 0777) = -1 ENOENT (No such file or directory)
mkdir("././.lake/build/ir/Mathlib", 0777) = -1 ENOENT (No such file or directory)
mkdir("././.lake/build/ir", 0777)       = 0
mkdir("././.lake/build/ir/Mathlib", 0777) = 0
mkdir("././.lake/build/ir/Mathlib/Data", 0777) = 0
mkdir("././.lake/build/ir/Mathlib/Data/Rbtree", 0777) = 0
openat(AT_FDCWD, "././.lake/build/ir/Mathlib/Data/Rbtree/Insert.c", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 4
write(4, "// Lean compiler output\n// Modul"..., 1209) = 1209
close(4)                                = 0
openat(AT_FDCWD, "././.lake/build/ir/Mathlib/Data/Rbtree/Insert.c.hash", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 4
write(4, "16678743707097875166", 20)    = 20
close(4)                                = 0
read(3, "", 8192)                       = 0
munmap(0x787001e7b000, 487424)          = 0
close(3)                                = 0

Note also that all of the (small) files here are written using single large writes, so I don't see how this can be improved unless you think another syscall besides write would perform better.