lakefile now accepts an extra file

[oxe-i]

1. Adds the flag --wfail to lake test to treat warnings as errors.
2. Adjust lakefile.toml so that it accepts an extra file called Extra.lean.

For performance reasons, we don't use the exercises' lakefile.toml in the test runner. This is because we pre-build some modules to reduce build times during tests.

However, once lakefile.toml changes, lake recompiles all the modules, so, in order to pre-build, we must have a generic lakefile that is used when creating the test-runner docker image and again to test every exercise.

This generic lakefile.toml currently has a structure that only accepts the solution file and the test files, making it impossible to implement exercises that accept extra modules. This PR fixes that by adding an extra Extra.lean module to the lakefile.

While doing that, I've also added --wfail to lake test and an extra configuration to lakefile.toml. Both serve to treat warnings as errors, making the build to fail. This is necessary in some exercises and good practice in the others.

[keiravillekode]

Some additional context motivating this change is in

exercism/lean#176
exercism/lean#177

[oxe-i]

@exercism/guardians just in case the notification got lost