leanOptions handling potentially brokeen

[mo271]

Adding

[leanOptions]
weak.linter.unusedVariables = false

to the lakefile.toml
causes build failures in the literate faces, see commits in an example repo I made:

https://github.com/mo271/WeakLiterate

I have a potential fix prepared, will make a pr shortly.

[mo271]

This is not just theoretical, but also affect the real-world repo https://github.com/google-deepmind/formal-conjectures/