pass options to the whole project in lakefile

Stream: lean4

[MangoIV]

Hi, can I somehow pass set_option autoImplicit false to the entire project?

[Scott Morrison]

Check the Mathlib lakefile for examples!

[Kevin Buzzard]

The answer is surely yes because I believe that mathlib is doing something like this, so I would look there!

[Martin Dvořák]

https://github.com/madvorak/chomsky/blob/main/lakefile.lean

[MangoIV]

thank you so much, sorry for not looking by myself :D

[Martin Dvořák]

It's good you asked; this info isn't trivial to find.

[Marcus Rossel]

Is there a way to also make this work for options introduced by packages? I require a package X and want to set its option x.y to true globally. But if I use the leanOptions approach I get invalid -D parameter, unknown configuration option 'x.y' on all files which don't import X.

[Jon Eugster]

I think that still is not possible and is tracked here: lean4#3403