cleaning your hard disk

Stream: lean4

[Kevin Buzzard]

Is this still a thing? I am expecting the answer "yes" and furthermore I am expecting it just to be a fact of life.

[Wojciech Nawrocki]

Yes, while the interfaces have changed the server will still execute whatever the user tells it to and potentially spawn arbitrary processes.

[Sebastian Ullrich]

Fun fact: this issue was created before people started happily curling elan into their shells