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.