std doesn't work within mathlib any more

Stream: std4

[Kevin Buzzard]

With mathlib open in VS Code, I just jumped to definition to a definition in Std and found that the file (Std.Logic) didn't compile in VS Code any more -- looks like the issue is no autoimplicits. I've been a way for a week so might have missed the memo -- is this expected?

[Mario Carneiro]

unfortunately yes

[Mario Carneiro]

there was a previous zulip thread about it, but it looks like change might be hard

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lake.20server.20uses.20options.20from.20the.20wrong.20package/near/376826199

[Scott Morrison]

We could turn back on autoImplicit in mathlib... Just sayin' :-)

[Mario Carneiro]

actually this is odd, if I import Lake.Util.Proc then I can see and compile some autoimplicits there (e.g. Lake.logProcCmd) even from a server rooted in mathlib4, even though if I copy-paste that definition into a fresh file it doesn't work in mathlib itself. But Std.Logic is indeed broken

[Eric Wieser]

Scott Morrison said:

We could turn back on autoImplicit in mathlib... Just sayin' :-)

Or off in std :-)

[Alex J. Best]

Won't you have the same issue jumping to things in core / aesop / etc too?

[Eric Wieser]

Yes, that was a joke, sorry.

[Eric Wieser]

But this isn't new with autoImplicit false, we already had this problem with relaxedAutoImplicit

[Eric Wieser]

If this is really obnoxious, perhaps we should have a mathlib_preamble command that runs at the top of every file, and use that instead of fiddling with global options that have the wrong scope

[Mario Carneiro]

Alex J. Best said:

Won't you have the same issue jumping to things in core / aesop / etc too?

Apparently not core / lake, that was the topic of my message above. I don't really understand why, but they are different from other dependencies since lake doesn't build them.

[Kevin Buzzard]

I am all of a sudden much keener on having autoImplicits back. I still loathe them but this consequence is quite unpleasant.

[Mario Carneiro]

this is pretty clearly a lake/server bug though, the same thing would happen for any global option. If we capitulate on this then we will basically be giving up on global (project-specific) options entirely

[Kevin Buzzard]

Jireh points out via DM that I should say that it was the multi-character autoImplicits which I loathed.

[Mac Malone]

Mario Carneiro said:

this is pretty clearly a lake/server bug though

This is not a bug. This is an expected limitation of the current implementation of the Lean server (and the editor integrations). Workspace / Server configurations effect all files opened in the same instance of the editor. Support for multiple workspaces in the same editor in the future is under consideration, but if it comes, it will be an new feature, not a fix.

[Mac Malone]

This limitation also extends beyond go-to-def, it is that same reason why, for instance, opening file in a test or example in Lake codebase when editing the whole Lake package will have import failures (because the workspace uses the Lake package configuration not the examples or tests).

[Mac Malone]

However, I should note, I certainly would love to support these use cases in the future! :grinning_face_with_smiling_eyes:

[François G. Dorais]

These are very highly desired features! Thank you for considering them!

[Scott Morrison]

Haha! The Mathlib tests don't work with Mathlib any more.

Open up e.g. test/rewrites.lean, and it is full of errors.

Explanation:

• in CI it is running without turning off autoImplicit, but
• when opened in VSCode autoImplicit is turned off.

[Scott Morrison]

My solution to this would be to turn autoImplicit back on, so perhaps someone else can fix this. :-)

[Eric Wieser]

I thought @Alex J. Best made a PR to fix this

[Eric Wieser]

#6597, which is already merged

[Alex J. Best]

#6597 looks like I didn't touch rewrites for some reason. Maybe it was ok before some other recent change to that file?

[Eric Wieser]

I would guess the missing piece is setting the flags in CI to ensure it doesn't regress

[Alex J. Best]

I'm not sure what to do really. To make that PR I had to make test a package in the lake file so that I could run lake build on the whole directory. Surely there is a better way to do it. But I'm still a bit surprised lake env lean test/ doesn't use the args

[Eric Wieser]

That doesn't surprise me at all, I think that just means "set environment variables then run lean test/"

[Eric Wieser]

If we want to pass args to lean we need to do so with lean -DautoImplicit=false test or similar

[Scott Morrison]

@Mac Malone , could we ask you the best way to do this? We would like the Mathlib tests to run with the arguments (e.g. autoImplicit=false) that are set in the lakefile?

