search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.69k stars 233 forks source link

FStar.IO could do with a flush #3496

Open briangmilnes opened 1 month ago

briangmilnes commented 1 month ago

For testing, I write log files then read them and do a string compare to the expected. Useful for things like running external but small tests. It would be good to have the write log flushed before reading.

FStar.Unix the new wrapper I've finished (but not merged) has flush of course. Should we make a flush in FStar.IO so that we can call it in fstar/rst/fsharp/c?

briangmilnes commented 1 month ago

OCaml unix alas does not provide an O_TMPFILE flag to openfile. So we could do with a random, a tmpfile addition and a file delete in FStar.IO. I'll build them if approved.