live.lean-lang.org indefinitely waiting

Stream: general

[Shreyas Srinivas]

Lean Live is indefinitely waiting for the server to start at the time of this message.

[Marc Huisinga]

Testing it now, it seems to work for me.

[Shreyas Srinivas]

Works for me now.

[Jon Eugster]

I think I observed that too sometimes, and I think it might be depending on where your cursor position is in the document. Further, I think I occationally have this in VSCode, as well (or used to have?).

Lean mentions it in this troubleshooting doc, so it's likely unrelated to the webeditor. Next time this happens, you could try if "☰ > Restart Server" does anything, or note the exact code and cursor position you had and file an issue at lean4web.

[Sebastian Ullrich]

I was updating the server OS today

[Shreyas Srinivas]

Okay. Thanks :). That would also explain why restarting the server failed for me at that time.

[Edward van de Meent]

I seem to be having this issue today, any chance it's the same cause? any other people with the same issue?

[Jovan Gerbscheid]

Yes, same here. Additionally, when it was working before, it was using an outdated version of mathlib, because the grw tactic wasn't available (which was merged Wednesday/Thursday)

[Shreyas Srinivas]

Even when you choose “Latest Mathlib”?

[Jovan Gerbscheid]

Yes, that's the default option (but currently the website doesn't work at all)

[Alexander Bentkamp]

It received an update today. Does the problem still persist? It seems to work fine for me.

[Jovan Gerbscheid]

In the infoview it shows the message "Waiting for Lean server to start..."

[Alexander Bentkamp]

@Joachim Breitner

[Alexander Bentkamp]

How about lean.math.hhu.de

[Alexander Bentkamp]

Sorry, I cannot reproduce this. It work fine for me.

[Jovan Gerbscheid]

Alexander Bentkamp said:

How about lean.math.hhu.de

It's got the same problem for me

[Alexander Bentkamp]

Can you try to clear your browser's cache?

[Jovan Gerbscheid]

It doesn't seems to help (I tried 3 different browsers)

[Ayhon]

On my end there are also no issues, and grw is available in "Latest Mathlib". Could it be a regional problem? My region is Paris, France

[Michael Stoll]

For me, it's also working (though it now and then appears to be slow).

[Alexander Bentkamp]

Can you check the developer console? Maybe some error shows up there?

[Jovan Gerbscheid]

I did see some funny messages in the webconsole

[LeanMonaco]: is ready!

Successfully compiled asm.js code (total compilation time 7ms)

Object { "@leanprover/infoview": "/infoview/index.production.min.js", react: "/infoview/react.production.min.js", "react/jsx-runtime": "/infoview/react-jsx-runtime.production.min.js", "react-dom": "/infoview/react-dom.production.min.js" }

TODO: catch JSON.parse failure: SyntaxError: JSON.parse: unexpected character at line 1 column 1 of the JSON data

TODO: data which is not JSON:

Array(7) [ "esms", true, true, false, false, false, false ]

14:50:51.694 - [InfoProvider] initInfoView got null client.

[Jovan Gerbscheid]

And

Fout bij brontoewijzing: Error: URL constructor:  is not a valid URL.
Stack in the worker:resolveSourceMapURL@resource://devtools/client/shared/source-map-loader/utils/fetchSourceMap.js:56:22
getOriginalURLs@resource://devtools/client/shared/source-map-loader/source-map.js:73:24
workerHandler/</<@resource://devtools/client/shared/worker-utils.js:115:52
workerHandler/<@resource://devtools/client/shared/worker-utils.js:113:13

[Johan Commelin]

Whut, where is the Dutch coming from?

[Jovan Gerbscheid]

That's the language of my laptop :sweat_smile:

[Jz Pan]

I got the same error

2025-06-16 234425.png

[Alexander Bentkamp]

Okay, I can reproduce it now. Seems to be a Windows issue.

[Kenny Lau]

push

[Joachim Breitner]

Is it indeed the case that all windows users are affected, and nobody on other platforms? Or only some?

[Edward van de Meent]

/poll are you experiencing this issue?/are you a windows user?
yes/yes
yes/no
no/yes
no/no

[Alexander Bentkamp]

I am close to having a fix. For the impatient Windows users, here is a workaround. Install the Firefox extension User Agent Switcher and set it to Linux or Mac.

[Joachim Breitner]

What’s the cause? (No hurry)

[Edward van de Meent]

:huh: why does this even matter????

