I want to turn off the autoImplicit option for a whole lake project. Could I achieve that in lakefile.lean? The options moreLeanArgs, moreLeancArgs, and moreLinkArgs don't seem to concern set_option; am I mistaken?
$\begingroup$
$\endgroup$
7
1 Answer
$\begingroup$
$\endgroup$
moreLeanArgs := #["-DautoImplicit=false"] works for me, but you need (probably) also add -DautoImplicit=false to the Lean’s “Server Args” in your editor (e.g. VSCode).
(Reposted as answer.)
moreLeanArgs := #["-DautoImplicit=false"]works for me, but you need (probably) also add-DautoImplicit=falseto the Lean’s “Server Args” in your editor (e.g. VSCode). $\endgroup$"lean4.serverArgs": ["-DautoImplicit=false"]in.vscode/settings.jsondid the trick. Thanks a lot. Please post it as an answer. However, the setting is not shared betweenlakeand the Lean4 VSCode extension.moreLeanArgs := #["-DautoImplicit=false"]in the lake only applies to lake. $\endgroup$"lean4.serverArgs": ["-DautoImplicit=false"]will affect the live parsing of the prelude. Is there a way for the language server to apply global options at the project/library granularity? $\endgroup$