leanprover-community/lean4game

Make Loading Faster

Closed this issue · 3 comments

abentkamp commented
Make Loading Faster
abentkamp commented

82af2de makes the initial loading of the game much faster, but the loading of levels is still very slow. It might be a good idea to load all levels immediately, even if the user hasn't opened them. The impact on memory should be small since mmap is used to share the memory across the different processes.

Seasawher commented

I measured how many seconds it takes to redisplay after reloading with a local preview using docker, and it took more than 1m.

The Dockerfile used can be found at leanprover-community/NNG4#5 (comment).

joneugster commented

I timed this today with the Robo game:

  • Built the container at 100s
  • Server ready at 160s
  • (Reopening devcontainer: 3s)
  • Loading a game: 1.5s
  • Loading an empty level: 3.5s
  • Loading a level with 10 lines of code: 4.0s

This indicates that the devcontainer setup might be fast enough at present.

I'd close this issue for now. We did visit the mmap idea above and something seems to not work there so the impact on memory outweights the waiting time.