Proof window not opening

[alexamadori]

Hey, I'm having a problem with the proof window not opening. If I remember correctly, a while ago, it used to open automatically as soon as I started writing the proof for a theorem. Now it just doesn't appear. Tried both vscode and cursor. Even if I use "Display proof view" from the cmd + P menu nothing happens.

[TheoWinterhalter]

Isn't it a duplicate of #821?
Have you tried "Coq: Interpret to point" or any command that is supposed to interpret the file?
Since #788, the default mode is manual.

[alexamadori]

This solution from #821 worked, thanks for the quick response!

Imo this is a bit confusing, in my case I didn't find #821 when I was googling this problem, probably because in my search I was calling the window "proof window" instead of something containing "goals". I think I would've had an easier time if there had been some kind of visual indication that the file wasn't being interpreted up to the open proof, but I'm not sure how I would do that.

[TheoWinterhalter]

I mean the README explains how to use the extension, and there is the navigation buttons now that should be a hint you can navigate manually.