moreServerOptions and moreLeanArgs

Stream: lean4

[Dan Velleman]

I have a project in which I have included moreServerOptions in the package declaration and moreLeanArgs in the declaration of a lean_lib, which is the default target. (I did it that way because I was copying another lakefile that did it that way.) This works fine for files that are part of the library. But if I have a Lean file in the project that is not part of the library, I can open it in VSCode and write proofs in that file, but the options I set in moreServerOptions and moreLeanArgs don't seem to apply. (For example, I would like to set pp.funBinderTypes to true.) Is there a way to set options that apply to all files in the project, whether they are part of a build target or not?

I don't think I really understand the difference between server options and lean arguments. Do I have to set both? Does it depend on what option I'm setting?

[Yaël Dillies]

Someone please correct me but I believe that server options are for interactive use (eg within vscode through the extension) while Lean args are for building (eg lake build)

[Dan Velleman]

It looks like leanOptions does both--options for both lean and the server. But the options still don't seem to apply to a file that I open in VSCode but that isn't part of a build target. That's what I'm really looking for--a way to set options in any file.

[Eric Wieser]

I think the recommendation is that you should make the files you open in VSCode be part of a build target

[Mac Malone]

@Dan Velleman One way to do this is via setting moreGlobalServerArgs with e.g. -Dpp.funBinderTypes=true. Note that these settings wil apply to every Lean file, even those opened to other projects. This previously caused problems for some users, hence why this is no longer the default.

[Eric Wieser]

Is there any way to set options only for files which do not belong to any project?

[Mac Malone]

@Eric Wieser Not presently, but that could be added relatively easily. Maybe it would be worthwhile to make an issue?

[Eric Wieser]

I suspect that's the feature that Dan is asking for

[Eric Wieser]

(as setting moreGlobalServerArgs will break files in other projects when using goto definition; the pp options will break files which use #guard_msgs)

[Dan Velleman]

I am interested in lean files that are in the package's directory. I was assuming that any such file would belong to the project, even if it wasn't associated with a build target. When I open such a file, it uses the version of Lean specified in the lean-toolchain, and it uses the dependencies specified in the lakefile. So I was expecting that other things specified in the configuration of the package, such as leanOptions, would also apply to such files. But it sounds like that is not the case. That's why I was confused.

I have read the README file for lake, but I found it hard to understand. For example, I didn't know at first what "build" means. When I was first getting started with Lean, I didn't want to build anything, I just wanted to write proofs and have Lean check them, so I didn't know what building was for. There are references to olean, ilean, c, and o files, but I don't think there is any explanation of what those files are. I assumed at first that if I had 2 lean files in the package's directory, then one could import the other. It took me a while to figure out that a file can only be imported if it is in a library. I have gradually, by trial and error, figured out how to do most of what I want to do with lake. Is there some other document that I should have been reading that explains these things?

[Dan Velleman]

By the way, I am primarily interested in Lean for education rather than research. For education, I sometimes want to write files that have errors in them, to illustrate mistakes and how Lean catches them and gives error messages. I assume that such files cannot be part of a build target--the build would fail.

[Eric Wieser]

When you say "a package's directory", do you mean my_git_repository/Foo.lean or my_git_repository/MyLib/Foo.lean? The latter should work out of the box

[Eric Wieser]

Dan Velleman said:

I assume that such files cannot be part of a build target--the build would fail.

Not every build target has to be built. When used with the globbing option, lean_lib creates a build target for every lean file inside the folder. You can then only build the ones that are known to work when testing; perhaps by having a WorkingFiles.lean that imports all the error-free files, but not the erroring ones, and then using lake build WorkingFiles

[Dan Velleman]

I meant my_git_repository/foo.lean.

I suppose another possibility is to have MyLib1 and MyLib2. If MyLib1 is the default target, then I assume lake build will only build that one. It still seems strange to me to put files into a build target that I have no intention of building, but perhaps that is the recommended setup.