Zulip Chat Archive
Stream: general
Topic: VSCode says busily processing...
Duncan Skahan (Oct 26 2024 at 15:53):
This is my first time using Lean. I'm trying to following Mathematics in Lean, but when I type something the Lean extension seems to freeze up and say "busily processing..."
Kevin Buzzard (Oct 27 2024 at 10:00):
Have you got a fully compiled mathlib? Can you compile your project on the command line?
Last updated: May 02 2025 at 03:31 UTC