Help Needed: Software Execution Issue of Lean4

Stream: mathlib4

[泡泡]

I'm encountering a problem while using Lean4 in combination with VS Code for theorem proving, and I'm now seeking help from everyone.

During the operation, I wrote Lean4 code following the regular steps and attempted to conduct theorem proving. However, the expected green checkmark symbol didn't appear, which means there was no feedback on the execution result. I have confirmed that the Lean4 extension in VS Code has been correctly installed, and all relevant dependencies have also been set up properly.

I have tried restarting VS Code, and even reinstalling the Lean4 extension and the related environment, but the problem still persists. Currently, I'm not sure whether there is a logical error in the code or there are some omissions in the environment configuration.

[Kyle Miller]

If you run the command lake build from the root of your project, do you get any feedback?

[Maja Kądziołka]

If you make an intentional error, do you get notified of it?