Zulip Chat Archive
Stream: general
Topic: lean hangs
Floris van Doorn (Jan 24 2019 at 00:13):
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 (Jan 24 2019 at 08:45):
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 (Jan 24 2019 at 08:46):
I just kill it in Task Manager because it's always the one occupying the most memory
Last updated: Dec 20 2023 at 11:08 UTC