How does lakefile elaboration work in the Lean server?

Stream: lean4

[Eric Wieser]

If I paste

import Lake
open Lake DSL

package foo

into the web editor, or any file not called lakefile.lean, I get the error

elaboration function for `Lake.DSL.packageCommand` has not been implemented

Where is the code that special-cases lakefile.lean in the lean server, and what does it do in order to provide these missing elaborators?

[Mac Malone]

The relevent special case is here.

[Mac Malone]

For configuration files, Lake loads Lake as an elaboration plugin, which enables the Lake DSL (as the DSL is all builtin macros/elaborators/initializers now).

[Eric Wieser]

I guess this is a plugin to keep the Lean binary itself lighter-weight?

[Mac Malone]

Yes, and the DSL is builtin to avoid staging issues in Lake.