Arguments in lakefile

Stream: lean4

[Heather Macbeth]

Is there a way to set an option using moreServerArgs in the lakefile, when the option in question is defined in mathlib rather than in core Lean?

(If it matters, the option I want to set is this one.)

[Mac Malone]

I think you can do it the same way?

[Heather Macbeth]

@Mac Thanks for the answer ... to clarify, my usual lakefile doesn't even know about that option. Am I supposed to import mathlib to my lakefile??

[Mac Malone]

Unfortunately, I am apparently wrong. According to @Gabriel Ebner, custom options cannot be configured this way at all (without making a plugin).

[Heather Macbeth]

OK, thanks! What is a plugin?

[Mac Malone]

It is a special kind of precompiled module that Lake does not currently support (partially because Lean does not yet support them in custom frontends).