I hate `Level_n.lean`
Closed this issue · 6 comments
It's difficult to navigate the game levels on github or command line because everything's called Level_37.lean instead of add_comm.lean. Is there any way we could name levels arbitrarily in a more human-friendly way and have some other file which says what order they all go in? Or is this already possible?
The file names can be chosen arbitrarily. They just need to be imported somewhere. What determines the order is the number in the files after the Level command.
If you prefer, we could in principle change the implementation and remove the numbers completely and do things with names as we do for worlds.
Maybe the names should be 37_add_comm.lean or so to ensure that the files are listed in the correct order in VSCode.
Oh nice idea. Thanks a lot! It occurred to me after I opened this that the names might not matter (I don't have a clue how the software works), and have spent the last hour trying and failing to get a server running locally to check :-)
@joneugster would a PR be welcome with some file renaming? My attention is finally turning to this game.
yes please! :)
Actually I think that what I will do is to rewrite all of the levels!