[Eric Wieser]

I guess this would also mean the tests run with pp.unicode_fun or whatever it's called

[Mario Carneiro]

This was part of lake#147

[Mac Malone]

@Scott Morrison For now, I would just suggest manually passing the options on CLI in the test runner (i.e., the Makefile).

[Mario Carneiro]

Mac Malone said:

Mario Carneiro said:

this is pretty clearly a lake/server bug though

This is not a bug. This is an expected limitation of the current implementation of the Lean server (and the editor integrations). Workspace / Server configurations effect all files opened in the same instance of the editor. Support for multiple workspaces in the same editor in the future is under consideration, but if it comes, it will be an new feature, not a fix.

I think this is very clearly a bug in the sense "these features (project-specific option setting, lean server mode) do not work together as would be expected by anyone who understands what they are supposed to do"

[Mario Carneiro]

the fix may indeed require some rearchitecting

[Mario Carneiro]

I don't think there was ever a point at which this "feature" was considered and rejected as out of scope for the server mode

[Mac Malone]

@Mario Carneiro I would like to politely disagree. First, moreServerArgs is not a project-specific option, it is a workspace-global one (workspace configuration is simply inherited from the root package), and this is by design . In many cases, this is what is desired (i.e., if a user sets pp.unicode_fun=true, they probably want to see it in dependent packages as well). Second, global server options were originally a design decision of the lean --server, not Lake. If you were to skip Lake entirely and run lean --server -DautoImplicit=false, you would get the same behavior. Finally, moreLeanArgs is the package-specific option. Where the feature proposed here to be added, it would use those plus moreServerArgs of the workspace to instantiate file workers based on where the package the file resides. However, the Lean server currently does not support per-file-worker arguments, so that cannot be done without a significant change in design.

[Mario Carneiro]

the issue here is not moreServerArgs, it is moreLeanArgs being set per-project

[Mario Carneiro]

the reason mathlib sets moreServerArgs is because if you don't set them then mathlib can't even compile itself in the server

[Mario Carneiro]

However, the Lean server currently does not support per-file-worker arguments, so that cannot be done without a significant change in design.

aka "it's a bug but it will be hard to fix without re-architecting"

[Mac Malone]

Mario Carneiro said:

aka "it's a bug but it will be hard to fix without re-architecting"

An unsupported feature is not a bug.

[Mario Carneiro]

It's a feature that already exists and was not implemented correctly

[Mac Malone]

Mario Carneiro said:

the reason mathlib sets moreServerArgs is because if you don't set them then mathlib can't even compile itself in the server

What do you mean by this? Mathlib would certainly compile without -DautoImplicit=false.

[Mario Carneiro]

If mathlib's lakefile was to set moreLeanArgs but not moreServerArgs then you wouldn't be able to open any file, and the title of this topic would be "mathlib doesn't work within mathlib anymore" instead

[Mac Malone]

Mario Carneiro said:

It's a feature that already exists and was not implemented correctly

moreLeanArgs explicitly states that it only effects lean compilation (not interactive editing)

[Mario Carneiro]

Options are not optional for lean. If you get them wrong everything breaks. So I do not accept this reasoning of "it's just not an implemented feature", this is just wrong behavior. If we didn't want to handle this we shouldn't have added project-specific options

[Mario Carneiro]

Mac Malone said:

What do you mean by this? Mathlib would certainly compile without -DautoImplicit=false.

Maybe this one, but if you turn off -Dpp.unicode.fun=true then tests break

[Mac Malone]

Mario Carneiro said:

If mathlib's lakefile was to set moreLeanArgs but not moreServerArgs then you wouldn't be able to open any file

Why? None of Mathlib's server configuration options pp.unicode.fun=true,autoImplicit=false,relazedAutoImplicit=false should have this effect (one is meant to be purely visual, and the other two just disable features, meaning that the code they support is a strict subset of the default supported code).

[Mac Malone]

Mario Carneiro said:

Maybe this one, but if you turn off -Dpp.unicode.fun=true then tests break

True, though I could argue that is a bug with #guard_msgs being dependent on visual customization options.

[Mario Carneiro]

Hardly. The fact is, all options can potentially change behavior, if only by changing what the result of getOption returns, so in general only the user (or package maintainer) can make the call on whether adding/removing it is safe for the project

