For game developers: small script for refactoring levels

Stream: Lean for teaching

[Marcus Zibrowius]

I've added a short bash script sofi.sh to the GameSkeleton repository that mildly simplifies the process of inserting/deleting levels within an existing game world. Quoting from the documentation:

Say, for example, you have an “Arithmetic World” in the folder

Game/Levels/Arithmetic

consisting of the three levels listed in the leftmost column of the table below. Suppose you want to
switch the order of multiplication and addition, and insert an additional level on subtraction in
between. Then you can simply edit the file names as in the second column, and add the additional
file for the level on substraction, so that the files are in the intended order when sorted
alphabetically (as displayed in the third column).

existing levels	manual changes	files in alphabetical order	end result
L01_hello.lean	L01_hello.lean	L01_hello.lean	L01_hello.lean
L02_multiply.lean	L03_multiply.lean	L02a_add.lean	L02_add.lean
L03_add.lean	L02a_add.lean	L02b_substract.lean	L03_substract.lean
	L02b_substract.lean	L03_multiply.lean	L04_multiply.lean

Calling

./sofi.sh Game/Levels/Arithmetic

will then

• rename the files as in the last column,
• update the level number in each file,

• make a reasonable attempt to update the import statements in each of the
  level files, and

• update the imports in the base file Game/Levels/Arithmetic.lean.

More details are documented in the script itself. I’ve been using this script for a while now, and it seems to work, but I still suggest you commit all your changes before giving it a try.