Where is the Lean Server Error Log?

Stream: new members

[Arthur Ryman]

I was editing a lean file in VS Code when an error message popped up, something like "Lean Server quit ...". It had a "Restart Server" button which I clicked without taking note of the detailed error message. Does the lean server log error messages to a file somewhere? I'd like to check that before I report the issue on GitHub. I am using a MacBook Pro with M1 Max chip, macOS Venture 13.0. I had to install lean using Rosetta. Thanks.

[Julian Berman]

I'm not sure if VSCode does it by default -- but if the server crashed really hard (via say sigabrt'ing, which if this is Lean 3 on an M1 I think is a possibility), you might find it in Console.app (find that in spotlight via cmd-space if you haven't used it before, and in crash reports check if you see one that says it's from a lean process)

[Arthur Ryman]

@Julian Berman Thanks for the pointer to Console. I checked. No Lean message.

[Julian Berman]

Has it happened again since whenever it happened last?

[Arthur Ryman]

@Julian Berman It just happened once, but I haven't been using VS Code as much lately. If it happens again I'll take a screenshot of the error message and post it here.