set_option per project

Stream: lean4

[Horatiu Cheval]

Is it possible to set an option once so that its effect applies in an entire project? Particularly, I want to disable autobound variables in all files in my project. Is there a way other than putting set_option autoBoundImplicitLocal false at the top of each file?

[Sebastian Ullrich]

Something like moreLeanArgs := #["-DautoBoundImplicitLocal=false"] in your lakefile.lean should do it

[Horatiu Cheval]

Sebastian Ullrich said:

Something like moreLeanArgs := #["-DautoBoundImplicitLocal=false"] in your lakefile.lean should do it

Thanks! This work in the sense that lake build throws an error, but the VSCode extension still doesn't seem to care, it behaves as if the option were set to true

[Sebastian Ullrich]

There is a separate moreServerArgs option (which may want to inherit moreLeanArgs? @Mac ), but it will not do anything in VS Code until https://github.com/leanprover/vscode-lean4/pull/118 is merged and released.

[Gabriel Ebner]

But you should probably not add -Dsomething=... to moreServerArgs because that will apply all files opened with that server, and we might want to open dependencies in the same server as the root project.

[Sebastian Ullrich]

Oh yes, semantic options should definitely not go in there. print-paths would be more appropriate, except that processing of arbitrary cmdline options at least has already happened at that point.

[Sebastian Ullrich]

Which is why I went with a more specific field for load-dynlibs

[Mac]

Sebastian Ullrich said:

There is a separate moreServerArgs option (which may want to inherit moreLeanArgs? Mac ), but it will not do anything in VS Code until https://github.com/leanprover/vscode-lean4/pull/118 is merged and released.

It also worth noting that adding -Dsomething=... to moreServerArgs won't actually do what one may expect as -D options are not forwarded to the workers (see here).

[Leonardo de Moura]

We also have this open issue https://github.com/leanprover/lean4/issues/14 for persistent set_options. It is not high priority, but we want to implement it for use cases like the one in this thread.