Project-wide `set_option foo true`?

Stream: new members

[Louis Cabarion]

What’s the recommended way to set set_option foo true "project-wide"?

In other words, I’d like it to behave as if every .lean file in the project started with set_option foo true (after import:s), but configured in a single place (rather than repeating it in each file).

[Aaron Liu]

You can put it in the lakefile

[Louis Cabarion]

@Aaron Liu That sounds great! I checked the lakefile documentation but couldn’t find the name of the setting key. Do you know how to set it?

[Aaron Liu]

You can copy off of what mathlib does

[Michael Rothgang]

As another example (of a lakefile.toml; mathlib has a lakefile.lean): https://github.com/leanprover-community/sphere-eversion/blob/master/lakefile.toml sets the pp.unicode.fun to true