search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

Update to Lean 4.2.0 #8

Closed globin closed 9 months ago

globin commented 9 months ago

Fixes #7 for me locally

TentativeConvert commented 9 months ago

I tried this locally. With these changes, I can now run lake update -R in the Robo folder (and lake exe cache get in the Robo folder, and npm install in the lean4game folder). However, I still cannot run the Robo game locally. While NNG4 works, every time I try to open the Robo game I get an immediate error message

Server initialization failed. Source: extension

(This may be completely unrelated to this pull request – I just happened to have this particular comment window open as I was rather hopeful I'd be able to to report that I can finally run things locally again.)

globin commented 9 months ago

I have both folders on the same level and ran:

In Robo

lake update -R
lake exe cache get
lake build

In lean4game:

npm install
npm start

Then Robo works for me at http://localhost:3000/#/g/local/Robo

TentativeConvert commented 9 months ago

Thanks a lot! Yes, now it works. The command I was missing was lake build. I guess this also needs to go in the documentation. I updated the corresponding issue in the lean4game repository accordingly.

TentativeConvert commented 9 months ago

PS: I'm leaving it to @joneugster to merge this, since he's the one who knows what he's doing.

joneugster commented 9 months ago

Sorry for not merging this promptly, and thanks for the PR! This has now been superseded by the bump to v4.3.0-rc2,main should be now working again.