Is it possible to display loading progress?

leanprover-community / lean4game

Server to host lean games.

https://adam.math.hhu.de

GNU General Public License v3.0

199 stars 35 forks source link

Is it possible to display loading progress? #87

Closed TentativeConvert closed 12 months ago

joneugster commented 1 year ago

Not that easily, I believe.

abentkamp commented 1 year ago

As we discussed, I believe most of the loading time comes from loading the olean files. This needs to happen every time we open a new level because levels might have different imports.

The problem with loading process is that we generally cannot predict how many oleans must be loaded, as the dependencies of any given olean file can only be determined once it has been loaded. But at least we could display the number of oleans that have been loaded so that the user can see that something is happening. Or we could even save the number of oleans somewhere, which would allow us to give a percentage as well.

TentativeConvert commented 1 year ago

Any kind of visual feedback every time an olean file loads would be a massive improvement over the current situation (e.g. an "led" that lights up every time loading of a file is completed). Displaying the number of files loaded seems unnecessarily technical. Obviously, computing and visualizing a percentage would be optimal.

joneugster commented 1 year ago

Some progress has been made in and around f6727e5c9f7f638fa05c6ce60d4a11e07682ecdb.

joneugster commented 12 months ago

The current implementations of Alex seem to resolve this now:

Starting a game should be almost instant thanks to the JSON files
Loading a level shows progress in means of the loading circle filling up counting the imported modules.

Therefore, I think Ill close this issue for now.