Storing FloatArray?

Stream: lean4

[Siddhartha Gadgil]

What is an efficient way to store a bunch (about 9000) of FloatArray's to a file (or to files) from Lean (to load in Lean)?

Thanks.

[Arthur Paulino]

Probably an unpopular idea: do it in C via FFI. You can just dump the bytes and read them later

[Siddhartha Gadgil]

Only unpopular with me because I have low confidence in my FFI abilities (I am a mathematician, not a computer scientist).

[Sebastian Ullrich]

There is no need for that, use the .olean format via e.g. docs#pickle and you have the same reasonably compact layout as in memory