[Aaron Liu]

I'm on chrome, how do I install a firefox extension

[Edward van de Meent]

i imagine there's an equivalent chrome extension

[Jz Pan]

Alexander Bentkamp said:

I am close to having a fix. For the impatient Windows users, here is a workaround. Install the Firefox extension User Agent Switcher and set it to Linux or Mac.

Sounds like that it's server's fault?

[Alexander Bentkamp]

To be honest, I haven't fully understood the issue yet, but at least I found a way to fix it. The fix will be deployed soon. The problem is caused by the different file path conventions under Windows vs Unix. For the VSCode extension in the browser and for the Lean server, I must provide a file path of the file being edited. Most of the packages in the browser use Windows file paths under Windows and the server uses Unix file paths. It would probably be better if all browser packages used the convention of the operating system. I'll see what I can do about that.

[Mario Carneiro]

@Aaron Liu you answered both yes/yes and no/no on that poll? Are you in superposition?

[Aaron Liu]

I have two machines

[Jz Pan]

Alexander Bentkamp said:

To be honest, I haven't fully understood the issue yet, but at least I found a way to fix it. The fix will be deployed soon. The problem is caused by the different file path conventions under Windows vs Unix. For the VSCode extension in the browser and for the Lean server, I must provide a file path of the file being edited. Most of the packages in the browser use Windows file paths under Windows and the server uses Unix file paths. It would probably be better if all browser packages used the convention of the operating system. I'll see what I can do about that.

Sounds really strange. Since User Agent Switcher will make it works under Windows, I assume that currently the server will response differently according to the user agent of the HTTP request to be Windows or not. So to me the solution is let the server ignore the user agent send from client, instead, always assume the client is Linux.

[Alexander Bentkamp]

The server does not respond differently. It's the javascript on th client that looks at the user agent and behaves differently.

[Jz Pan]

Alexander Bentkamp said:

It's the javascript on the client that looks at the user agent and behaves differently.

I see. So we should nuke the script... Is it come from some upstream projects? Maybe we should submit an issue.

[Alexander Bentkamp]

Yes, I haven't been able to identify the source yet. I think it might be monaco.

[Jz Pan]

Does downgrading to an older script helps?

[Alexander Bentkamp]

I dont think so, but I can only be sure when I find the source

[Joachim Breitner]

Should be deployed on live.lean-lang.org now. Thanks for fixing this, @Alexander Bentkamp !

[Alexander Bentkamp]

Thanks and sorry for the inconvenience!

[Jakub Nowak]

Same issue now. Maybe it should display something like "this is an expected maintenance"? So at least we know, there's a maintenance, not some error. Possibly with ETA.

[Joachim Breitner]

Works for me at the moment. Maybe a temporary usage spike?

[Alexander Bentkamp]

It was broken for me an hour ago and now it works.

[Joachim Breitner]

Yeah, looks like someone was using lots of memory:

Dec 17 08:15:24 live systemd[1]: server.service: A process of this unit has been killed by the OOM killer.
Dec 17 08:15:24 live systemd[1]: server.service: Failed with result 'oom-kill'.
Dec 17 08:15:24 live systemd[1]: server.service: Consumed 22min 21.079s CPU time, 113.1G memory peak, 31.9G memory swap peak, 80G read from disk, 70.8G written to disk, 8.8M incoming IP traff>
Dec 17 08:15:25 live systemd[1]: server.service: Scheduled restart job, restart counter is at 6.
Dec 17 08:15:25 live systemd[1]: Started server.service.
Dec 17 08:15:25 live server[3664533]: HTTP on port 8080

[Snir Broshi]

I was playing around with a panic bug on the site around this time, but the site was live until 2025-12-17T08:50:00+02:00, could it be related? What timezone are the logs you sent in?

[Joachim Breitner]

UTC

[Snir Broshi]

Joachim Breitner said:

UTC

So they're 75 minutes after Jakub reported above that the site was down. Maybe the 22min in the logs is not the real time, and it's about a process that took 75 minutes to get killed by the OOM killer?

[Shreyas Srinivas]

I conducted an interview over it and it took a lot of time to respond at times

[Shreyas Srinivas]

This was between 16:10 and 16:35 Berlin time

[Jovan Gerbscheid]

I often get into a position where after typing some stuff, Lean won't load anymore. My solution is to just refresh the website, and then it works again. This has especially gotten worse since a few months ago.