[Mario Carneiro]

anyway we wouldn't be having this discussion if turning these options on / off was harmless

[Mario Carneiro]

it has broken code due to its misapplication

[Mario Carneiro]

and there is currently no way to set options to avoid the breakage

[Mario Carneiro]

other than just not setting options at all, which again is just saying the feature is broken

[Mac Malone]

Mario Carneiro said:

general only the user (or package maintainer) can make the call on whether adding/removing it is safe for the project

Yes, this a decision by the package manager to determine which set of options they choose to support.

[Mac Malone]

I certainly think users should ideally be able to choose workspace-wide presentation options. I do not think all options should be package-specific.

[Mario Carneiro]

Sure. These are supposed to be package-specific options though

[Mario Carneiro]

no one is interested in workspace-wide options here

[Mario Carneiro]

those are useful for sure, but most packages will be in no position to set them

[Mac Malone]

Mario Carneiro said:

Maybe this one, but if you turn off -Dpp.unicode.fun=true then tests break

Also, this does not actually currently break tests because the tests that need it currently set this at the top of the file (or otherwise they would break the CI which does not set this).

[Mario Carneiro]

yes, that's the workaround. Your point?

[Mario Carneiro]

it's still broken behavior

[Mac Malone]

Mario Carneiro said:

no one is interested in workspace-wide options here

At the very least, I am. That is why I added moreServerArgs in the first place.

[Mario Carneiro]

I mean, they aren't the cause of the issue here

[Mario Carneiro]

They kind of indirectly are, because mathlib sets moreServerArgs as well as moreLeanArgs, but it only does that because the server doesn't use project-specific options correctly

[Mario Carneiro]

I'd rather talk about how we fix the root cause, and pass project-specific options to the server

[Mac Malone]

Mario Carneiro said:

it's still broken behavior

Okay, I get the feeling we are not going to come to an agreement here. You and I fundamentally disagree on what should be the expected behavior of these programs, and that is fine. I just wanted to clarify that the current behavior is expected and intended from the developer's perspective.

[Mario Carneiro]

it's intended for opening std from mathlib or vice versa to break?

[Mario Carneiro]

It might be expected, but intended seems a bit unlikely

[Mac Malone]

@Mario Carneiro Yes, if one globally disables a feature the other one relies on being enabled.

[Mario Carneiro]

okay, let's say no one sets moreServerArgs. No global options here. Only now you can't even open mathlib files in mathlib

[Mac Malone]

@Mario Carneiro Again, I am very confused about this assertion, why does this break mathlib? That does seem like a bug somewhere since nothing I know of should depend on those arguments being set.

[Mario Carneiro]

sigh. The details of the options aren't that important here, let's suppose autoImplicit was off by default and enabled by mathlib if it helps

[Mario Carneiro]

it's just as unacceptable for mathlib to incorrectly accept code as to incorrectly reject code

[Mac Malone]

