Auto-implicits

Stream: mathlib4

[Yaël Dillies]

Is turning off auto-implicits mathlib-wide on the table? I just had a very confusing error because I used npow_rec, which created an auto-implicit called npow_rec, while had they been disabled I wouldn't have spent 15min to see that I meant npowRec.

[Mario Carneiro]

@Kevin Buzzard has mentioned that he has as part of his workflow to put a set_option at the top of the file and then remove it when he is done

[Mario Carneiro]

I think it is a useful feature and don't want to remove it for new code, but for porting it's generally better to disable auto-implicits

[Yaël Dillies]

I would be happy if I could remove it locally without touching code (I don't think asking people to write set_option AutoImplicit False at the top of each file they edit is a viable solution), because I can see this problem repeating over and over again.

[Yaël Dillies]

Better error messages would help too. In my case, the error was a cryptic and uninspectable

invalid default value for field, it contains metavariables
  zsmulRec nsmul

[Yaël Dillies]

(or rather inspectable, but didn't give me the crucial info)

[Mario Carneiro]

mathport could add the set_option line

[Mario Carneiro]

I have no idea what you want to do about the error message

[Yaël Dillies]

Sure, but that doesn't help with writing new code.

[Mario Carneiro]

for new code the option shouldn't be disabled

[Marc Huisinga]

Maybe the error message could point it out if auto-implicits are involved?

[Mario Carneiro]

that's what I just said above

[Yaël Dillies]

Well, I want it disabled for me :stuck_out_tongue_closed_eyes:

[Yaël Dillies]

The error message never told me what the metavariable was.

[Mario Carneiro]

You can do that by modifying the lakefile

[Mario Carneiro]

you can add set_options that apply globally there

[Mario Carneiro]

and if you don't push the lakefile changes then you can work with a different set of options than everyone else

[Yaël Dillies]

That doesn't really work with my setup, though. I'm working on fresh gitpods every time.

[Mario Carneiro]

okay... if you have no personal configuration then I'm not sure how you expect to persist personal changes

[Yaël Dillies]

Those auto-implicits definitely break the principle of least surprise, which I why I would like to consider disabling them mathlib-wise, given that mathlib is mostly targeted towards mathematicians.

[Mario Carneiro]

I think you just aren't used to them yet. The syntax highlighting is very good for spotting auto-implicits

[Yaël Dillies]

Auto-implicits don't show up in #where either, right?

[Mario Carneiro]

that wouldn't make any sense?

[Yaël Dillies]

Well, variable {f : α → α} now makes sense, so I sure hope my question does make sense.

[Mario Carneiro]

I have found that it is much easier to get the types right with auto implicits instead of long-scoped variable lines

[Mario Carneiro]

Often you can just avoid needing variable lines at all, and then you don't need to use #where all the time either

[Yaël Dillies]

All the files I've structured use long-scoped variable lines, sorted by increasing typeclass assumptions, and very short lemma statements.

[Yaël Dillies]

I'm not sure how you would achieve short statements with auto-implicits in topology or algebra.

[Mario Carneiro]

It depends on the theorem, but if the statement already implies the necessary typeclass assumptions then you don't need any variable lines

[Mario Carneiro]

you just have the same short statement without the variable line

[Moritz Doll]

Yael, the experience is completely different between porting existing code and writing new code. At first I thought it was nonsense as well (I have coe being a type), but it is so nice, when you remove all the boilerplate that is just defining types.

[Kevin Buzzard]

Yes this autoImplicit thing is very much a porting only technique. It's brilliant not to have to define various variables because the system just guesses them correctly.

[Siddhartha Gadgil]

Mario Carneiro said:

You can do that by modifying the lakefile

I did not realise this. I get bitten by auto_implicit often enough that it is probably worth doing this for my code, and even more so for code on which students depend.

[Jon Eugster]

Mario Carneiro said:

you can add set_options that apply globally there

I didn't quite get this to work, I just added some lines

set_option autoImplicit false
set_option ...... false

anywhere in the lakefile.lean, but it does not seem like they're globally set. Is there a documentation of that feature?

[Alex J. Best]

You can add -D autoImplicit=false as an extra Lean 4 server arg in your vscode settings, this should persist acrosss instances of gitpod if set up properly

[Sebastian Ullrich]

We could also (optionally) display auto implicits as LSP inlay hints (specially highlighted text that is not actually part of the editor) as in ... {α} .... Except that as usual the API is not really made for the incremental processing of a theorem prover.

[Gabriel Ebner]

FYI, inlay hint requests support ranges and the LSP server can request inlays to be refreshed, so we could send partial results and then update them as the file is process: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.18/specification/#workspace_inlayHint_refresh All of this seems to be implemented in VS Code.

[Sebastian Ullrich]

The part that made me hesitate to use the analogous request for semantic highlighting is that it is an unconditional workspace-wide refresh. But I don't think we will know whether that is a performance issue in editors without trying.

[Patrick Massot]

Note that semantic highlighting is already brittle in VSCode. Sometimes VScode gets tired of highlighting stuff and needs to be reloaded.