Zulip Chat Archive
Stream: general
Topic: lean game server down
Johan Commelin (Dec 19 2024 at 07:58):
Is the lean game server down for everyone or just me?
Johan Commelin (Dec 19 2024 at 07:58):
Damiano Testa (Dec 19 2024 at 10:59):
I just clicked on the link, and it does not work for me either.
Kevin Buzzard (Dec 19 2024 at 12:22):
Aw man, just after that Hacker news mention too. Maybe it got hacked!
Mario Carneiro (Dec 19 2024 at 12:35):
or maybe these events are correlated
Johan Commelin (Dec 19 2024 at 14:54):
HN hug of death?
Ruben Van de Velde (Dec 19 2024 at 15:17):
Slashdotted, as we used to call it
Marcus Zibrowius (Dec 19 2024 at 16:16):
Probably just full hard drive. @Jon Eugster was working on this issue earlier today. I suppose he'll report once it's resolved.
Marcus Zibrowius (Dec 19 2024 at 16:17):
For future reference: @Matvey Lorkish is currently the canonical person to whom to report such faults. We will try to make this more obvious.
Jon Eugster (Dec 19 2024 at 17:20):
Yep I think we're a bit tight on space as mathlib, Lean and the interest in the games grow.
What I found interesting (besides obviously dead file that Incould delete) was that I got a few additional GB back by deleting all .lake folders and rebuilding the corresponding Lean projects again. Something I think I should try to reproduce again and report
Kevin Buzzard (Dec 19 2024 at 19:20):
Game.MyNat.PeanoAxioms has import Mathlib.Tactic in which probably imports a huge amount of mathlib most of which we don't want. Would minimising imports help? I can have a look at this now if you want @Jon Eugster
Kevin Buzzard (Dec 19 2024 at 19:22):
My memory from NNG3 was that sometimes people would complain that there was a Lean tactic which they wanted to use and couldn't use even in the lawless mode, so it looks like I played it safe and imported all the tactics.
Kevin Buzzard (Dec 19 2024 at 19:49):
https://github.com/leanprover-community/NNG4/pull/83
Christian K (Feb 13 2025 at 15:28):
Is the Lean game server down again?
https://adam-dev.math.hhu.de/ is just a blank page and https://lean.math.hhu.de/ does not work for me either
Eric Taucher (Feb 13 2025 at 15:30):
It seems up. If you use F12 from an Internet browser you can see that what is being served notes the Lean Game Server but there is an error with some JavaScript.
Eric Taucher (Feb 13 2025 at 15:30):
However it should probably be rebooted as it does seem to be in an invalid state for end user use.
Eric Taucher (Feb 13 2025 at 15:32):
@Matvey Lorkish
Could you please reboot the Lean Game Server. Thanks.
Matvey Lorkish (Feb 13 2025 at 16:12):
Apologies for the down time, I will reboot the server asap once I am home later in the evening!
Matvey Lorkish (Feb 13 2025 at 21:53):
Ok, the server seems to be working without my doing. Will look into it tomorrow in detail.
Last updated: May 02 2025 at 03:31 UTC