I/O and Processes🔗

This chapter covers various topics related to I/O and processes, threads and concurrency in Lean. Lean has great support for running tasks concurrently and provides a powerful API for handling I/O operations. We use the IO monad to perform our operations.

In Lean, it is important to understand the difference in Process, Threads and Tasks. When you spawn a child process, Lean gives you a handle to the OS process. When you spawn an internal computation, Lean gives you a Task. Hence Task is not a schedulable entity at the OS level.

Recipes:

1. Handling Stdin/Stdout/Stderr Streams
2. Parsing Command Line Arguments
3. Spawning a Child Process
4. Spawning Tasks and Worker Threads
5. Running Tasks in Parallel
6. Putting a Process to Sleep
7. Process Interruption and Idle Sleep
8. Time Measurement of Process
9. Miscellaneous IO