"A Lean Intro to Logic" server problem

[Madjosz]

When opening any level in A Lean Intro to Logic game I get a server connection error after some seconds:

Error while running Lake: thread 'main' panicked at src/elan-utils/src/utils.rs:472:32:
called Result::unwrap() on an Err value: Error { description: "Couldn't resolve host name", code: 6, extra: Some("Could not resolve host: github.com") }
note: run with RUST_BACKTRACE=1 environment variable to display a backtrace

[Trequetrum]

Hey @Madjosz. I'm the author of the "Intro to Logic" game. I just checked this out and saw the same error.
No idea what the problem is, but I've updated the game to v4.7.0 and it's working for me now.

Can you confirm whether this fixed things for you too?

[joneugster]

I deleted some old toolchains last week when debugging some space issues, sorry for that!

[Madjosz]

It's working again, thx for your work!