Let us say I have a text file of a million lines, and I want to cut
it into smaller (10K lines) ones.
How to do this? I have tried a few ways, none I think is lazy (I
mean not reading the file all at the start).