Zulip Chat Archive

Stream: new members

Topic: Where is the Lean Server Error Log?

Arthur Ryman (Nov 06 2022 at 21:04):

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 (Nov 06 2022 at 22:57):

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 (Nov 11 2022 at 13:26):

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

Julian Berman (Nov 11 2022 at 14:51):

Has it happened again since whenever it happened last?

Arthur Ryman (Nov 11 2022 at 15:06):

@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.

Last updated: Dec 20 2023 at 11:08 UTC