1
$\begingroup$

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?

$\endgroup$
7
  • $\begingroup$ 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). $\endgroup$
    – siegment
    May 21 at 6:01
  • $\begingroup$ @siegment "lean4.serverArgs": ["-DautoImplicit=false"] in .vscode/settings.json did the trick. Thanks a lot. Please post it as an answer. However, the setting is not shared between lake and the Lean4 VSCode extension. moreLeanArgs := #["-DautoImplicit=false"] in the lake only applies to lake. $\endgroup$ May 21 at 9:46
  • 1
    $\begingroup$ >However, the setting is not shared between lake and the Lean4 VSCode extension< Yes, that’s why I wrote about editor settings. $\endgroup$
    – siegment
    May 21 at 17:30
  • $\begingroup$ @siegment I understand. I was trying to further ask if there was a way to unify the settings? $\endgroup$ May 22 at 2:14
  • $\begingroup$ @siegment Unfortunately, "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$ May 22 at 2:50

1 Answer 1

1
$\begingroup$

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.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.