lean hangs

Stream: general

[Floris van Doorn]

I don't know if there is any place for bug reports for Lean 3, but Lean will hang on these two lines (and start to slowly fill up your memory):

notation S`[`:95 ϕ `]`:90 := 0
variables (α : Type) [add_group α]

(I am not implying that declaring this notation is a good idea)

On a related note: does someone know how to kill lean processes which are spawned by leanpkg build in msys2 on Windows? Killing the command with ctrl+C does not kill the Lean processes (which is a problem if they are busy filling up your memory).

[Neil Strickland]

You can use the commands taskkill and/or tasklist under cmd.exe. Specifically, taskkill /f /fi "imagename eq lean.exe" should do the job. Or you can open a new msys terminal window and use ps and kill as in Linux.

[Kenny Lau]

I just kill it in Task Manager because it's always the one occupying the most memory