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?

Improve this question
$\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$
    – Simon Eatwell
    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$
    – Simon Eatwell
    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$
    – Simon Eatwell
    May 22 at 2:50

1 Answer 1

Reset to default
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.)

Improve this 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.