@Mario Carneiro There are many cases were the server accepts (or rejects) code that would not be if the module is compiled. (For instance, #eval'ing an extern definition).

[Mario Carneiro]

Honestly, setting -DautoImplicit=false in the args to be used by CI isn't even that important. It is primarily used for its effect on the server

[Mario Carneiro]

but it needs to be an effect on the server when it is compiling a file from mathlib and not otherwise

[Mac Malone]

@Mario Carneiro Yes, I agree that this is nice to have. I am also confident it can be implemented. My only goal was to make clear that this is known to be currently unsupported.

[Mario Carneiro]

Yes I know you know that the bug exists

[Mario Carneiro]

I would like us to fix it though

[Mac Malone]

:thumbs_up:

[Mario Carneiro]

because more people are noticing, and it really does degrade the cross-project go to def experience

[Mario Carneiro]

as far as lake changes are concerned, I do think there is one place it can help, namely to have a moreServerArgs field in LeanConfig

[Mac Malone]

@Mario Carneiro This feature requires the server to figure out what package each file belongs to, get that information from Lake and use it to configure the workers. That requires tighter integration between Lean and Lake than is currently supported. So, this will require rework. Whether that is the highest priority is something that has to be internally discussed. However, if you want to make an issue about it on the lean 4 repo and gather support, feel free to do so!

[Mario Carneiro]

I am willing to write a patch

[Mario Carneiro]

the simpler implementation I am thinking of would be to have the server ask lake for the lean options for a given file

[Mario Carneiro]

although it might be hampered by the issue where lake takes 1 second to do anything

[Mac Malone]

Mario Carneiro said:

although it might be hampered by the issue where lake takes 1 second to do anything

That is a performance bug that I am working on addressing. lean4#2444 is one step in that direction.

[Mac Malone]

And also a great example of something that could be considered higher priority than this feature. To be clear, I want to add the feature mentioned in this thread. It just is not my current highest priority.

[Joachim Breitner]

Another stance on the issue, which would solve (or at least sidestep) this problem without adding more logic and coupling to our tools, could be this:
it's not desirable of the meaning of a lean file is unclear without consulting additional information elsewhere. This makes it harder for humans to read it, or to copy it into separate projects etc.
So setting options that, in a way, change how the language work elsewhere isn't great.
The conclusion would be that every file should be explicit about every deviation from the standard lean settings!
Yes, this would mean that every file in mathlib4, would turn autoImplicits off. But as a reader of files, I'd actually appreciate that! Else switching between projects I have to remember which settings are where.
If the boiler plate at the beginning of the files gets too big, one could probably define and use a mathlib_options macro (as was suggested before).
At least until per-package-options are implemented, this might be the lesser evil, compared to not being able to open std files in a mathlib workspace?
(This opinion is influenced by best practices around Haskell language extensions, which are quite like these language-changing options, and per-package configuration in the build tool is possible, but not encouraged.)

[Mario Carneiro]

this was how lean 3 worked BTW

[Joachim Breitner]

Was it bad?

[Mario Carneiro]

I think it's fair to say there was an unfilled niche

[Mario Carneiro]

mathlib still scrambles sometimes to determine where "the first file" is so that it can shove a bunch of initialization in there

[Mario Carneiro]

in any case I don't like the idea of using implementation difficulties as a justification here

[Joachim Breitner]

I'd say the resulting implementation simplicity (no urgent need for per-package-configuration options) is just a nice side-benefit, and the main justification would be “explicit is better than implicit” and maybe also easy portability of files between projects.

[Mario Carneiro]

your suggestion wouldn't exactly make portability easier since the target project doesn't have mathlib_options

[Mario Carneiro]

I'm not sure it would be any more explicit either, you still have to look up the definition of mathlib_options to find out what the settings are

[Joachim Breitner]

My (primary) suggestion is to write out the option explicitly, which (certainly as long as it’s only one option) I’d prefer over the macro.

The macro still has the advantage of being explicit in “something changes” and offering the user a tooltip to find out more. And it would also work in projects that import mathlib, wouldn’t it?

[Eric Wieser]

Joachim Breitner said:

At least until per-package-options are implemented, this might be the lesser evil, compared to not being able to open std files in a mathlib workspace?

I agree this seems like the best solution (combined with a linter to enforce it be used in every file), assuming there are enough people impacted by not being able to open std files.

[Eric Wieser]

(to be clear, I am not suggesting we enforce disable autoImplicit; but that we enforce that enabling it be spelt mathlib_options; set_option autoImplicit true)

[Mario Carneiro]

In any case, I put up an implementation at lean4#2456

[Bhavik Mehta]

Is there progress on this? It came up in LftCM that Std is full of errors if you open it from mathlib4

[Eric Wieser]

Or is the problem that it's full of errors if you open it from LftCM?

[Bhavik Mehta]

This was for mathlib4, opened from my clone of mathlib4 not my clone of LftCM

[Mario Carneiro]

it's blocked on the RFC lean4#2455. If you want to see progress on it please upvote / comment on the thread because I don't know any other way to move this stuff forward

[Mario Carneiro]

Or poke @Mac Malone since I think he's the one in charge of this part of the code (there is some server code too, not sure who owns that right now cc: @Sebastian Ullrich )

[Sebastian Ullrich]

Yes, this is slightly awkward timing with server ownership being moved from me to Marc. Please bear with us. As a workaround, does opening it as a separate workspace root work (I didn't check if that was discussed before)?

[Mario Carneiro]

it does

[Mac Malone]

@Mario Carneiro The PR still has some problems that need to be addressed (see my comment). That is why nothing has happened lately on it from my end.